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