41 citations · 131 across the 6 of their papers we have counts for
Showing 2017Show all
3 papers · 1 filter
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★ 41 cited
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…
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…