34 citations · 95 across the 15 of their papers we have counts for
6 papers · 1 filter
Algebraic Presentations of Type Dependency
Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North +1
C-systems were defined by Cartmell as the algebraic structures that correspond exactly to generalised algebraic theories. B-systems were defined by Voevodsky in his quest to formul…
Characterizations of modalities and lex modalities
J. Daniel Christensen, Egbert Rijke
A reflective subuniverse in homotopy type theory is an internal version of the notion of a localization in topology or in the theory of -categories. Working in homotopy typ…
Modal Descent
Felix Cherubini, Egbert Rijke
Any modality in homotopy type theory gives rise to an orthogonal factorization system of which the left class is stable under pullbacks. We show that there is a second orthogonal f…
Modalities in homotopy type theory
Egbert Rijke, Michael Shulman, Bas Spitters
Univalent homotopy type theory (HoTT) may be seen as a language for the category of -groupoids. It is being developed as a new foundation for mathematics and as an internal…
The join construction
Egbert Rijke
In homotopy type theory we can define the join of maps as a binary operation on maps with a common co-domain. This operation is commutative, associative, and the unique map from th…
Sets in homotopy type theory
Egbert Rijke, Bas Spitters
Homotopy Type Theory may be seen as an internal language for the -category of weak -groupoids which in particular models the univalence axiom. Voevodsky proposes th…