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 / C.j. Cioffo ; coordinatore: V. Mastropietro ; supervisor: S. Mantovani ; co-supervisor: N. Gambino. - : . Dipartimento di Matematica Federigo Enriques, 2022 Jul 13. ((34. ciclo, Anno Accademico 2021.

HOMOTOPY SETOIDS AND GENERALIZED QUOTIENT COMPLETION

C.J. Cioffo
2022-07-13

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.
MANTOVANI, SANDRA
MASTROPIETRO, VIERI
Settore MAT/01 - Logica Matematica
Settore MAT/02 - Algebra
HOMOTOPY SETOIDS AND GENERALIZED QUOTIENT COMPLETION / C.j. Cioffo ; coordinatore: V. Mastropietro ; supervisor: S. Mantovani ; co-supervisor: N. Gambino. - : . Dipartimento di Matematica Federigo Enriques, 2022 Jul 13. ((34. ciclo, Anno Accademico 2021.
Doctoral Thesis
File in questo prodotto:
File Dimensione Formato  
phd_unimi_R12371.pdf

accesso aperto

Descrizione: PhD Thesis
Tipologia: Altro
Dimensione 1.63 MB
Formato Adobe PDF
1.63 MB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS 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: http://hdl.handle.net/2434/933293
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact