Denotational semantics of type theories provide a framework for understanding and reasoning about type theories and the behaviour of programs and proofs. In particular, it is important to study what can and can not be proved within Martin-Löf Type Theory (MLTT) as it is the basis of proof assistants like Agda, Lean and Coq. Many models, including a certain class of comprehension categories, full and split comprehension categories, have been studied for the semantics of dependent type theories. The motivation for this work comes from the fact that not all comprehension categories are full and split, and one expects that type theories more general than MLTT can be interpreted in a comprehension category which is not full and split.

In this thesis, we first study how MLTT is interpreted in full split comprehension categories through concrete examples. Next, we investigate type theories that can be interpreted in comprehension cat- egories which are not necessarily full and split. For this, we propose a candidate type theory for the internal language of comprehension categories by extracting a type theory from the semantics given by a general comprehension category which is not full and split. We also give an interpretation of this type theory in every comprehension category.

The goal of this paper is to formalize the Fundamental Group of the Circle within Coq and the Unimath library, as described in the paper by Mr Licata and Mr Shulman, and show it is isomorphic to Z. Fundamental groups are a powerful algebraic invariant for studying Homotopy theory, and provide deep, yet concise insights into the fundamental properties of a space.