module Cat.Displayed.Comprehension {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ') where
open Cat.Reasoning B open Cat.Displayed.Reasoning E open Displayed E open Functor open _=>_ open Total-hom open /-Obj open Slice-hom
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 = 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 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
Other sources call such fibrations comprehension categories, but this is a bit of a misnomer, as they are structures on fibrations!↩︎