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

DOI10.1007/S40062-016-0161-ZzbMATH Open1375.18018arXiv1511.06901OpenAlexW2963097660MaRDI QIDQ504545FDOQ504545

Authors: Giuseppe Rosolini 

Publication date: 17 January 2017

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

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.

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

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

Mathematics Subject Classification ID

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

Cites Work

• Regular and exact completions
• Title not available (Why is that?)
• Tripos theory
• Title not available (Why is that?)
• Data Types as Lattices
• Title not available (Why is that?)
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Equilogical spaces
• A small complete category
• Some free constructions in realizability and proof theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Discrete Objects in the Effective Topos
• Title not available (Why is that?)
• Sobriety for equilogical spaces
• Colimit completions and the effective topos
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (4)

• Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
• Univalent polymorphism
• Categories of partial equivalence relations as localizations
• Homotopy theoretic models of identity types

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)