A dependently-typed construction of semi-simplicial types

Hugo Herbelin 1, 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
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).
Liste complète des métadonnées

https://hal.inria.fr/hal-00935446
Contributor : Hugo Herbelin <>
Submitted on : Thursday, January 23, 2014 - 3:15:42 PM
Last modification on : Friday, January 4, 2019 - 5:33:25 PM
Document(s) archivé(s) le : Thursday, April 24, 2014 - 12:10:22 PM

File

simplicial-revise-final.pdf
Publisher files allowed on an open archive

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Collections

Citation

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. ⟨http://journals.cambridge.org/article_S0960129514000528⟩. ⟨10.1017/S0960129514000528⟩. ⟨hal-00935446⟩

Share

Metrics

Record views

350

Files downloads

159