In this thesis, we deal with some categorical structures arising from the Martin-Löf Intuitionistic Type Theory. In the first part, we introduce the homotopy setoids, considering ideas from the homotopy type theory, and we study their categorical properties. In order to do that, we use the categorical framework of the elementary doctrines introduced by Maietti and Rosolini. In this setting, we provide some results about the elementary quotient completion and we prove that homotopy setoids form a weak notion of pretopos. In the second part of this thesis, we introduce the notion of biased elementary doctrine which generalizes the one of elementary doctrine. For this framework we provide a generalized notion of quotient completion and we obtain as particular instances both the theory of the exact completion and of the elementary quotient completion. In the last part of the thesis, we develop a categorical semantic for fragments of intuitionistic first order logic that generalizes the categorical Brouwer-Heyting-Kolmogorv interpretation. Our result is suitable for a larger class of categories.
HOMOTOPY SETOIDS AND GENERALIZED QUOTIENT COMPLETION
CIOFFO, CIPRIANO JUNIOR
2022
Abstract
In this thesis, we deal with some categorical structures arising from the Martin-Löf Intuitionistic Type Theory. In the first part, we introduce the homotopy setoids, considering ideas from the homotopy type theory, and we study their categorical properties. In order to do that, we use the categorical framework of the elementary doctrines introduced by Maietti and Rosolini. In this setting, we provide some results about the elementary quotient completion and we prove that homotopy setoids form a weak notion of pretopos. In the second part of this thesis, we introduce the notion of biased elementary doctrine which generalizes the one of elementary doctrine. For this framework we provide a generalized notion of quotient completion and we obtain as particular instances both the theory of the exact completion and of the elementary quotient completion. In the last part of the thesis, we develop a categorical semantic for fragments of intuitionistic first order logic that generalizes the categorical Brouwer-Heyting-Kolmogorv interpretation. Our result is suitable for a larger class of categories.File | Dimensione | Formato | |
---|---|---|---|
phd_unimi_R12371.pdf
accesso aperto
Dimensione
1.63 MB
Formato
Adobe PDF
|
1.63 MB | Adobe PDF | Visualizza/Apri |
I documenti in UNITESI sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/20.500.14242/81387
URN:NBN:IT:UNIMI-81387