41 citations · 131 across the 6 of their papers we have counts for
8 papers
Univalent Higher Categories via Complete Semi-Segal Types
Paolo Capriotti, Nicolai Kraus
Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent cat…
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…
Free Applicative Functors
Paolo Capriotti, Ambrus Kaposi
Applicative functors are a generalisation of monads. Both allow the expression of effectful computations into an otherwise pure language, like Haskell. Applicative functors are to…