module Cat.Displayed.Comprehension
  {o  o' ℓ'} {B : Precategory o }
  (E : Displayed B o' ℓ')
  where

Comprehension categories🔗

Fibrations provide an excellent categorical framework for studying logic and type theory, as they give us the tools required to describe objects in a context, and substitutions between them. However, this framework is missing a key ingredient: we have no way to describe context extension!

Before giving a definition, it is worth pondering what context extension does. Consider some context Γ\Gamma, and type ΓA  type\Gamma \vdash A\; \mathrm{type}; context extension yields a new context Γ.A\Gamma.A extended with a fresh variable of type AA, along with a substitution π:Γ.AA\pi : \Gamma.A \to A that forgets this fresh variable.

We also have a notion of substitution extension: Given any substitution σ:ΓΔ\sigma : \Gamma \to \Delta, types ΓA  type\Gamma \vdash A\; \mathrm{type} and ΔB  type\Delta \vdash B\; \mathrm{type}, and term Γ.At:B[σ]\Gamma.A \vdash t : B[\sigma], there exists some substitution σ.t:Γ.AΔ.B\sigma. t : \Gamma.A \to \Delta.B such that the following square commutes.

Furthermore, when the term tt is simply a variable from Γ\Gamma, this square is a pullback square!

Now that we’ve got a general idea of how context extension ought to behave, we can begin to categorify. Our first step is to replace the category of contexts with an arbitrary category B\mathcal{B}, and the types with some fibration E\mathcal{E}. We can then encode context extension via a functor from E\mathcal{E} to the codomain fibration. This is a somewhat opaque definition, so it’s worth unfolding somewhat. Note that the action of such a functor on objects takes some object xx over Γ\Gamma in E\mathcal{E} to a pair of an object we will suggestively name Γ.A\Gamma.A in B\mathcal{B}, along with a map Γ.AΓ\Gamma.A \to \Gamma. Thus, the action on objects yields both the extended context and the projection substitution. If we inspect the action on morphisms of E\mathcal{E}, we see that it takes some map t:XσYt : X \to_{\sigma} Y over σ\sigma to a map σ.t\sigma.t in B\mathcal{B}, such that the following square commutes:

Note that this is the exact same square as above!

Furthermore, this functor ought to be fibred; this captures the situation where extending a substitution with a variable yields a pullback square.

We call such a fibred functor a comprehension structure on E\mathcal{E}1.

Comprehension : Type _
Comprehension = Vertical-fibred-functor E (Slices B)

Now, let’s make all that earlier intuition formal. Let E\mathcal{E} be a fibration, and PP be a comprehension structure on E\mathcal{E}. We begin by defining context extensions, along with their associated projections.

module Comprehension (fib : Cartesian-fibration E) (P : Comprehension) where opaque
  open Vertical-fibred-functor P
  open Cartesian-fibration fib

  _⨾_ :  Γ  Ob[ Γ ]  Ob
  Γ  x = F₀′ x .domain

  infixl 5 _⨾_

  _[_] :  {Γ Δ}  Ob[ Δ ]  Hom Γ Δ  Ob[ Γ ]
  x [ σ ] =  base-change E fib σ .F₀ x

  πᶜ :  {Γ x}  Hom (Γ  x) Γ
  πᶜ {x = x} = F₀′ x .map

As E\mathcal{E} is a fibration, we can reindex along the projection to obtain a notion of weakening.

  weaken :  {Γ}  (x : Ob[ Γ ])  Ob[ Γ ]  Ob[ Γ  x ]
  weaken x y = y [ πᶜ ]

Furthermore, if yy is an object over Γ\Gamma, then we have a map over πᶜ between from the weakened form of yy to yy.

  πᶜ′ :  {Γ} {x y : Ob[ Γ ]}  Hom[ πᶜ ] (weaken x y) y
  πᶜ′ = has-lift.lifting πᶜ _

  πᶜ′-cartesian :  {Γ x y}  is-cartesian E πᶜ (πᶜ′ {Γ} {x} {y})
  πᶜ′-cartesian = has-lift.cartesian πᶜ _

Next, we define extension of substitutions, and show that they commute with projections.

  _⨾ˢ_ :  {Γ Δ x y} (σ : Hom Γ Δ)  Hom[ σ ] x y  Hom (Γ  x) (Δ  y)
  σ ⨾ˢ f = F₁′ f .to

  infixl 5 _⨾ˢ_

  sub-proj :  {Γ Δ x y} {σ : Hom Γ Δ}  (f : Hom[ σ ] x y)  πᶜ  (σ ⨾ˢ f)  σ  πᶜ
  sub-proj f = sym $ F₁′ f .commute

Crucially, when ff is cartesian, then the above square is a pullback.

  sub-pullback
    :  {Γ Δ x y} {σ : Hom Γ Δ} {f : Hom[ σ ] x y}
     is-cartesian E σ f
     is-pullback B πᶜ σ (σ ⨾ˢ f) πᶜ
  sub-pullback {f = f} cart = cartesian→pullback B (F-cartesian f cart)

  module sub-pullback
    {Γ Δ x y} {σ : Hom Γ Δ} {f : Hom[ σ ] x y}
    (cart : is-cartesian E σ f)
    = is-pullback (sub-pullback cart)

We also obtain a map over σ.f\sigma.f between the weakenings of xx and yy, which also commutes with projections.

  _⨾ˢ′_
    :  {Γ Δ x y} (σ : Hom Γ Δ)  (f : Hom[ σ ] x y)
     Hom[ σ ⨾ˢ f ] (weaken x x) (weaken y y)
  σ ⨾ˢ′ f = has-lift.universal′ πᶜ _ (sub-proj f) (f ∘′ πᶜ′)

  infixl 5 _⨾ˢ′_

  sub-proj′
    :  {Γ Δ x y} {σ : Hom Γ Δ}  (f : Hom[ σ ] x y)
     πᶜ′ ∘′ (σ ⨾ˢ′ f) ≡[ sub-proj f ] f ∘′ πᶜ′
  sub-proj′ f = has-lift.commutesp πᶜ _ (sub-proj _) (f ∘′ πᶜ′)

If we extend the identity substitution with the identity morphism, we obtain the identity morphism.

  sub-id :  {Γ x}  id {Γ} ⨾ˢ id′ {Γ} {x}  id
  sub-id = ap to F-id′

  sub-id′ :  {Γ x}  (id ⨾ˢ′ id′) ≡[ sub-id {Γ} {x} ] id′
  sub-id′ = symP $ has-lift.uniquep πᶜ _ _ (symP sub-id) (sub-proj id′) id′ $
    idr′ _ ∙[] symP (idl′ _)

Furthermore, extending a substitution with a pair of composites is the same as composing the two extensions.

  sub-∘
    :  {Γ Δ Ψ x y z}
     {σ : Hom Δ Ψ} {δ : Hom Γ Δ} {f : Hom[ σ ] y z} {g : Hom[ δ ] x y}
     (σ  δ) ⨾ˢ (f ∘′ g)  (σ ⨾ˢ f)  (δ ⨾ˢ g)
  sub-∘ {σ = σ} {δ = δ} {f = f} {g = g} = ap to F-∘′

  sub-∘′
    :  {Γ Δ Ψ x y z}
     {σ : Hom Δ Ψ} {δ : Hom Γ Δ} {f : Hom[ σ ] y z} {g : Hom[ δ ] x y}
     ((σ  δ) ⨾ˢ′ (f ∘′ g)) ≡[ sub-∘ ] (σ ⨾ˢ′ f) ∘′ (δ ⨾ˢ′ g)
  sub-∘′ = symP $ has-lift.uniquep πᶜ _ _ (symP sub-∘) (sub-proj _) _ $
    pulll[] _ (sub-proj′ _)
    ∙[] extendr[] _ (sub-proj′ _)

We can also define the substitution Γ.AΓ.A.A\Gamma.A \to \Gamma.A.A that duplicates the variable AA via the following pullback square.

  δᶜ :  {Γ x}  Hom (Γ  x) (Γ  x  weaken x x)
  δᶜ = sub-pullback.universal (has-lift.cartesian πᶜ _) {p₁' = id} {p₂' = id} refl

This lets us easily show that applying projection after duplication is the identity.

  proj-dup :  {Γ x}  πᶜ  δᶜ {Γ} {x}  id
  proj-dup = sub-pullback.p₁∘universal (has-lift.cartesian πᶜ _)

  extend-proj-dup :  {Γ x}  (πᶜ ⨾ˢ πᶜ′)  δᶜ {Γ} {x}  id
  extend-proj-dup = sub-pullback.p₂∘universal (has-lift.cartesian πᶜ _)

We also obtain a substitution upstairs from the weakening of xx to the iterated weakening of xx.

  δᶜ′ :  {Γ} {x : Ob[ Γ ]}  Hom[ δᶜ ] (weaken x x) (weaken (weaken x x) (weaken x x))
  δᶜ′ = has-lift.universal′ πᶜ (weaken _ _) proj-dup id′

We also obtain similar lemmas detailing how duplication upstairs interacts with projection.

  proj-dup′ :  {Γ x}  πᶜ′ ∘′ δᶜ′ {Γ} {x} ≡[ proj-dup ] id′
  proj-dup′ = has-lift.commutesp πᶜ _ proj-dup _

  extend-proj-dup′ :  {Γ x}  (πᶜ ⨾ˢ′ πᶜ′) ∘′ δᶜ′ {Γ} {x} ≡[ extend-proj-dup ] id′
  extend-proj-dup′ = has-lift.uniquep₂ πᶜ _ _ _ _ _ _
    (pulll[] _ (sub-proj′ _) ∙[] cancelr[] _ proj-dup′)
    (idr′ _)

From this, we can conclude that δᶜ′ is cartesian. The factorisation of h:uΓ.x.xh' : u \to \Gamma.x.x is given by πh\pi \circ h'. This is universal, as δᶜ′ is given by the universal factorisation of π\pi.

  δᶜ′-cartesian :  {Γ x}  is-cartesian E (δᶜ {Γ} {x}) δᶜ′
  δᶜ′-cartesian = cart where
    open is-cartesian

    cart : is-cartesian E _ _
    cart .universal m h′ = hom[ cancell proj-dup ] (πᶜ′ ∘′ h′)
    cart .commutes m h′ = cast[] $
      unwrapr _
      ∙[] has-lift.uniquep₂ πᶜ _ _ (ap₂ _∘_ refl (cancell proj-dup)) refl _ _
        (cancell[] _ proj-dup′)
        refl
    cart .unique m′ p =
      has-lift.uniquep₂ πᶜ _ refl refl _ _ _
        refl
        (unwrapr _
        ∙[] ap₂ _∘′_ refl (ap₂ _∘′_ refl (sym p))
        ∙[] λ i  πᶜ′ ∘′ cancell[] _  proj-dup′ {f′ = m′} i)

We can also characterize how duplication interacts with extension.

  dup-extend
    :  {Γ Δ x y} {σ : Hom Γ Δ} {f : Hom[ σ ] x y}
     δᶜ  (σ ⨾ˢ f)  (σ ⨾ˢ f ⨾ˢ (σ ⨾ˢ′ f))  δᶜ
  dup-extend {σ = σ} {f = f} =
    sub-pullback.unique₂ (has-lift.cartesian πᶜ _)
      {p = refl}
      (cancell proj-dup )
      (cancell extend-proj-dup)
      (pulll (sub-proj _)
        cancelr proj-dup)
      (pulll (sym sub-∘  ap₂ _⨾ˢ_ (sub-proj _) (sub-proj′ _)  sub-∘)
        cancelr extend-proj-dup)

  dup-extend′
    :  {Γ Δ x y} {σ : Hom Γ Δ} {f : Hom[ σ ] x y}
     δᶜ′ ∘′ (σ ⨾ˢ′ f) ≡[ dup-extend ] (σ ⨾ˢ f ⨾ˢ′ (σ ⨾ˢ′ f)) ∘′ δᶜ′
  dup-extend′ {σ = σ} {f = f} =
    has-lift.uniquep₂ πᶜ _ _ _ _ _ _
      (cancell[] _ proj-dup′)
      (pulll[] _ (sub-proj′ (σ ⨾ˢ′ f)) ∙[] cancelr[] _ proj-dup′)
  extend-dup² :  {Γ x}  (δᶜ {Γ} {x} ⨾ˢ δᶜ′)  δᶜ  δᶜ  δᶜ
  extend-dup² =
    sub-pullback.unique₂ (has-lift.cartesian πᶜ _)
      {p = refl}
      (pulll (sub-proj _)  cancelr proj-dup)
      (cancell (sym sub-∘  ap₂ _⨾ˢ_ proj-dup proj-dup′  sub-id))
      (cancell proj-dup)
      (cancell extend-proj-dup)

  extend-dup²′ :  {Γ x}  (δᶜ {Γ} {x} ⨾ˢ′ δᶜ′) ∘′ δᶜ′ ≡[ extend-dup² ] δᶜ′ ∘′ δᶜ′
  extend-dup²′ = has-lift.uniquep₂ πᶜ
    _ _ _ _ _ _
    (pulll[] _ (sub-proj′ δᶜ′) ∙[] cancelr[] _ proj-dup′)
    (cancell[] _ proj-dup′)

Note that we can extend the operation of context extension to a functor from the total category of E\mathcal{E} to B\mathcal{B}, that takes every pair (Γ,A)(\Gamma, A) to Γ.A\Gamma.A

  Extend : Functor ( E) B
  Extend .F₀ (Γ , x) = Γ  x
  Extend .F₁ (total-hom σ f) = σ ⨾ˢ f
  Extend .F-id = ap to F-id′
  Extend .F-∘ f g = ap to F-∘′

There is also a natural transformation from this functor into the projection out of the total category of E\mathcal{E}, where each component of is a projection Γ.AΓ\Gamma.A \to \Gamma.

  proj : Extend => πᶠ E
  proj .η (Γ , x) = πᶜ
  proj .is-natural (Γ , x) (Δ , y) (total-hom σ f) =
    sub-proj f

Comprehension structures as Comonads🔗

Comprehension structures on fibrations E\mathcal{E} induce comonads on the total category of E\mathcal{E}. These comonads are particularly nice: all of the counits are cartesian morphisms, and every square of the following form is a pullback square, provided that ff is cartesian.

We call such comonads comprehension comonads.

record Comprehension-comonad : Type (o    o'  ℓ') where
  no-eta-equality
  field
    comonad : Comonad ( E)

  open Comonad comonad public

  field
    counit-cartesian
      :  {Γ x}  is-cartesian E (counit.ε (Γ , x) .hom) (counit.ε (Γ , x) .preserves)
    cartesian-pullback
      : (∀ {Γ Δ x y} {σ : Hom Γ Δ} {f : Hom[ σ ] x y}
       is-cartesian E σ f
       is-pullback ( E)
          (counit.ε (Γ , x)) (total-hom σ f)
          (W₁ (total-hom σ f)) (counit.ε (Δ , y)))

As promised, comprehension structures on E\mathcal{E} yield comprehension comonads.

Comprehension→comonad
  : Cartesian-fibration E
   Comprehension
   Comprehension-comonad
Comprehension→comonad fib P = comp-comonad where
  open Comprehension fib P
  open Comonad

We begin by constructing the endofunctor EE\int E \to \int E, which maps a pair Γ,X\Gamma, X to the extension Γ.X\Gamma.X, along with the weakening of XX.

  comonad : Comonad ( E)
  comonad .W .F₀ (Γ , x) =
    Γ  x , weaken x x
  comonad .W .F₁ (total-hom σ f) =
    total-hom (σ ⨾ˢ f) (σ ⨾ˢ′ f)
  comonad .W .F-id =
    total-hom-path E sub-id sub-id′
  comonad .W .F-∘ (total-hom σ f) (total-hom δ g) =
    total-hom-path E sub-∘ sub-∘′

The counit is given by the projection substitution, and comultiplication is given by duplication.

  comonad .counit .η (Γ , x) =
    total-hom πᶜ πᶜ′
  comonad .counit .is-natural (Γ , x) (Δ , g) (total-hom σ f) =
    total-hom-path E (sub-proj f) (sub-proj′ f)
  comonad .comult .η (Γ , x) =
    total-hom δᶜ δᶜ′
  comonad .comult .is-natural (Γ , x) (Δ , g) (total-hom σ f) =
    total-hom-path E dup-extend dup-extend′
  comonad .left-ident =
    total-hom-path E extend-proj-dup extend-proj-dup′
  comonad .right-ident =
    total-hom-path E proj-dup proj-dup′
  comonad .comult-assoc =
    total-hom-path E extend-dup² extend-dup²′

To see that this comonad is a comprehension comonad, note that the projection substitution is cartesian. Furthermore, we can construct a pullback square in the total category of E\mathcal{E} from one in the base, provided that two opposing sides are cartesian, which the projection morphism most certainly is!

  comp-comonad : Comprehension-comonad
  comp-comonad .Comprehension-comonad.comonad = comonad
  comp-comonad .Comprehension-comonad.counit-cartesian = πᶜ′-cartesian
  comp-comonad .Comprehension-comonad.cartesian-pullback cart =
    cartesian+pullback→total-pullback E
      πᶜ′-cartesian πᶜ′-cartesian
      (sub-pullback cart)
      (cast[] (symP (sub-proj′ _)))

We also show that comprehension comonads yield comprehension structures.

Comonad→comprehension
  : Cartesian-fibration E
   Comprehension-comonad
   Comprehension

We begin by constructing a vertical functor EB\mathcal{E} \to B^{\to} that maps an xx lying over Γ\Gamma to the base component of the counit ε:W(Γ,X)(Γ,X)\varepsilon : W(\Gamma, X) \to (\Gamma, X).

Comonad→comprehension fib comp-comonad = comprehend where
  open Comprehension-comonad comp-comonad
  open Vertical-functor
  open is-pullback

  vert : Vertical-functor E (Slices B)
  vert .F₀′ {Γ} x = cut (counit.ε (Γ , x) .hom)
  vert .F₁′ {f = σ} f =
    slice-hom (W₁ (total-hom σ f) .hom)
      (sym (ap hom (counit.is-natural _ _ _)))
  vert .F-id′ = Slice-path B (ap hom W-id)
  vert .F-∘′ = Slice-path B (ap hom (W-∘ _ _))

To see that this functor is fibred, recall that pullbacks in the codomain fibration are given by pullbacks. Furthermore, if we have a pullback square in the total category of E\mathcal{E} where two opposing sides are cartesian, then we have a corresponding pullback square in B\mathcal{B}. As the comonad is a comprehension comonad, counit is cartesian, which finishes off the proof.

  fibred : is-vertical-fibred vert
  fibred {f = σ} f cart =
    pullback→cartesian B $
    cartesian+total-pullback→pullback E fib
      counit-cartesian counit-cartesian
      (cartesian-pullback cart)

  comprehend : Comprehension
  comprehend .Vertical-fibred-functor.vert = vert
  comprehend .Vertical-fibred-functor.F-cartesian = fibred

  1. Other sources call such fibrations comprehension categories, but this is a bit of a misnomer, as they are structures on fibrations!↩︎