Generating Higher Identity Proofs in Homotopy Type Theory

Thibaut Benjamin

Finster and Mimram have defined a dependent type theory called CaTT, which describes the structure of omega-categories. Types in homotopy type theory with their higher identity typ…