The category of equilogical spaces and the effective topos as homotopical quotients

DOI10.1007/S40062-016-0161-ZMaRDI QIDQ504545zbMATHOpenAlexFDO

Authors Giuseppe Rosolini

Publication date 17 January 2017

Published in Journal of Homotopy and Related Structures (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1511.06901

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Categorical logic, topoi (03G30) Topoi (18B25) Foundations, relations to logic and deductive systems (18A15)

Abstract: We show that the two models of extensional type theory, those given by the category of equilogical spaces and by the effective topos, are homotopical quotients of categories of 2-groupoids.

Recommendations

• A homotopy-theoretic model of function extensionality in the effective topos
• Equilogical spaces
• Martin-Löf complexes
• scientific article; zbMATH DE number 1531377
• Univalent polymorphism

Cites work

• scientific article; zbMATH DE number 3825806 (Why is no real title available?)
• scientific article; zbMATH DE number 4061468 (Why is no real title available?)
• scientific article; zbMATH DE number 45228 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• scientific article; zbMATH DE number 1522867 (Why is no real title available?)
• scientific article; zbMATH DE number 3794304 (Why is no real title available?)
• scientific article; zbMATH DE number 1392302 (Why is no real title available?)
• scientific article; zbMATH DE number 3257107 (Why is no real title available?)
• A small complete category
• Colimit completions and the effective topos
• Data Types as Lattices
• Equilogical spaces
• Homotopy type theory. Univalent foundations of mathematics
• Regular and exact completions
• Sobriety for equilogical spaces
• Some free constructions in realizability and proof theory
• The Discrete Objects in the Effective Topos
• Tripos theory

Cited in

(5)

• Homotopy theoretic models of identity types
• A homotopy-theoretic model of function extensionality in the effective topos
• Univalent polymorphism
• Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
• Categories of partial equivalence relations as localizations

This page was built for publication: The category of equilogical spaces and the effective topos as homotopical quotients

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q504545)