Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style

Florian Rabe, Navid Roux

Type theories can be formalized using the intrinsically (hard) or the extrinsically (soft) typed style. In large libraries of type theoretical features, often both styles are prese…