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).
Type de document :
Article dans une revue
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〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00935446
Contributeur : Hugo Herbelin <>
Soumis le : jeudi 23 janvier 2014 - 15:15:42
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37
Document(s) archivé(s) le : jeudi 24 avril 2014 - 12:10:22

Fichier

simplicial-revise-final.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

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〉

Partager

Métriques

Consultations de la notice

270

Téléchargements de fichiers

100