Skip to Main content Skip to Navigation
Journal articles

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 : Semi-simplicial sets type theory homotopy type theory constructive mathematics
Document type :
Journal articles
Complete list of metadata
https://hal.inria.fr/hal-00935446
Contributor : Hugo Herbelin Connect 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

File

Vignette du document
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 | PPS | CNRS | INRIA | INSMI | INRIA2 | UNIV-PARIS

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 Datacite

Share

Metrics

Record views

151

Files downloads

131

 

Contact                    Legal Notice                    Personal Data