15 citations · 15 across the 1 of their papers we have counts for
3 papers
math.CT2017
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…
cs.LO2017★ 15 cited
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…
cs.LO2015
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…