We show that the two models of an extensional version of Martin-Löf type theory, those given by the category of equilogical spaces and by the effective topos, are homotopical quotients of appropriate categories of 2-groupoids.
The category of equilogical spaces and the effective topos as homotopical quotients
ROSOLINI, GIUSEPPE
2016-01-01
Abstract
We show that the two models of an extensional version of Martin-Löf type theory, those given by the category of equilogical spaces and by the effective topos, are homotopical quotients of appropriate categories of 2-groupoids.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
