open import Cat.Displayed.Instances.Slice
open import Cat.Displayed.Comprehension
open import Cat.Diagram.Product.Solver
open import Cat.Displayed.Cartesian
open import Cat.Displayed.Functor
open import Cat.Diagram.Pullback
open import Cat.Diagram.Product
open import Cat.Instances.Slice
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Reasoning

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 $\mathcal{B}$ 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 $\Gamma \times X:\mathcal{B}\text{.}$

Maps between types in contexts $(\Gamma \times X)\to (\Delta \times Y)$ are then given by a map $\Gamma \to \Delta$ between contexts, and a map $\Gamma \times X\to Y\text{,}$ which is meant to denote a derivation of $Y$ from $\Gamma \times X\text{.}$

To encode this as a displayed category, we define the space of objects over some $\Gamma$ to be simply an object of $B\text{.}$ 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 $\Gamma \to \Delta$ as the base morphism, so the displayed portion of the map will be the map $\Gamma \times X\to Y$ between derivations. The identity morphism $id:\Gamma \times Y\to Y$ ignores the context, and derives $Y$ by using the $Y$ we already had, and is thus represented by the second projection ${\pi }_2\text{.}$

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 $f^{\prime }:\Gamma \times X\to Y$ in the simple fibration is cartesian if and only if the morphism $⟨{\pi }_1,f^{\prime }⟩:\Gamma \times X\to \Gamma \times Y$ 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 $m:\Psi \to \Gamma \text{,}$ and $h^{\prime }:\Psi \times Z\to Y$ be a pair of morphisms; we need to construct some $m^{\prime }:\Psi \times Z\to X$ that factorizes $h^{\prime }$ through $f^{\prime }\text{.}$

We begin by constructing the map $⟨m\circ {\pi }_1,h^{\prime }⟩:\Psi \times Z\to \Gamma \times Y\text{,}$ which we can then pre-compose with the inverse to $⟨{\pi }_1,f^{\prime }⟩$ to obtain a map $\Psi \times Z\to \Gamma \times X\text{.}$ 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 $f^{\prime }$ boils down to pushing around products and using that fact that the inverse to $⟨{\pi }_1,f^{\prime }⟩$ 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 $f:\Gamma \to \Delta$ and $f^{\prime }:\Gamma \times X\to Y$ form a cartesian map in the simple fibration. We can construct an inverse to $⟨{\pi }_1,f^{\prime }⟩$ by factorizing the map ${\pi }_2:\Gamma \times Y\to Y\text{,}$ 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 $i\circ ⟨{\pi }_1,f^{\prime }⟩:\Gamma \times X\to X$ is equal to ${\pi }_2\text{.}$ To see this, consider the following diagram

Note that ${\pi }_2$ factorizes $f^{\prime }\text{,}$ so it must be equal to the universal factorisation of $f^{\prime }\text{,}$ as $f^{\prime }$ is cartesian. Furthermore, $i\circ ⟨{\pi }_1,f^{\prime }⟩$ also factorizes $f^{\prime }\text{,}$ which lets us see that $i\circ ⟨{\pi }_1,f^{\prime }⟩={\pi }_2\text{.}$

      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 $⟨{\pi }_1,i⟩$ 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 $\Gamma \to Delta$ in the base, and a $(\Delta ,Y)$ upstairs, we can construct a lift by selecting $(\Gamma ,Y)$ 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!

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

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 $X$ over $\Gamma$ to the projection ${\pi }_1:\Gamma \times X\to \Gamma \text{.}$

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 $⟨{\pi }_1,f^{\prime }⟩\text{,}$ 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₂' ⟩

    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