I did find the diff from mini-tt to the universe one though: github.com/simhu/cubical/
Conversation
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
how does your naive version work? just brute force shift everything under binders?