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 and type context extension yields a new context extended with a fresh variable of type along with a substitution that forgets this fresh variable.

We also have a notion of substitution extension: Given any substitution types and and term there exists some substitution such that the following square commutes.

Furthermore, when the term is simply a variable from 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 and the types with some fibration We can then encode context extension via a functor from 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 over in to a pair of an object we will suggestively name in along with a map Thus, the action on objects yields both the extended context and the projection substitution. If we inspect the action on morphisms of we see that it takes some map over to a map in 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 1.

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

Now, letโ€™s make all that earlier intuition formal. Let be a fibration, and be a comprehension structure on 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 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 is an object over then we have a map over ฯ€แถœ between from the weakened form of to

  ฯ€แถœ' : โˆ€ {ฮ“} {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 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 between the weakenings of and 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 that duplicates the variable 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 to the iterated weakening of

  ฮดแถœ' : โˆ€ {ฮ“} {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 is given by This is universal, as ฮดแถœ' is given by the universal factorisation of

  ฮดแถœ'-cartesian : โˆ€ {ฮ“ x} โ†’ is-cartesian E (ฮดแถœ {ฮ“} {x}) ฮดแถœ'
  ฮดแถœ'-cartesian {ฮ“ = ฮ“} {x = x} = cart where
    open is-cartesian

    cart : is-cartesian E (ฮดแถœ {ฮ“} {x}) ฮดแถœ'
    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 to that takes every pair to

  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 where each component of is a projection

  proj : Extend => ฯ€แถ E
  proj .ฮท (ฮ“ , x) = ฯ€แถœ
  proj .is-natural (ฮ“ , x) (ฮ” , y) (total-hom ฯƒ f) =
    sub-proj f

Comprehension structures as comonads๐Ÿ”—

Comprehension structures on fibrations induce comonads on the total category of 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 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 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 which maps a pair to the extension along with the weakening of

  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 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 that maps an lying over to the base component of the counit

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 where two opposing sides are cartesian, then we have a corresponding pullback square in 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!โ†ฉ๏ธŽ