module Cat.Displayed.Instances.CT-Structure
  {o β„“} (B : Precategory o β„“)
  (has-prods : βˆ€ X Y β†’ Product B X Y)
  where

open Precategory B
open Binary-products B has-prods
open Simple B has-prods

CT structuresπŸ”—

CT-Structures are a refinement of simple fibrations, which allow us to model type theories where the contexts aren’t necessarily representable as types. This is done by defining a CT-Structure (short for Context and Type Structure) on our category of contexts, which allows us to distinguish certain contexts as denoting types (for instance, singleton contexts, or possibly the empty context if we have unit types). A CT-structure is quite simple, consisting of only a predicate on contexts meant to denote which ones are types, along with the restriction that there is at least one type, to prevent the entire structure from becoming degenerate.

record CT-Structure (s : Level) : Type (o βŠ” lsuc s) where
  field
    is-tp : Ob β†’ Prop s
    βˆƒ-tp  : βˆƒ[ tp ∈ Ob ] (tp ∈ is-tp)

open CT-Structure

We can construct a displayed category over our category of contexts in much the same manner as the simple fibration; the only difference is that we restrict the displayed object to objects that the CT-structure distinguishes as types.

Simple-ct : βˆ€ {s} β†’ CT-Structure s β†’ Displayed B (o βŠ” s) β„“
Simple-ct ct .Displayed.Ob[_] Ξ“ = Ξ£[ X ∈ Ob ] ∣ is-tp ct X ∣
Simple-ct ct .Displayed.Hom[_] {Ξ“} {Ξ”} u X Y = Hom (Ξ“ βŠ—β‚€ X .fst) (Y .fst)
Simple-ct ct .Displayed.Hom[_]-set {Ξ“} {Ξ”} u X Y = Hom-set (Ξ“ βŠ—β‚€ X .fst) (Y .fst)
Simple-ct ct .Displayed.id' = Ο€β‚‚
Simple-ct ct .Displayed._∘'_ {f = u} {g = v} f g = f ∘ ⟨ v ∘ π₁ , g ⟩
Simple-ct ct .Displayed.idr' {f = u} f =
  f ∘ ⟨ (id ∘ π₁) , Ο€β‚‚ ⟩ β‰‘βŸ¨ products! B has-prods βŸ©β‰‘
  f                      ∎
Simple-ct ct .Displayed.idl' {f = u} f =
  Ο€β‚‚ ∘ ⟨ u ∘ π₁ , f ⟩ β‰‘βŸ¨ products! B has-prods βŸ©β‰‘
  f                   ∎
Simple-ct ct .Displayed.assoc' {f = u} {g = v} {h = w} f g h =
  f ∘ ⟨ (v ∘ w) ∘ π₁ , g ∘ ⟨ w ∘ π₁ , h ⟩ ⟩ β‰‘βŸ¨ products! B has-prods βŸ©β‰‘
  (f ∘ ⟨ v ∘ π₁ , g ⟩) ∘ ⟨ w ∘ π₁ , h ⟩     ∎

Cartesian mapsπŸ”—

If a map is cartesian in the simple fibration, then it is cartesian in a simple CT fibration.

Simple-cartesian→Simple-ct-cartesian
  : βˆ€ {s} {Ξ“ Ξ” x y} {Οƒ : Hom Ξ“ Ξ”} {f : Hom (Ξ“ βŠ—β‚€ x) y}
  β†’ (ct : CT-Structure s)
  β†’ (x-tp : x ∈ ct .is-tp) β†’ (y-tp : y ∈ ct .is-tp)
  β†’ is-cartesian Simple Οƒ f
  β†’ is-cartesian (Simple-ct ct) {a' = x , x-tp} {b' = y , y-tp} Οƒ f
Simple-cartesian→Simple-ct-cartesian ct x-tp y-tp cart = ct-cart where
  open is-cartesian

  ct-cart : is-cartesian (Simple-ct ct) _ _
  ct-cart .universal = cart .universal
  ct-cart .commutes = cart .commutes
  ct-cart .unique = cart .unique

Fibration structureπŸ”—

Much like the simple fibration, the simple fibration associated to a CT-structure also deserves its name.

open Cartesian-fibration
open Cartesian-lift
open is-cartesian

Simple-ct-fibration : βˆ€ {s} (ct : CT-Structure s) β†’ Cartesian-fibration (Simple-ct ct)
Simple-ct-fibration ct .has-lift u Y .x' = Y
Simple-ct-fibration ct .has-lift u Y .lifting = Ο€β‚‚
Simple-ct-fibration ct .has-lift u Y .cartesian .universal _ h = h
Simple-ct-fibration ct .has-lift u Y .cartesian .commutes g h = Ο€β‚‚βˆ˜βŸ¨βŸ©
Simple-ct-fibration ct .has-lift u Y .cartesian .unique {m = g} {h' = h} h' p =
  h'                   β‰‘Λ˜βŸ¨ Ο€β‚‚βˆ˜βŸ¨βŸ© βŸ©β‰‘Λ˜
  Ο€β‚‚ ∘ ⟨ g ∘ π₁ , h' ⟩ β‰‘βŸ¨ p βŸ©β‰‘
  h ∎

EmbeddingsπŸ”—

There is an evident embedding of the simple fibration associated with a CT-structure into the simple fibration.

Simple-ct→Simple
  : βˆ€ {s} β†’ (ct : CT-Structure s)
  β†’ Vertical-functor (Simple-ct ct) Simple
Simple-ct→Simple ct .Vertical-functor.F₀' = fst
Simple-ctβ†’Simple ct .Vertical-functor.F₁' f = f
Simple-ct→Simple ct .Vertical-functor.F-id' = refl
Simple-ctβ†’Simple ct .Vertical-functor.F-∘' = refl

Furthermore, if is (merely) inhabited, then we can construct a CT-Structure that considers every context a type.

All-types : βˆ₯ Ob βˆ₯ β†’ CT-Structure lzero
All-types X .is-tp _ = el ⊀ (hlevel 1)
All-types X .βˆƒ-tp = βˆ₯-βˆ₯-map (Ξ» x β†’ x , tt) X

Simpleβ†’Simple-ct : βˆ€ {X} β†’ Vertical-functor Simple (Simple-ct (All-types X))
Simple→Simple-ct .Vertical-functor.F₀' X = X , tt
Simpleβ†’Simple-ct .Vertical-functor.F₁' f = f
Simple→Simple-ct .Vertical-functor.F-id' = refl
Simpleβ†’Simple-ct .Vertical-functor.F-∘' = refl