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
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).
Keywords : constructive mathematics homotopy type theory type theory Semi-simplicial sets
Document type :
Journal articles
Complete list of metadatas
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
Long-term archiving on : 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

UNIV-PARIS7 | INRIA | INSMI | PPS | USPC | INRIA-ROCQ

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. ⟨10.1017/S0960129514000528⟩. ⟨hal-00935446⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

386

Files downloads

226

Contact


archive-ouverte@inria.fr