41 citations · 172 across the 17 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…
math.LO2017★ 9 cited
Space-Valued Diagrams, Type-Theoretically (Extended Abstract)
Nicolai Kraus, Christian Sattler
Topologists are sometimes interested in space-valued diagrams over a given index category, but it is tricky to say what such a diagram even is if we look for a notion that is stabl…