HOMOTOPY SETOIDS AND GENERALIZED QUOTIENT COMPLETION

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.