A homotopy-theoretic model of function extensionality in the effective topos. (10th September 2018)

• Record Type: Journal Article
• Authors: FRUMIN, DAN; VAN DEN BERG, BENNO
• Is Part Of: Mathematical structures in computer science. Volume 29:Number 4(2019)
• Page Start: 588
• Page End: 614
• Publication Date: 2018-09-10
• Subjects: Computer science -- Mathematics -- Periodicals; 004.015105
• DOI: 10.1017/S0960129518000142
• Languages: English
• ISSNs: 0960-1295

Abstract

Abstract : We present a way of constructing a Quillen model structure on a full subcategory of an elementary topos, starting with an interval object with connections and a certain dominance. The advantage of this method is that it does not require the underlying topos to be cocomplete. The resulting model category structure gives rise to a model of homotopy type theory with identity types, Σ- and Π-types, and functional extensionality. We apply the method to the effective topos with the interval object ∇2. In the resulting model structure we identify uniform inhabited objects as contractible objects, and show that discrete objects are fibrant. Moreover, we show that the unit of the discrete reflection is a homotopy equivalence and the homotopy category of fibrant assemblies is equivalent to the category of modest sets. We compare our work with the path object category construction on the effective topos by Jaap van Oosten.