Today's fun: trying to get my head around universe lifting operators in Pikelet again! This time, with actual normalisation-by-evaluation! 🌌🤔🤯
Conversation
Revisiting this internship report: "Dependently typed lambda calculus with a lifting operator" by Damien Rouhling (www-sop.inria.fr/members/Damien) - it's a bit delicate maintaining the universe levels in the environment. I'm finally seeing how it works together though... I think!
Replying to
The soundness proofs as always go over my head, as always. Really need to focus on learning to get my head around those at some stage!