Was trying to do the one in that internship report, but I'm having *issues* because my environments store values in WHNF, and they need to be shifted then: github.com/brendanzab/rus
Conversation
This Tweet was deleted by the Tweet author. Learn more
I did find the diff from mini-tt to the universe one though: github.com/simhu/cubical/
1
I find the syntax for environments/substitutions etc. super unclear though
1
My current issue is that lifting does not work through variables:
> (Fun (A : Type) -> A -> A)^1
Fun (x0 : Type^1) -> (Fun (x1 : x0) -> x0) : Type^2
> let Id = (Fun (A : Type) -> A -> A) in Id^1
Fun (x0 : Type) -> (Fun (x1 : x0) -> x0) : Type^1
😭🥴😫
1
This Tweet was deleted by the Tweet author. Learn more
Yes, this is where I am coming to as well!
1
Meaning I was thinking it through today and feeling that I might need it on neutrals. I'm just unsure what happens during readback? Do variables get the lift back?
1
I've found it leads to wacky behavior like:
> let Id = Fun (A : Type) -> A -> A in Id^2
Fun (x0 : Type^2) -> (Fun (x1 : x0^4) -> x0^4) : Type^3
If I add it to the var constructor on neutrals
This Tweet was deleted by the Tweet author. Learn more
This Tweet was deleted by the Tweet author. Learn more
tis heartening to know I am not the only one
1
Show replies