I have an Agda formalization of canonicity in a similar manner, although with non-cumulative Coquand universes, if you're interested (the repo is a mess though sorry) github.com/AndrasKovacs/g
This Tweet was deleted by the Tweet author. Learn more
Conversation
wooooow - some impressive type signatures in Pi.agda! :O
1
Oh wait - every file has impressive type signatures in it
Type signatures are copied from UnfoldedDepModelTemplate.agda where they are given by printing everything with implicit params shown. My current "best practice" in Agda looks like this unfortunately.
2
1
hahaha this is just so... amaze
1
2