open import Cat.Displayed.Base open import Cat.Prelude import Cat.Reasoning import Cat.Displayed.Morphism import Cat.Displayed.Reasoning as DR module Cat.Displayed.Cartesian {o ℓ o′ ℓ′} {B : Precategory o ℓ} (E : Displayed B o′ ℓ′) where open Cat.Reasoning B open Displayed E open Cat.Displayed.Morphism E open DR E
Cartesian morphisms and Fibrations🔗
While displayed categories give the essential framework we need to express the idea of families of categories indexed by a category, they do not quite capture the concept precisely. The problem is that while a category displayed over does indeed give a collection of fibre categories , this assignment isn’t necessarily functorial!
More precisely, we should have that a collection of categories, indexed by a category, should be a pseudofunctor , where is a bicategory of categories. It turns out that we can characterise this assignment entirely in terms of the displayed objects and morphisms in !
Fix an arrow in the base category , an object over (resp. over ), and an arrow over . We say that is cartesian if, up to very strong handwaving, it fits into a “pullback diagram”. The barred arrows with triangle tips here indicate the “projection” from a displayed object to its base, and so are implicit in the type dependency.
record is-cartesian {a b a′ b′} (f : Hom a b) (f′ : Hom[ f ] a′ b′) : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where no-eta-equality
More specifically, let and be over , and suppose that we have a map (below, in violet), and a map lying over the composite (in red). The universal property of a Cartesian map says that we have a universal factorisation of through a map (in green, marked ).
field universal : ∀ {u u′} (m : Hom u a) (h′ : Hom[ f ∘ m ] u′ b′) → Hom[ m ] u′ a′ commutes : ∀ {u u′} (m : Hom u a) (h′ : Hom[ f ∘ m ] u′ b′) → f′ ∘′ universal m h′ ≡ h′ unique : ∀ {u u′} {m : Hom u a} {h′ : Hom[ f ∘ m ] u′ b′} → (m′ : Hom[ m ] u′ a′) → f′ ∘′ m′ ≡ h′ → m′ ≡ universal m h′
Given a “right corner” like that of the diagram below, and note that the input data consists of , , and over ,
We also provide some helper functions for working with morphisms that are displayed over something that is propositionally equal to a composite, rather than displayed directly over a composite.
universal′ : ∀ {u u′} {m : Hom u a} {k : Hom u b} → (p : f ∘ m ≡ k) (h′ : Hom[ k ] u′ b′) → Hom[ m ] u′ a′ universal′ {u′ = u′} p h′ = universal _ (coe1→0 (λ i → Hom[ p i ] u′ b′) h′) commutesp : ∀ {u u′} {m : Hom u a} {k : Hom u b} → (p : f ∘ m ≡ k) (h′ : Hom[ k ] u′ b′) → f′ ∘′ universal′ p h′ ≡[ p ] h′ commutesp {u′ = u′} p h′ = to-pathp⁻ $ commutes _ (coe1→0 (λ i → Hom[ p i ] u′ b′) h′) universalp : ∀ {u u′} {m₁ m₂ : Hom u a} {k : Hom u b} → (p : f ∘ m₁ ≡ k) (q : m₁ ≡ m₂) (r : f ∘ m₂ ≡ k) → (h′ : Hom[ k ] u′ b′) → universal′ p h′ ≡[ q ] universal′ r h′ universalp {u = u} p q r h′ i = universal′ (is-set→squarep (λ _ _ → Hom-set u b) (ap (f ∘_) q) p r refl i) h′ uniquep : ∀ {u u′} {m₁ m₂ : Hom u a} {k : Hom u b} → (p : f ∘ m₁ ≡ k) (q : m₁ ≡ m₂) (r : f ∘ m₂ ≡ k) → {h′ : Hom[ k ] u′ b′} → (m′ : Hom[ m₁ ] u′ a′) → f′ ∘′ m′ ≡[ p ] h′ → m′ ≡[ q ] universal′ r h′ uniquep p q r {h′ = h′} m′ s = to-pathp⁻ (unique m′ (from-pathp⁻ s) ∙ from-pathp⁻ (universalp p q r h′)) uniquep₂ : ∀ {u u′} {m₁ m₂ : Hom u a} {k : Hom u b} → (p : f ∘ m₁ ≡ k) (q : m₁ ≡ m₂) (r : f ∘ m₂ ≡ k) → {h′ : Hom[ k ] u′ b′} (m₁′ : Hom[ m₁ ] u′ a′) (m₂′ : Hom[ m₂ ] u′ a′) → f′ ∘′ m₁′ ≡[ p ] h′ → f′ ∘′ m₂′ ≡[ r ] h′ → m₁′ ≡[ q ] m₂′ uniquep₂ {u′ = u′} p q r m₁′ m₂′ α β = to-pathp⁻ $ unique m₁′ (from-pathp⁻ α) ·· from-pathp⁻ (universalp p q r _) ·· ap (coe1→0 (λ i → Hom[ q i ] u′ a′)) (sym (unique m₂′ (from-pathp⁻ β)))
Properties of Cartesian Morphisms🔗
The composite of 2 cartesian morphisms is in turn cartesian.
cartesian-∘ : ∀ {x y z} {f : Hom y z} {g : Hom x y} → ∀ {x′ y′ z′} {f′ : Hom[ f ] y′ z′} {g′ : Hom[ g ] x′ y′} → is-cartesian f f′ → is-cartesian g g′ → is-cartesian (f ∘ g) (f′ ∘′ g′) cartesian-∘ {f = f} {g = g} {f′ = f′} {g′ = g′} f-cart g-cart = fg-cart where module f′ = is-cartesian f-cart module g′ = is-cartesian g-cart fg-cart : is-cartesian (f ∘ g) (f′ ∘′ g′) fg-cart .is-cartesian.universal m h′ = g′.universal m (f′.universal′ (assoc f g m) h′) fg-cart .is-cartesian.commutes m h′ = (f′ ∘′ g′) ∘′ g′.universal m (f′.universal′ (assoc f g m) h′) ≡⟨ shiftr (sym $ assoc _ _ _) (pullr′ refl (g′.commutes m _)) ⟩≡ hom[] (f′ ∘′ f′.universal′ (assoc f g m) h′) ≡⟨ hom[]⟩⟨ f′.commutes _ _ ⟩≡ hom[] (hom[] h′) ≡⟨ hom[]-∙ _ _ ∙ liberate _ ⟩≡ h′ ∎ fg-cart .is-cartesian.unique {m = m} {h′ = h′} m′ p = g′.unique m′ $ f′.unique (g′ ∘′ m′) $ f′ ∘′ g′ ∘′ m′ ≡⟨ from-pathp⁻ (assoc′ f′ g′ m′) ⟩≡ hom[] ((f′ ∘′ g′) ∘′ m′) ≡⟨ weave _ _ _ p ⟩≡ hom[] h′ ∎
Furthermore, the identity morphism is cartesian.
cartesian-id : ∀ {x x′} → is-cartesian id (id′ {x} {x′}) cartesian-id .is-cartesian.universal m h′ = hom[ idl m ] h′ cartesian-id .is-cartesian.commutes m h′ = from-pathp⁻ (idl′ _) ∙ hom[]-∙ _ _ ∙ liberate _ cartesian-id .is-cartesian.unique m′ p = from-pathp⁻ (symP $ idl′ _) ∙ weave _ _ _ p
In fact, every invertible map is also cartesian, as we can use the inverse to construct the requisite factorization.
invertible→cartesian : ∀ {x y} {f : Hom x y} {x′ y′} {f′ : Hom[ f ] x′ y′} → (f-inv : is-invertible f) → is-invertible[ f-inv ] f′ → is-cartesian f f′ invertible→cartesian {f = f} {f′ = f′} f-inv f′-inv = f-cart where module f-inv = is-invertible f-inv module f′-inv = is-invertible[_] f′-inv f-cart : is-cartesian f f′ f-cart .is-cartesian.universal m h′ = hom[ cancell f-inv.invr ] (f′-inv.inv′ ∘′ h′) f-cart .is-cartesian.commutes m h′ = f′ ∘′ hom[ cancell f-inv.invr ] (f′-inv.inv′ ∘′ h′) ≡⟨ whisker-r _ ⟩≡ hom[] (f′ ∘′ f′-inv.inv′ ∘′ h′) ≡⟨ revive₁ (cancell′ f-inv.invl f′-inv.invl′ {q = cancell f-inv.invl}) ⟩≡ hom[] h′ ≡⟨ liberate _ ⟩≡ h′ ∎ f-cart .is-cartesian.unique {h′ = h′} m′ p = m′ ≡˘⟨ liberate _ ⟩≡˘ hom[] m′ ≡⟨ weave refl (insertl f-inv.invr) (cancell f-inv.invr) (insertl′ _ f′-inv.invr′) ⟩≡ hom[] (f′-inv.inv′ ∘′ f′ ∘′ m′) ≡⟨ apr′ p ⟩≡ hom[] (f′-inv.inv′ ∘′ h′) ∎
If is cartesian, it’s also a [weak monomorphism]. [weak monomorphism]: Cat.Displayed.Morphism.html#weak-monos
cartesian→weak-monic : ∀ {x y} {f : Hom x y} → ∀ {x′ y′} {f′ : Hom[ f ] x′ y′} → is-cartesian f f′ → is-weak-monic f′ cartesian→weak-monic {f′ = f′} f-cart g′ g″ p = g′ ≡⟨ unique g′ p ⟩≡ universal _ (f′ ∘′ g″) ≡˘⟨ unique g″ refl ⟩≡˘ g″ ∎ where open is-cartesian f-cart
We can use this fact to show that 2 cartesian lifts over the same morphisms must have their domains related by a vertical isomorphism. Suppose they’re called and , and fit into a diagram like the one below.
Since and are both Cartesian morphisms, we can factor through by a map , and conversely, through by , so that we have , and is a factorisation of through , its own domain; but, of course, also factors through its own domain by the identity map! Since is Cartesian, these factorisations must be the same, hence . A symmetric argument shows that is also the identity, so .
cartesian-domain-unique : ∀ {x y} {f : Hom x y} → ∀ {x′ x″ y′} {f′ : Hom[ f ] x′ y′} {f″ : Hom[ f ] x″ y′} → is-cartesian f f′ → is-cartesian f f″ → x′ ≅↓ x″ cartesian-domain-unique {f′ = f′} {f″ = f″} f′-cart f″-cart = make-iso[ id-iso ] to* from* invl* invr* where open is-cartesian to* = universal′ f″-cart (B .Precategory.idr _) f′ from* = universal′ f′-cart (B .Precategory.idr _) f″ invl* : to* ∘′ from* ≡[ idl id ] id′ invl* = to-pathp⁻ $ cartesian→weak-monic f″-cart _ _ $ f″ ∘′ to* ∘′ from* ≡⟨ shiftr (assoc _ _ _) (pulll′ _ (f″-cart .commutes _ _)) ⟩≡ hom[] (hom[] f′ ∘′ from*) ≡⟨ smashl _ _ ⟩≡ hom[] (f′ ∘′ from*) ≡⟨ (hom[]⟩⟨ f′-cart .commutes _ _) ∙ hom[]-∙ _ _ ⟩≡ hom[] f″ ≡⟨ weave _ (sym $ idr _) (ap (_ ∘_) (sym $ idl _)) (symP $ idr′ f″) ⟩≡ hom[] (f″ ∘′ id′) ≡˘⟨ whisker-r _ ⟩≡˘ f″ ∘′ hom[] id′ ∎ invr* : from* ∘′ to* ≡[ idl id ] id′ invr* = to-pathp⁻ $ cartesian→weak-monic f′-cart _ _ $ f′ ∘′ from* ∘′ to* ≡⟨ shiftr (assoc _ _ _) (pulll′ _ (f′-cart .commutes _ _)) ⟩≡ hom[] (hom[] f″ ∘′ to*) ≡⟨ smashl _ _ ⟩≡ hom[] (f″ ∘′ to*) ≡⟨ (hom[]⟩⟨ f″-cart .commutes _ _) ∙ hom[]-∙ _ _ ⟩≡ hom[] f′ ≡⟨ weave _ (sym $ idr _) (ap (_ ∘_) (sym $ idl _)) (symP $ idr′ f′) ⟩≡ hom[] (f′ ∘′ id′) ≡˘⟨ whisker-r _ ⟩≡˘ f′ ∘′ hom[] id′ ∎
Cartesian morphisms are also stable under vertical retractions.
cartesian-vertical-retraction-stable : ∀ {x y} {f : Hom x y} → ∀ {x′ x″ y′} {f′ : Hom[ f ] x′ y′} {f″ : Hom[ f ] x″ y′} {ϕ : Hom[ id ] x′ x″} → is-cartesian f f′ → has-section↓ ϕ → f″ ∘′ ϕ ≡[ idr _ ] f′ → is-cartesian f f″ cartesian-vertical-retraction-stable {f′ = f′} {f″} {ϕ} f-cart ϕ-sect factor = f″-cart where open is-cartesian f-cart module ϕ-sect = has-section[_] ϕ-sect f″-cart : is-cartesian _ f″ f″-cart .is-cartesian.universal m h′ = hom[ idl m ] (ϕ ∘′ universal m h′) f″-cart .is-cartesian.commutes m h′ = f″ ∘′ hom[] (ϕ ∘′ universal m h′) ≡⟨ whisker-r _ ⟩≡ hom[] (f″ ∘′ ϕ ∘′ universal m h′) ≡⟨ revive₁ {p = ap (_ ∘_) (idl m)} (pulll′ (idr _) factor) ⟩≡ hom[] (f′ ∘′ universal m h′) ≡⟨ (hom[]⟩⟨ commutes m h′) ∙ liberate _ ⟩≡ h′ ∎ f″-cart .is-cartesian.unique {m = m} {h′ = h′} m′ p = m′ ≡⟨ shiftr (sym (eliml (idl _))) (introl′ (idl _) ϕ-sect.is-section′) ⟩≡ hom[] ((ϕ ∘′ ϕ-sect.section′) ∘′ m′) ≡⟨ weave _ (pullr (idl _)) _ (pullr′ (idl _) (to-pathp (unique _ unique-path))) ⟩≡ hom[] (ϕ ∘′ universal m h′) ∎ where sect-commute : f′ ∘′ ϕ-sect.section′ ≡[ idr _ ] f″ sect-commute = to-pathp⁻ $ f′ ∘′ ϕ-sect.section′ ≡⟨ shiftr _ (λ i → factor (~ i) ∘′ ϕ-sect.section′) ⟩≡ hom[] ((f″ ∘′ ϕ) ∘′ ϕ-sect.section′) ≡⟨ weave _ (idr _ ∙ idr _) _ (cancelr′ (idl _) ϕ-sect.is-section′) ⟩≡ hom[] f″ ∎ unique-path : f′ ∘′ hom[ idl m ] (ϕ-sect.section′ ∘′ m′) ≡ h′ unique-path = f′ ∘′ hom[ idl m ] (ϕ-sect.section′ ∘′ m′) ≡⟨ whisker-r _ ⟩≡ hom[] (f′ ∘′ ϕ-sect.section′ ∘′ m′) ≡⟨ shiftl _ (pulll′ (idr _) sect-commute) ⟩≡ f″ ∘′ m′ ≡⟨ p ⟩≡ h′ ∎
We also have the following extremely useful pasting lemma, which generalizes the pasting law for pullbacks.
cartesian-pasting : ∀ {x y z} {f : Hom y z} {g : Hom x y} → ∀ {x′ y′ z′} {f′ : Hom[ f ] y′ z′} {g′ : Hom[ g ] x′ y′} → is-cartesian f f′ → is-cartesian (f ∘ g) (f′ ∘′ g′) → is-cartesian g g′ cartesian-pasting {f = f} {g = g} {f′ = f′} {g′ = g′} f-cart fg-cart = g-cart where open is-cartesian g-cart : is-cartesian g g′ g-cart .universal m h′ = universal′ fg-cart (sym (assoc _ _ _)) (f′ ∘′ h′) g-cart .commutes m h′ = g′ ∘′ universal′ fg-cart (sym (assoc _ _ _)) (f′ ∘′ h′) ≡⟨ f-cart .unique _ (from-pathp⁻ (assoc′ _ _ _) ∙ from-pathp (commutesp fg-cart _ _)) ⟩≡ f-cart .universal _ (f′ ∘′ h′) ≡˘⟨ f-cart .unique h′ refl ⟩≡˘ h′ ∎ g-cart .unique {m = m} {h′ = h′} m′ p = uniquep fg-cart (sym (assoc _ _ _)) refl (sym (assoc _ _ _)) m′ (pullr′ refl p)
If a morphism is both vertical and cartesian, then it must be an isomorphism. We can construct the inverse by factorizing the identity morphism, which is possible due to the fact that is vertical.
vertical+cartesian→invertible : ∀ {x} {x′ x″ : Ob[ x ]} {f′ : Hom[ id ] x′ x″} → is-cartesian id f′ → is-invertible↓ f′ vertical+cartesian→invertible {x′ = x′} {x″ = x″} {f′ = f′} f-cart = make-invertible↓ f⁻¹′ f′-invl f′-invr where open is-cartesian f-cart f⁻¹′ : Hom[ id ] x″ x′ f⁻¹′ = universal′ (idl _) id′ f′-invl : f′ ∘′ f⁻¹′ ≡[ idl _ ] id′ f′-invl = commutesp _ id′ path : f′ ∘′ f⁻¹′ ∘′ f′ ≡[ elimr (idl _) ] f′ path = cancell′ (idl _) (commutesp (idl _) id′) f′-invr : f⁻¹′ ∘′ f′ ≡[ idl _ ] id′ f′-invr = to-pathp⁻ $ f⁻¹′ ∘′ f′ ≡⟨ shiftr _ (uniquep _ (idl _) (idl _) (f⁻¹′ ∘′ f′) path) ⟩≡ hom[] (universal′ (idl _) f′) ≡⟨ weave _ _ _ (symP $ uniquep (idr _) refl (idl _) id′ (idr′ _)) ⟩≡ hom[] id′ ∎
Cartesian Lifts🔗
We call an object over together with a Cartesian arrow a Cartesian lift of . Cartesian lifts, defined by universal property as they are, are unique when they exist, so that “having Cartesian lifts” is a property, not a structure.
record Cartesian-lift {x y} (f : Hom x y) (y′ : Ob[ y ]) : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where no-eta-equality field {x′} : Ob[ x ] lifting : Hom[ f ] x′ y′ cartesian : is-cartesian f lifting open is-cartesian cartesian public
We note that the classical literature often differentiates between fibrations — those displayed categories for which there exist Cartesian lifts for every right corner — and cloven fibrations, those for which the Cartesian lifts are “algebraic” in a sense. This is because, classically, essentially unique means that there are still some choices to be made, and invoking the axiom of choice makes an “arbitrary” set of such choices. But, in the presence of univalence, there is exactly one choice to be made, that is, no choice at all. Thus, we do not dwell on the distinction.
record Cartesian-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where no-eta-equality field has-lift : ∀ {x y} (f : Hom x y) (y′ : Ob[ y ]) → Cartesian-lift f y′ module has-lift {x y} (f : Hom x y) (y′ : Ob[ y ]) = Cartesian-lift (has-lift f y′)
A Cartesian fibration is a displayed category having Cartesian lifts for every right corner.
Why?🔗
Admittedly, the notion of Cartesian morphism is slightly artificial. It arises from studying the specific properties of the pullback functors which exist in a category of pullbacks, hence the similarity in universal property!
In fact, the quintessential example of a Cartesian fibration is the codomain fibration, which is a category displayed over , where the fibre over is the slice category . We may investigate further (to uncover the name “codomain”): the total space of this fibration is the arrow category , and the projection functor is the codomain functor .
This displayed category extends to a pseudofunctor exactly when has all pullbacks, because in a world where the vertical arrows are “just” arrows, a Cartesian morphism is exactly a pullback square.
Other examples exist:
- The family fibration exhibits any category as displayed over . The fibres are functor categories (with discrete domains), reindexing is given by composition.
- The category of modules is fibred over the category of rings. The fibre over a ring is the category of -modules, Cartesian lifts are given by restriction of scalars.
Properties of Cartesian Fibrations🔗
If is a fibration, then every morphism is equivalent to a vertical morphism.
open Cartesian-lift open Cartesian-fibration fibration→vertical-equiv : ∀ {X Y X′ Y′} → (fib : Cartesian-fibration) → (u : Hom X Y) → Hom[ u ] X′ Y′ ≃ Hom[ id ] X′ (fib .has-lift u Y′ .x′) fibration→vertical-equiv fib u = Iso→Equiv $ (λ u′ → fib .has-lift _ _ .universal id (hom[ idr u ]⁻ u′)) , iso (λ u′ → hom[ idr u ] (fib .has-lift _ _ .lifting ∘′ u′)) (λ u′ → sym $ fib .has-lift _ _ .unique u′ (sym (hom[]-∙ _ _ ∙ liberate _))) (λ u′ → (hom[]⟩⟨ fib .has-lift _ _ .commutes _ _) ·· hom[]-∙ _ _ ·· liberate _)