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

TL;DR

This paper demonstrates that the models of extensional type theory provided by equilogical spaces and the effective topos can be understood as homotopical quotients of categories of 2-groupoids, linking type theory with higher category theory.

Contribution

It establishes a novel connection between models of type theory and homotopical quotients of 2-groupoid categories, providing new insights into their structural foundations.

Findings

Equilogical spaces model as homotopical quotients of 2-groupoids

Effective topos as a homotopical quotient of 2-groupoids

Bridges type theory models with higher categorical structures

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.