A dependently-typed construction of semi-simplicial types. (June 2015) - HERBELIN, HUGO
<x content-type="archive" xml:space="preserve">Abstract</x> This paper presents a dependently-typed construction of semi-simplicial sets in a 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).