Type theories

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Daniel Gratzer and Elisabeth Stenholm.

Created on 2022-04-14.
Last modified on 2024-09-23.

{-# OPTIONS --guardedness #-}

Modules in the type theories namespace

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

Recent changes

• 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
• 2023-11-27. Elisabeth Stenholm, Daniel Gratzer and Egbert Rijke. Additions during work on material set theory in HoTT (#910).
• 2023-05-06. Egbert Rijke. Collecting some easily defined precategories (#598).
• 2023-03-12. Fredrik Bakke and Jonathan Prieto-Cubides. Generate module indexes (#501).
• 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).