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
- 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497).