A dependently-typed construction of semi-simplicial types

Hugo Herbelin (1, 2)

1 PPS - Preuves, Programmes et Systèmes
2 PI.R2 - Design, study and implementation of languages for proofs and programs

This paper presents a dependently-typed construction of semi-simplicial sets in type theory where sets are taken to be types. This addresses an open question raised on the wiki of the special year on Univalent Foundations at the Institute of Advanced Study (2012-2013).

Mots clés: Semi-simplicial sets; type theory; homotopy type theory; constructive mathematics

Domaines: Logique [math.LO]; Topologie algébrique [math.AT]; Logique en informatique [cs.LO]

Hugo Herbelin. A dependently-typed construction of semi-simplicial types. Mathematical Structures in Computer Science, 2015, From type theory and homotopy theory to Univalent Foundations of Mathematics, 25 (Special issue 05), pp.16. ⟨10.1017/S0960129514000528⟩. ⟨hal-00935446⟩