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
1
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
