41 citations · 131 across the 6 of their papers we have counts for
6 papers · 1 filter
Two-Level Type Theory and Applications
Danil Annenkov, Paolo Capriotti, Nicolai Kraus +1
We define and develop two-level type theory (2LTT), a version of Martin-Löf type theory which combines two different type theories. We refer to them as the inner and the outer type…
Models of Type Theory with Strict Equality
Paolo Capriotti
This thesis introduces the idea of two-level type theory, an extension of Martin-Löf type theory that adds a notion of strict equality as an internal primitive. A type theory with…
Quotient inductive-inductive types
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra +2
Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotien…
Extending Homotopy Type Theory with Strict Equality
Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to def…
Functions out of Higher Truncations
Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi
In homotopy type theory, the truncation operator ||-||n (for a number n > -2) is often useful if one does not care about the higher structure of a type and wants to avoid coherence…
Non-wellfounded trees in Homotopy Type Theory
Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
We prove a conjecture about the constructibility of coinductive types - in the principled form of indexed M-types - in Homotopy Type Theory. The conjecture says that in the presenc…