Comprehension of fibered type theories

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-04-14.
Last modified on 2023-06-07.

{-# OPTIONS --guardedness #-}

module type-theories.comprehension-type-theories where
Imports 




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 : {!!}
-}



Recent changes