PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : 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).
https://hal.inria.fr/hal-00935446 Contributor : Hugo HerbelinConnect in order to contact the contributor Submitted on : Thursday, January 23, 2014 - 3:15:42 PM Last modification on : Friday, January 21, 2022 - 3:21:52 AM Long-term archiving on: : Thursday, April 24, 2014 - 12:10:22 PM
Hugo Herbelin. A dependently-typed construction of semi-simplicial types. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2015, From type theory and homotopy theory to Univalent Foundations of Mathematics, 25 (Special issue 05), pp.16. ⟨10.1017/S0960129514000528⟩. ⟨hal-00935446⟩