Conversation
This Tweet was deleted by the Tweet author. Learn more
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
1
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
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
(excuse the terrible pretty printing)