module Cat.Displayed.Instances.Comma where
Comma categories as displayed categories🔗
We can neatly present comma categories as categories displayed over product categories.
module _ {oa ℓa ob ℓb oc ℓc} {A : Precategory oa ℓa} {B : Precategory ob ℓb} {C : Precategory oc ℓc} (F : Functor A C) (G : Functor B C) where private module A = Cat.Reasoning A module B = Cat.Reasoning B module C = Cat.Reasoning C module F = Cat.Functor.Reasoning F module G = Cat.Functor.Reasoning G open Displayed
Comma : Displayed (A ×ᶜ B) ℓc ℓc Comma .Ob[_] (a , b) = C.Hom (F.₀ a) (G.₀ b) Comma .Hom[_] (u , v) f g = G.₁ v C.∘ f ≡ g C.∘ F.₁ u Comma .Hom[_]-set _ _ _ = hlevel 2 Comma .id' = C.eliml G.F-id ∙ C.intror F.F-id Comma ._∘'_ α β = G.popr β ∙ sym (F.shufflel (sym α)) Comma .idr' _ = prop! Comma .idl' _ = prop! Comma .assoc' _ _ _ = prop!
Comma categories are discrete two-sided fibrations🔗
module _ {oa ℓa ob ℓb oc ℓc} {A : Precategory oa ℓa} {B : Precategory ob ℓb} {C : Precategory oc ℓc} {F : Functor A C} {G : Functor B C} where private module A = Cat.Reasoning A module B = Cat.Reasoning B module C = Cat.Reasoning C module F = Cat.Functor.Reasoning F module G = Cat.Functor.Reasoning G open is-discrete-two-sided-fibration open Displayed
Comma categories are discrete two-sided fibrations.
Comma-is-discrete-two-sided-fibration : is-discrete-two-sided-fibration (Comma F G) Comma-is-discrete-two-sided-fibration .fibre-set _ _ = hlevel 2 Comma-is-discrete-two-sided-fibration .cart-lift f g .centre = g C.∘ F.₁ f , C.eliml G.F-id Comma-is-discrete-two-sided-fibration .cart-lift f g .paths (h , p) = Σ-prop-path! (sym p ∙ C.eliml G.F-id) Comma-is-discrete-two-sided-fibration .cocart-lift f g .centre = G.₁ f C.∘ g , C.intror F.F-id Comma-is-discrete-two-sided-fibration .cocart-lift f g .paths (h , p) = Σ-prop-path! (p ∙ C.elimr F.F-id) Comma-is-discrete-two-sided-fibration .vert-lift {x = f} {y = g} {u = h} {v = k} p = G.F₁ B.id C.∘ G.F₁ k C.∘ f ≡⟨ C.eliml G.F-id ⟩≡ G.F₁ k C.∘ f ≡⟨ p ⟩≡ g C.∘ F.₁ h ≡⟨ C.intror F.F-id ⟩≡ (g C.∘ F.F₁ h) C.∘ F.F₁ A.id ∎ Comma-is-discrete-two-sided-fibration .factors _ = prop!
Every morphism in a discrete two-sided fibration is cartesian, but this is not neccesarily true of every morphism. In our setting, the cartesian maps are given by squares that satisfy the following pasting property: for every (potentially non-commutative) square of the below form, if the overall rectangle commutes, then the upper square commutes.
pasting→comma-cartesian : ∀ {w x y z} {u : A.Hom w x} {v : B.Hom y z} {f : C.Hom (F.₀ w) (G.₀ y)} {g : C.Hom (F.₀ x) (G.₀ z)} → (p : G.₁ v C.∘ f ≡ g C.∘ F.₁ u) → (∀ {a b} {h : C.Hom (F.₀ a) (G.₀ b)} {j : A.Hom a w} {k : B.Hom b y} → G.₁ v C.∘ G.₁ k C.∘ h ≡ g C.∘ F.₁ u C.∘ F.₁ j → G.₁ k C.∘ h ≡ f C.∘ F.₁ j) → is-cartesian (Comma F G) (u , v) p pasting→comma-cartesian p paste .is-cartesian.universal _ outer = paste (C.pulll (sym $ G.F-∘ _ _) ·· outer ·· ap₂ C._∘_ refl (F.F-∘ _ _)) pasting→comma-cartesian p paste .is-cartesian.commutes _ _ = prop! pasting→comma-cartesian p paste .is-cartesian.unique _ _ = prop! comma-cartesian→pasting : ∀ {w x y z} {u : A.Hom w x} {v : B.Hom y z} {f : C.Hom (F.₀ w) (G.₀ y)} {g : C.Hom (F.₀ x) (G.₀ z)} → (p : G.₁ v C.∘ f ≡ g C.∘ F.₁ u) → is-cartesian (Comma F G) (u , v) p → ∀ {a b} {h : C.Hom (F.₀ a) (G.₀ b)} {j : A.Hom a w} {k : B.Hom b y} → G.₁ v C.∘ G.₁ k C.∘ h ≡ g C.∘ F.₁ u C.∘ F.₁ j → G.₁ k C.∘ h ≡ f C.∘ F.₁ j comma-cartesian→pasting p p-cart outer = is-cartesian.universal p-cart _ $ C.pushl (G.F-∘ _ _) ·· outer ·· ap₂ C._∘_ refl (sym $ F.F-∘ _ _)
Moreover, a square is cocartesian when it satisfies the dual pasting lemma.
pasting→comma-cocartesian : ∀ {w x y z} {u : A.Hom w x} {v : B.Hom y z} {f : C.Hom (F.₀ w) (G.₀ y)} {g : C.Hom (F.₀ x) (G.₀ z)} → (p : G.₁ v C.∘ f ≡ g C.∘ F.₁ u) → (∀ {a b} {h : C.Hom (F.₀ a) (G.₀ b)} {j : A.Hom x a} {k : B.Hom z b} → G.₁ k C.∘ G.₁ v C.∘ f ≡ h C.∘ F.₁ j C.∘ F.₁ u → G.₁ k C.∘ g ≡ h C.∘ F.₁ j) → is-cocartesian (Comma F G) (u , v) p comma-cocartesian→pasting : ∀ {w x y z} {u : A.Hom w x} {v : B.Hom y z} {f : C.Hom (F.₀ w) (G.₀ y)} {g : C.Hom (F.₀ x) (G.₀ z)} → (p : G.₁ v C.∘ f ≡ g C.∘ F.₁ u) → is-cocartesian (Comma F G) (u , v) p → ∀ {a b} {h : C.Hom (F.₀ a) (G.₀ b)} {j : A.Hom x a} {k : B.Hom z b} → G.₁ k C.∘ G.₁ v C.∘ f ≡ h C.∘ F.₁ j C.∘ F.₁ u → G.₁ k C.∘ g ≡ h C.∘ F.₁ j
The proofs are formally dual, so we omit them.
pasting→comma-cocartesian p paste .is-cocartesian.universal _ outer = paste (C.pulll (sym $ G.F-∘ _ _) ·· outer ·· ap₂ C._∘_ refl (F.F-∘ _ _)) pasting→comma-cocartesian p paste .is-cocartesian.commutes _ _ = prop! pasting→comma-cocartesian p paste .is-cocartesian.unique _ _ = prop! comma-cocartesian→pasting p p-cocart outer = is-cocartesian.universal p-cocart _ $ C.pushl (G.F-∘ _ _) ·· outer ·· ap₂ C._∘_ refl (sym $ F.F-∘ _ _)