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

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.