module Cat.Displayed.Instances.Simple
  {o ℓ} (B : Precategory o ℓ)
  (has-prods : ∀ X Y → Product B X Y)
  where

open Cat.Reasoning B
open Binary-products B has-prods

Simple fibrations🔗

One reason to be interested in fibrations is that they provide an excellent setting to study logical and type-theoretical phenomena. When constructing models of type theories, the general pattern is to construct a category of contexts and substitutions, and then to study types and terms as structures over this category. The language of displayed categories allows us to capture this situation quite succinctly by considering these extra pieces of equipment as being fibred over our category of contexts.

Focusing in, the language of simple fibrations provides us with enough structure to study simply-typed languages that have enough structure to represent contexts internally (i.e.: product types).

To start, we fix some base category with binary products. Intuitvely, this will be some sort of category of contexts, and context extension endows this category with products. We interpret a type in a context to be an object

Maps between types in contexts are then given by a map between contexts, and a map which is meant to denote a derivation of from

To encode this as a displayed category, we define the space of objects over some to be simply an object of This may seem odd, but recall that we are modeling a type theory with enough structure to consider contexts as types: if this is not the situation (IE: STLC without products), then we need to consider a more refined notion.

For the maps, we already have the map as the base morphism, so the displayed portion of the map will be the map between derivations. The identity morphism ignores the context, and derives by using the we already had, and is thus represented by the second projection

Composition of morphisms is somewhat more involved, but can be derived by playing type-tetris, as it’s all a matter of golfing the types and contexts into the correct place. The category laws are then a matter of bashing through a bunch of nested pairings and projections, and can be entirely automated.

Simple : Displayed B o ℓ
Simple .Displayed.Ob[_] Γ = Ob
Simple .Displayed.Hom[_] {Γ} {Δ} u X Y = Hom (Γ ⊗₀ X) Y
Simple .Displayed.Hom[_]-set _ _ _ = Hom-set (_ ⊗₀ _) _
Simple .Displayed.id' = π₂
Simple .Displayed._∘'_ {f = u} {g = v} f g = f ∘ ⟨ v ∘ π₁ , g ⟩
Simple .Displayed.idr' f =
  f ∘ ⟨ (id ∘ π₁) , π₂ ⟩ ≡⟨ products! B has-prods ⟩≡
  f                      ∎
Simple .Displayed.idl' {f = u} f =
  π₂ ∘ ⟨ u ∘ π₁ , f ⟩ ≡⟨ products! B has-prods ⟩≡
  f                   ∎
Simple .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 morphisms🔗

A morphism in the simple fibration is cartesian if and only if the morphism is invertible. This means that the cartesian morphisms are the isomorphisms of types, as we are interpreting morphisms in the simple fibration as derivations.

We begin with the reverse direction, as it is slightly simpler to show.

⟨⟩-invertible→cartesian
  : ∀ {Γ Δ x y} {f : Hom Γ Δ} {f' : Hom (Γ ⊗₀ x) y}
  → is-invertible ⟨ π₁ , f' ⟩
  → is-cartesian Simple f f'
⟨⟩-invertible→cartesian {Γ} {Δ} {x} {y} {f} {f'} ⟨⟩-inv = cart where
  module ⟨⟩-inv = is-invertible ⟨⟩-inv
  open is-cartesian

Let and be a pair of morphisms; we need to construct some that factorizes through

We begin by constructing the map which we can then pre-compose with the inverse to to obtain a map Finally, we can compose these two maps with the second projection, yielding the required map.

  cart : is-cartesian Simple f f'
  cart .universal m h' = π₂ ∘ ⟨⟩-inv.inv ∘ ⟨ m ∘ π₁ , h' ⟩

Showing that this map uniquely factorises boils down to pushing around products and using that fact that the inverse to is, in fact, an inverse.

  cart .commutes m h' =
    f' ∘ ⟨ m ∘ π₁ , π₂ ∘ ⟨⟩-inv.inv ∘ ⟨ m ∘ π₁ , h' ⟩ ⟩ ≡˘⟨ ap₂ _∘_ refl (⟨⟩-unique _ (pulll (π₁-inv ⟨⟩-inv) ∙ π₁∘⟨⟩) refl) ⟩≡˘
    f' ∘ ⟨⟩-inv.inv ∘ ⟨ m ∘ π₁ , h' ⟩                   ≡⟨ pulll (π₂-inv ⟨⟩-inv) ⟩≡
    π₂ ∘ ⟨ m ∘ π₁ , h' ⟩                                ≡⟨ π₂∘⟨⟩ ⟩≡
    h'                                                  ∎
  cart .unique {m = m} {h' = h'} m' p =
    m'                                                      ≡˘⟨ π₂∘⟨⟩ ⟩≡˘
    π₂ ∘ ⟨ m ∘ π₁ , m' ⟩                                    ≡⟨ ap₂ _∘_ refl (introl ⟨⟩-inv.invr) ⟩≡
    π₂ ∘ (⟨⟩-inv.inv ∘ ⟨ π₁ , f' ⟩) ∘ ⟨ m ∘ π₁ , m' ⟩       ≡⟨ products! B has-prods ⟩≡
    π₂ ∘ ⟨⟩-inv.inv ∘ ⟨ m ∘ π₁ , ⌜ f' ∘ ⟨ m ∘ π₁ , m' ⟩ ⌝ ⟩ ≡⟨ ap! p ⟩≡
    π₂ ∘ ⟨⟩-inv.inv ∘ ⟨ m ∘ π₁ , h' ⟩ ∎

On to the forward direction! Let and form a cartesian map in the simple fibration. We can construct an inverse to by factorizing the map as in the following diagram:

cartesian→⟨⟩-invertible
  : ∀ {Γ Δ x y} {f : Hom Γ Δ} {f' : Hom (Γ ⊗₀ x) y}
  → is-cartesian Simple f f'
  → is-invertible ⟨ π₁ , f' ⟩
cartesian→⟨⟩-invertible {Γ} {Δ} {x} {y} {f} {f'} cart =
  make-invertible ⟨ π₁ , universal id π₂ ⟩
    left-inv
    right-inv
    where
      open is-cartesian cart

Showing that this map is a left inverse can be seen by a short computation.

      left-inv : ⟨ π₁ , f' ⟩ ∘ ⟨ π₁ , universal id π₂ ⟩ ≡ id
      left-inv =
        ⟨ π₁ , f' ⟩ ∘ ⟨ π₁ , universal id π₂ ⟩           ≡⟨ products! B has-prods ⟩≡
        ⟨ π₁ , ⌜ f' ∘ ⟨ id ∘ π₁ ,  universal id π₂ ⟩ ⌝ ⟩ ≡⟨ ap! (commutes id π₂) ⟩≡
        ⟨ π₁ , π₂ ⟩                                      ≡⟨ ⟨⟩-η ⟩≡
        id                                               ∎

Showing that the constructed map is a right inverse is somewhat more involved. The key lemma is that is equal to To see this, consider the following diagram

Note that factorizes so it must be equal to the universal factorisation of as is cartesian. Furthermore, also factorizes which lets us see that

      universal-π₂-unique : f' ∘ ⟨ id ∘ π₁ , universal id π₂ ∘ ⟨ π₁ , f' ⟩ ⟩ ≡ f'
      universal-π₂-unique =
        f' ∘ ⟨ id ∘ π₁ , universal id π₂ ∘ ⟨ π₁ , f' ⟩ ⟩ ≡⟨ products! B has-prods ⟩≡
        f' ∘ ⟨ id ∘ π₁ , universal id π₂ ⟩ ∘ ⟨ π₁ , f' ⟩ ≡⟨ pulll (commutes id π₂) ⟩≡
        π₂ ∘ ⟨ π₁ , f' ⟩                                 ≡⟨ π₂∘⟨⟩ ⟩≡
        f'                                               ∎

      universal-π₂∘f' : universal id π₂ ∘ ⟨ π₁ , f' ⟩ ≡ π₂
      universal-π₂∘f' =
        universal id π₂ ∘ ⟨ π₁ , f' ⟩ ≡⟨ unique _ universal-π₂-unique ⟩≡
        universal id f'               ≡˘⟨ unique _ (elimr (ap₂ ⟨_,_⟩ (idl _) refl ∙ ⟨⟩-η)) ⟩≡˘
        π₂                            ∎

We can then apply this lemma to see that forms a right inverse.

      right-inv : ⟨ π₁ ,  universal id π₂ ⟩ ∘ ⟨ π₁ , f' ⟩ ≡ id
      right-inv =
        ⟨ π₁ , universal id π₂ ⟩ ∘ ⟨ π₁ , f' ⟩ ≡⟨ products! B has-prods ⟩≡
        ⟨ π₁ , universal id π₂ ∘ ⟨ π₁ , f' ⟩ ⟩ ≡⟨ ap₂ ⟨_,_⟩ refl universal-π₂∘f' ⟩≡
        ⟨ π₁ , π₂ ⟩                            ≡⟨ ⟨⟩-η ⟩≡
        id                                     ∎

Fibration structure🔗

As suggested by it’s name, the simple fibration is a fibration. given a map in the base, and a upstairs, we can construct a lift by selecting as the corner of the lift, and then using the second projection as the lift itself. Intuitively, this encodes a substitution of contexts: because we are working with a simple type theory, the substitutions don’t need to touch the types, as there are no possible dependencies!

Simple-fibration : Cartesian-fibration Simple
Simple-fibration .has-lift f Y .x' = Y
Simple-fibration .has-lift f Y .lifting = π₂
Simple-fibration .has-lift f Y .cartesian .universal _ h = h
Simple-fibration .has-lift f Y .cartesian .commutes g h = π₂∘⟨⟩
Simple-fibration .has-lift f Y .cartesian .unique {m = g} {h' = h} h' p =
  h'                   ≡˘⟨ π₂∘⟨⟩ ⟩≡˘
  π₂ ∘ ⟨ g ∘ π₁ , h' ⟩ ≡⟨ p ⟩≡
  h ∎

Comprehension structure🔗

The simple fibration admits a fibred functor into the codomain fibration that maps an object over to the projection

Simple→Slices
  : Vertical-functor Simple (Slices B)
Simple→Slices = func where
  open Vertical-functor
  open /-Obj
  open Slice-hom

  func : Vertical-functor _ _
  func .F₀' {x} x' = cut {domain = x ⊗₀ x'} π₁
  func .F₁' {f = f} f' = slice-hom ⟨ f ∘ π₁ , f' ⟩ (sym π₁∘⟨⟩)
  func .F-id' =
    Slice-path B $
    ⟨ id ∘ π₁ , π₂ ⟩ ≡⟨ ap₂ ⟨_,_⟩ (idl _) refl ∙ ⟨⟩-η ⟩≡
    id               ∎
  func .F-∘' {f = f} {g = g} {f' = f'} {g' = g'} =
    Slice-path B $
    ⟨ (f ∘ g) ∘ π₁ , f' ∘ ⟨ g ∘ π₁ , g' ⟩ ⟩ ≡⟨ products! B has-prods ⟩≡
    ⟨ f ∘ π₁ , f' ⟩ ∘ ⟨ g ∘ π₁ , g' ⟩       ∎

Furthermore, this functor is fibred. The general sketch is that cartesian morphisms in the codomain fibration are given by pullbacks, and cartesian maps in the simple fibration are given by inverses to and we can use this inverse to construct the universal map for the pullback.

Simple→Slices-fibred
  : is-vertical-fibred Simple→Slices
Simple→Slices-fibred {f = f} f' cart =
  pullback→cartesian B pb
  where
    open is-pullback

    ⟨⟩-inv : is-invertible ⟨ π₁ , f' ⟩
    ⟨⟩-inv = cartesian→⟨⟩-invertible cart

    module ⟨⟩-inv = is-invertible ⟨⟩-inv

    pb : is-pullback B π₁ f ⟨ f ∘ π₁ , f' ⟩ π₁
    pb .square = sym π₁∘⟨⟩
    pb .universal {P'} {p₁'} {p₂'} p =
      ⟨⟩-inv.inv ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩
Showing that this map is universal involves a series of somewhat tedious calculations, so we omit them.
    pb .p₁∘universal {P} {p₁'} {p₂'} {p} =
      π₁ ∘ ⟨⟩-inv.inv ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩ ≡⟨ pulll (π₁-inv ⟨⟩-inv) ⟩≡
      π₁ ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩              ≡⟨ π₁∘⟨⟩ ⟩≡
      p₁' ∎
    pb .p₂∘universal {P} {p₁'} {p₂'} {p} =
      ⟨ f ∘ π₁ , f' ⟩ ∘ ⟨⟩-inv.inv ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩                ≡⟨ pulll (⟨⟩∘ _) ⟩≡
      ⟨ (f ∘ π₁) ∘ ⟨⟩-inv.inv , f' ∘ ⟨⟩-inv.inv ⟩ ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩ ≡⟨ ap₂ _∘_ (ap₂ ⟨_,_⟩ (pullr (π₁-inv ⟨⟩-inv)) (π₂-inv ⟨⟩-inv)) refl ⟩≡
      ⟨ f ∘ π₁ , π₂ ⟩ ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩                             ≡⟨ products! B has-prods ⟩≡
      ⟨ f ∘ p₁' , π₂ ∘ p₂' ⟩                                           ≡⟨ ap₂ ⟨_,_⟩ p refl ⟩≡
      ⟨ π₁ ∘ p₂' , π₂ ∘ p₂' ⟩                                          ≡⟨ products! B has-prods ⟩≡
      p₂' ∎
    pb .unique {P} {p₁'} {p₂'} {p} {h'} q r =
      h'                                                   ≡⟨ insertl ⟨⟩-inv.invr ⟩≡
      ⟨⟩-inv.inv ∘ ⟨ π₁ , f' ⟩ ∘ h'                        ≡⟨ ap₂ _∘_ refl (⟨⟩∘ h') ⟩≡
      ⟨⟩-inv.inv ∘ ⟨ ⌜ π₁ ∘ h' ⌝ , f' ∘ h' ⟩               ≡⟨ ap! q ⟩≡
      ⟨⟩-inv.inv ∘ ⟨ p₁' , ⌜ f' ∘ h' ⌝ ⟩                   ≡⟨ ap! (pushl (sym π₂∘⟨⟩)) ⟩≡
      ⟨⟩-inv.inv ∘ ⟨ p₁' , π₂ ∘ ⌜ ⟨ f ∘ π₁ , f' ⟩ ∘ h' ⌝ ⟩ ≡⟨ ap! r ⟩≡
      ⟨⟩-inv.inv ∘ ⟨ p₁' , π₂ ∘ p₂' ⟩                      ∎

This yields a comprehension structure on the simple fibration, which encodes the structure of a non-dependent type theory.

Simple-comprehension : Comprehension Simple
Simple-comprehension .Vertical-fibred-functor.vert = Simple→Slices
Simple-comprehension .Vertical-fibred-functor.F-cartesian = Simple→Slices-fibred