A canonical normal form theorem for the type theory of regular categories in Cubical Agda

Cubical Agda formalization of the canonical normal form theorem for the type theory of regular categories.

Overview

We formalize the proof that every closed derivable judgement in the type theory of regular categories (T_reg) reduces to one in canonical form. The type theory is built from the terminal type, dependent sum, extensional equality, and quotient on the terminal type. The proof uses the method of computability predicates, following Valentini's approach for extensional Martin-Löf type theory.

Requirements

• Agda (tested with 2.8.0)
• agda/cubical library (0.9)

Typechecking

agda src/TReg/Everything.agda

References

• R. Borsetto. A canonical normal form theorem for the type theory of regular categories. Master thesis, University of Padova, 2023.
• S. Valentini. Meta-mathematical aspects of Martin-Löf's type theory. PhD thesis, Katholieke Universiteit Nijmegen, 2000.