This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Type theories

{-# OPTIONS --guardedness #-}

Files in the type theories folder

module type-theories where

open import type-theories.comprehension-type-theories public
open import type-theories.dependent-type-theories public
open import type-theories.fibered-dependent-type-theories public
open import type-theories.pi-types-precategories-with-attributes public
open import type-theories.pi-types-precategories-with-families public
open import type-theories.precategories-with-attributes public
open import type-theories.precategories-with-families public
open import type-theories.sections-dependent-type-theories public
open import type-theories.simple-type-theories public
open import type-theories.unityped-type-theories public