I find the syntax for environments/substitutions etc. super unclear though
Conversation
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
how does your naive version work? just brute force shift everything under binders?
This Tweet was deleted by the Tweet author. Learn more
This Tweet was deleted by the Tweet author. Learn more
Show replies