Formalizing two-level type theory with cofibrant exo-nat

Elif Uskuplu

This study provides some results about two-level type-theoretic notions in a way that the proofs are fully formalizable in a proof assistant implementing two-level type theory such…