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

Comprehension of fibered type theories

{-# OPTIONS --guardedness #-}

module type-theories.comprehension-type-theories where

Idea

Given a fibered type theory S over T, we can form the comprehension type theory ∫ST analogous to the Grothendieck construction.

Definition

{-
record comprehension
  {l1 l2 l3 l4 : Level} {A : type-theory l1 l2}
  {B : fibered.fibered-type-theory l3 l4 A} : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  where
  coinductive
  field
    type : {!!}
    element : {!!}
    slice : {!!}
-}