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.
13-lug-2022
Inglese
MANTOVANI, SANDRA
MASTROPIETRO, VIERI
Università degli Studi di Milano
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.14242/81387
Il codice NBN di questa tesi è URN:NBN:IT:UNIMI-81387