From e717a6fa5c436d2fa8ce2e746bee40123691e83a Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Thu, 14 Aug 2025 15:02:43 -0700 Subject: [PATCH 01/24] displayed category of displayed functors, bidisplayed categories --- src/Cat/Bi/Displayed/Base.agda | 305 ++++++++++++++++++ .../Displayed/Instances/DisplayedFunctor.agda | 118 +++++++ 2 files changed, 423 insertions(+) create mode 100644 src/Cat/Bi/Displayed/Base.agda create mode 100644 src/Cat/Displayed/Instances/DisplayedFunctor.agda diff --git a/src/Cat/Bi/Displayed/Base.agda b/src/Cat/Bi/Displayed/Base.agda new file mode 100644 index 000000000..5219f593d --- /dev/null +++ b/src/Cat/Bi/Displayed/Base.agda @@ -0,0 +1,305 @@ + +open import Cat.Prelude +open import Cat.Displayed.Base +open import Cat.Instances.Product +open import Cat.Bi.Base +open import Cat.Displayed.Total +open import Cat.Displayed.Functor +open import Cat.Displayed.Instances.TotalProduct +open import Cat.Displayed.Instances.DisplayedFunctor hiding (_◆'_) +open import Cat.Displayed.Morphism +open import Cat.Displayed.Functor.Naturality +import Cat.Displayed.Reasoning as DR + +-- Some reference taken from https://arxiv.org/pdf/1903.01152 +module Cat.Bi.Displayed.Base where + +open Functor +open Displayed-functor +open _=[_]=>_ +open make-natural-iso[_] + +module _ where + + compose-assocˡ' : ∀ {o o' d d' ℓ ℓ'} {O : Type o} {H : O → O → Precategory ℓ ℓ'} + → {O' : O → Type o'} {H' : ∀ {a b} → O' a → O' b → Displayed (H a b) d d'} + → {F : ∀ {A B C} → Functor (H B C ×ᶜ H A B) (H A C)} + → (F' : ∀ {A B C} {A' : O' A} {B' : O' B} {C' : O' C} → Displayed-functor F (H' B' C' ×ᵀᴰ H' A' B') (H' A' C')) + → ∀ {A B C D} {A' : O' A} {B' : O' B} {C' : O' C} {D' : O' D} + → Displayed-functor (compose-assocˡ {O = O} {H = H} F) (H' C' D' ×ᵀᴰ H' B' C' ×ᵀᴰ H' A' B') (H' A' D') + compose-assocˡ' F' .F₀' (F , G , H) = F' .F₀' (F' .F₀' (F , G) , H) + compose-assocˡ' F' .F₁' (f , g , h) = F' .F₁' (F' .F₁' (f , g) , h) + compose-assocˡ' {H' = H'} F' {A' = A'} {D' = D'} .F-id' = + cast[] (apd (λ _ → F' .F₁') (F' .F-id' ,ₚ refl) ∙[] (F' .F-id')) + where + open Displayed (H' A' D') + open DR (H' A' D') + compose-assocˡ' {H' = H'} F' {A' = A'} {D' = D'} .F-∘' = + cast[] (apd (λ _ → F' .F₁') (F' .F-∘' ,ₚ refl) ∙[] F' .F-∘') + where + open Displayed (H' A' D') + open DR (H' A' D') + + compose-assocʳ' : ∀ {o o' d d' ℓ ℓ'} {O : Type o} {H : O → O → Precategory ℓ ℓ'} + → {O' : O → Type o'} {H' : ∀ {a b} → O' a → O' b → Displayed (H a b) d d'} + → {F : ∀ {A B C} → Functor (H B C ×ᶜ H A B) (H A C)} + → (F' : ∀ {A B C} {A' : O' A} {B' : O' B} {C' : O' C} + → Displayed-functor F (H' B' C' ×ᵀᴰ H' A' B') (H' A' C')) + → ∀ {A B C D} {A' : O' A} {B' : O' B} {C' : O' C} {D' : O' D} + → Displayed-functor (compose-assocʳ {O = O} {H = H} F) + (H' C' D' ×ᵀᴰ H' B' C' ×ᵀᴰ H' A' B') (H' A' D') + compose-assocʳ' F' .F₀' (F , G , H) = F' .F₀' (F , F' .F₀' (G , H)) + compose-assocʳ' F' .F₁' (f , g , h) = F' .F₁' (f , F' .F₁' (g , h)) + compose-assocʳ' {H' = H'} F' {A' = A'} {D' = D'} .F-id' = + cast[] (apd (λ _ → F' .F₁') (refl ,ₚ F' .F-id') ∙[] F' .F-id') + where + open Displayed (H' A' D') + open DR (H' A' D') + compose-assocʳ' {H' = H'} F' {A' = A'} {D' = D'} .F-∘' = + cast[] (apd (λ _ → F' .F₁') (refl ,ₚ F' .F-∘') ∙[] F' .F-∘') + where + open Displayed (H' A' D') + open DR (H' A' D') + +record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type (lsuc (o' ⊔ oh' ⊔ ℓh') ⊔ o ⊔ oh ⊔ ℓh) where + no-eta-equality + open Prebicategory B + field + Ob[_] : Ob → Type o' + Hom[_,_] : ∀ {A B} → Ob[ A ] → Ob[ B ] → Displayed (Hom A B) oh' ℓh' + + module Hom[] {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} = Displayed (Hom[ A' , B' ]) + + + _[_]↦_ : ∀ {A B} → Ob[ A ] → (A ↦ B) → Ob[ B ] → Type _ + A' [ f ]↦ B' = Hom[ A' , B' ] .Displayed.Ob[_] f + + + _[_]⇒_ : ∀ {A B} {f g : A ↦ B} + → {A' : Ob[ A ]} {B' : Ob[ B ]} + → A' [ f ]↦ B' → (f ⇒ g) → A' [ g ]↦ B' + → Type _ + _[_]⇒_ {A' = A'} {B' = B'} f' α g' = Hom[ A' , B' ] .Displayed.Hom[_] α f' g' + + + field + ↦id' : ∀ {x} {x' : Ob[ x ]} → x' [ id ]↦ x' + + ⇒id' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} + → {f : A ↦ B} {f' : A' [ f ]↦ B'} + → f' [ Hom.id ]⇒ f' + ⇒id' = Hom[].id' + + field + compose' : ∀ {A B C} {A' : Ob[ A ]} {B' : Ob[ B ]} {C' : Ob[ C ]} + → Displayed-functor compose (Hom[ B' , C' ] ×ᵀᴰ Hom[ A' , B' ]) Hom[ A' , C' ] + + module compose' {A} {B} {C} {A'} {B'} {C'} = Displayed-functor (compose' {A} {B} {C} {A'} {B'} {C'}) + + -- Displayed 1-cell composition + _⊗'_ : ∀ {A B C A' B' C'} {f : B ↦ C} {g : A ↦ B} → (B' [ f ]↦ C') → (A' [ g ]↦ B') → A' [ f ⊗ g ]↦ C' + _⊗'_ f' g' = compose' · (f' , g') + + -- Vertical displayed 2-cell composition + _∘'_ : ∀ {A B A' B'} {f g h : A ↦ B} + → {f' : A' [ f ]↦ B'} {g' : A' [ g ]↦ B'} {h' : A' [ h ]↦ B'} + → {β : g ⇒ h} {α : f ⇒ g} + → g' [ β ]⇒ h' → f' [ α ]⇒ g' + → f' [ β ∘ α ]⇒ h' + _∘'_ = Hom[]._∘'_ + + + -- Horizontal displayed 2-cell composition + _◆'_ : ∀ {A B C A' B' C'} + → {f₁ f₂ : B ↦ C} {β : f₁ ⇒ f₂} + → {g₁ g₂ : A ↦ B} {α : g₁ ⇒ g₂} + → {f₁' : B' [ f₁ ]↦ C'} {f₂' : B' [ f₂ ]↦ C'} + → {g₁' : A' [ g₁ ]↦ B'} {g₂' : A' [ g₂ ]↦ B'} + → (β' : f₁' [ β ]⇒ f₂') (α' : g₁' [ α ]⇒ g₂') + → (f₁' ⊗' g₁') [ β ◆ α ]⇒ (f₂' ⊗' g₂') + _◆'_ α' β' = compose'.₁' (α' , β') + + infixr 30 _∘'_ + infixr 25 _⊗'_ + infix 35 _◀'_ _▶'_ + + + -- Displayed whiskering on the right + _▶'_ : ∀ {A B C A' B' C'} {f : B ↦ C} {g₁ g₂ : A ↦ B} {α : g₁ ⇒ g₂} + → {g₁' : A' [ g₁ ]↦ B'} {g₂' : A' [ g₂ ]↦ B'} + → (f' : B' [ f ]↦ C') + → (α' : g₁' [ α ]⇒ g₂') + → f' ⊗' g₁' [ f ▶ α ]⇒ f' ⊗' g₂' + _▶'_ f' α' = compose'.₁' (⇒id' , α') + + + -- Displayed whiskering on the left + _◀'_ : ∀ {A B C A' B' C'} {g : A ↦ B} {f₁ f₂ : B ↦ C} {β : f₁ ⇒ f₂} + → {f₁' : B' [ f₁ ]↦ C'} {f₂' : B' [ f₂ ]↦ C'} + → (β' : f₁' [ β ]⇒ f₂') + → (g' : A' [ g ]↦ B') + → f₁' ⊗' g' [ β ◀ g ]⇒ f₂' ⊗' g' + _◀'_ β' g' = compose'.₁' (β' , ⇒id') + + + -- Displayed unitor and associator isos + field + unitor-l' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → _≅[_]_ Disp[ Hom[ A' , B' ] , Hom[ A' , B' ] ] Id' unitor-l (Right' compose' ↦id') + unitor-r' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → _≅[_]_ Disp[ Hom[ A' , B' ] , Hom[ A' , B' ] ] Id' unitor-r (Left' compose' ↦id') + + associator' : ∀ {A B C D} {A' : Ob[ A ]} {B' : Ob[ B ]} {C' : Ob[ C ]} {D' : Ob[ D ]} + → _≅[_]_ Disp[ Hom[ C' , D' ] ×ᵀᴰ (Hom[ B' , C' ] ×ᵀᴰ Hom[ A' , B' ]) , Hom[ A' , D' ] ] + (compose-assocˡ' {H' = Hom[_,_]} compose') associator (compose-assocʳ' {H' = Hom[_,_]} compose') + + -- Displayed versions of all the morphism combinators + -- The naturality types are crazy lol + + λ←' : ∀ {A B A' B'} {f : A ↦ B} (f' : A' [ f ]↦ B') → (↦id' ⊗' f') [ λ← f ]⇒ f' + λ←' = unitor-l' ._≅[_]_.from' .η' + + λ→' : ∀ {A B A' B'} {f : A ↦ B} + → (f' : A' [ f ]↦ B') + → f' [ λ→ f ]⇒ (↦id' ⊗' f') + λ→' = unitor-l' ._≅[_]_.to' .η' + + ρ←' : ∀ {A B A' B'} {f : A ↦ B} + → (f' : A' [ f ]↦ B') + → (f' ⊗' ↦id') [ ρ← f ]⇒ f' + ρ←' = unitor-r' ._≅[_]_.from' .η' + + ρ→' : ∀ {A B A' B'} {f : A ↦ B} + → (f' : A' [ f ]↦ B') + → f' [ ρ→ f ]⇒ (f' ⊗' ↦id') + ρ→' = unitor-r' ._≅[_]_.to' .η' + + ρ←nat' : ∀ {A B A' B'} {f₁ f₂ : A ↦ B} {β : f₁ ⇒ f₂} + → {f₁' : A' [ f₁ ]↦ B'} {f₂' : A' [ f₂ ]↦ B'} + → (β' : f₁' [ β ]⇒ f₂') + → (ρ←' _ ∘' (β' ◀' ↦id')) Hom[].≡[ ρ←nat β ] (β' ∘' ρ←' _) + ρ←nat' β' = unitor-r' .from' .is-natural' _ _ β' + + λ←nat' : ∀ {A B A' B'} {f₁ f₂ : A ↦ B} {β : f₁ ⇒ f₂} + → {f₁' : A' [ f₁ ]↦ B'} {f₂' : A' [ f₂ ]↦ B'} + → (β' : f₁' [ β ]⇒ f₂') + → (λ←' _ ∘' (↦id' ▶' β')) Hom[].≡[ λ←nat β ] (β' ∘' λ←' _) + λ←nat' β' = unitor-l' .from' .is-natural' _ _ β' + + ρ→nat' : ∀ {A B A' B'} {f₁ f₂ : A ↦ B} {β : f₁ ⇒ f₂} + → {f₁' : A' [ f₁ ]↦ B'} {f₂' : A' [ f₂ ]↦ B'} + → (β' : f₁' [ β ]⇒ f₂') + → (ρ→' _ ∘' β') Hom[].≡[ ρ→nat β ] ((β' ◀' ↦id') ∘' ρ→' _) + ρ→nat' β' = unitor-r' .to' .is-natural' _ _ β' + + λ→nat' : ∀ {A B A' B'} {f₁ f₂ : A ↦ B} {β : f₁ ⇒ f₂} + → {f₁' : A' [ f₁ ]↦ B'} {f₂' : A' [ f₂ ]↦ B'} + → (β' : f₁' [ β ]⇒ f₂') + → (λ→' _ ∘' β') Hom[].≡[ λ→nat β ] ((↦id' ▶' β') ∘' λ→' _) + λ→nat' β' = unitor-l' .to' .is-natural' _ _ β' + + α→' : ∀ {A B C D A' B' C' D'} + {f : C ↦ D} {g : B ↦ C} {h : A ↦ B} + → (f' : C' [ f ]↦ D') (g' : B' [ g ]↦ C') (h' : A' [ h ]↦ B') + → ((f' ⊗' g') ⊗' h') [ α→ f g h ]⇒ (f' ⊗' (g' ⊗' h')) + α→' f' g' h' = associator' ._≅[_]_.to' .η' (f' , g' , h') + + α←' : ∀ {A B C D A' B' C' D'} + {f : C ↦ D} {g : B ↦ C} {h : A ↦ B} + → (f' : C' [ f ]↦ D') (g' : B' [ g ]↦ C') (h' : A' [ h ]↦ B') + → (f' ⊗' (g' ⊗' h')) [ α← f g h ]⇒ ((f' ⊗' g') ⊗' h') + α←' f' g' h' = associator' ._≅[_]_.from' .η' (f' , g' , h') + + α←nat' : ∀ {A B C D A' B' C' D'} + {f₁ f₂ : C ↦ D} {g₁ g₂ : B ↦ C} {h₁ h₂ : A ↦ B} + {β : f₁ ⇒ f₂} {γ : g₁ ⇒ g₂} {δ : h₁ ⇒ h₂} + {f₁' : C' [ f₁ ]↦ D'} {f₂' : C' [ f₂ ]↦ D'} + {g₁' : B' [ g₁ ]↦ C'} {g₂' : B' [ g₂ ]↦ C'} + {h₁' : A' [ h₁ ]↦ B'} {h₂' : A' [ h₂ ]↦ B'} + → (β' : f₁' [ β ]⇒ f₂') (γ' : g₁' [ γ ]⇒ g₂') (δ' : h₁' [ δ ]⇒ h₂') + → (α←' _ _ _ ∘' (β' ◆' (γ' ◆' δ'))) Hom[].≡[ α←nat β γ δ ] + (((β' ◆' γ') ◆' δ') ∘' α←' _ _ _) + α←nat' β' γ' δ' = + associator' .from' .is-natural' (_ , _ , _) (_ , _ , _) (β' , γ' , δ') + + α→nat' : ∀ {A B C D A' B' C' D'} + {f₁ f₂ : C ↦ D} {g₁ g₂ : B ↦ C} {h₁ h₂ : A ↦ B} + {β : f₁ ⇒ f₂} {γ : g₁ ⇒ g₂} {δ : h₁ ⇒ h₂} + {f₁' : C' [ f₁ ]↦ D'} {f₂' : C' [ f₂ ]↦ D'} + {g₁' : B' [ g₁ ]↦ C'} {g₂' : B' [ g₂ ]↦ C'} + {h₁' : A' [ h₁ ]↦ B'} {h₂' : A' [ h₂ ]↦ B'} + → (β' : f₁' [ β ]⇒ f₂') (γ' : g₁' [ γ ]⇒ g₂') (δ' : h₁' [ δ ]⇒ h₂') + → (α→' _ _ _ ∘' ((β' ◆' γ') ◆' δ')) Hom[].≡[ α→nat β γ δ ] + ((β' ◆' (γ' ◆' δ')) ∘' α→' _ _ _) + α→nat' β' γ' δ' = + associator' .to' .is-natural' (_ , _ , _) (_ , _ , _) (β' , γ' , δ') + + field + triangle' + : ∀ {A B C A' B' C'} {f : B ↦ C} {g : A ↦ B} + → (f' : B' [ f ]↦ C') (g' : A' [ g ]↦ B') + → ((ρ←' f' ◀' g') ∘' α←' f' ↦id' g') Hom[].≡[ triangle f g ] (f' ▶' λ←' g') + + pentagon' + : ∀ {A B C D E A' B' C' D' E'} + → {f : D ↦ E} {g : C ↦ D} {h : B ↦ C} {i : A ↦ B} + → (f' : D' [ f ]↦ E') + → (g' : C' [ g ]↦ D') + → (h' : B' [ h ]↦ C') + → (i' : A' [ i ]↦ B') + → ((α←' f' g' h' ◀' i') ∘' α←' f' (g' ⊗' h') i' ∘' (f' ▶' α←' g' h' i')) + Hom[].≡[ pentagon f g h i ] + (α←' (f' ⊗' g') h' i' ∘' α←' f' g' (h' ⊗' i')) + + +-- Lets define the displayed bicategory of displayed categories! + +open Bidisplayed hiding (_∘'_) +Displayed-cat : ∀ o ℓ o' ℓ' → Bidisplayed (Cat o ℓ) _ _ _ +Displayed-cat o ℓ o' ℓ' .Ob[_] C = Displayed C o' ℓ' +Displayed-cat o ℓ o' ℓ' .Hom[_,_] D E = Disp[ D , E ] +Displayed-cat o ℓ o' ℓ' .↦id' = Id' +Displayed-cat o ℓ o' ℓ' .compose' = F∘'-functor +Displayed-cat o ℓ o' ℓ' .unitor-l' {B' = B'} = to-natural-iso' ni where + open Displayed B' + open DR B' + ni : make-natural-iso[ _ ] _ _ + ni .eta' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[] + ni .inv' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[] + ni .eta∘inv' x' = Nat'-path λ x'' → idl' _ + ni .inv∘eta' x' = Nat'-path λ x'' → idl' _ + ni .natural' x' y' f' = Nat'-path λ x'' → cast[] $ symP $ (idr' _ ∙[] id-comm[]) + +Displayed-cat o ℓ o' ℓ' .unitor-r' {B' = B'} = to-natural-iso' ni where + open Displayed B' + open DR B' + ni : make-natural-iso[ _ ] _ _ + ni .eta' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[] + ni .inv' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[] + ni .eta∘inv' x' = Nat'-path λ x'' → idl' _ + ni .inv∘eta' x' = Nat'-path λ x'' → idl' _ + ni .natural' x' y' f' = Nat'-path λ x'' → cast[] $ (idl' _ ∙[] symP (idr' _ ∙[] ((y' .F-id' ⟩∘'⟨refl) ∙[] idl' _))) + +Displayed-cat o ℓ o' ℓ' .associator' {C' = C'} {D' = D'} = to-natural-iso' ni where + open Displayed D' + open DR D' + module C' = Displayed C' + ni : make-natural-iso[ _ ] _ _ + ni .eta' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[] + ni .inv' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[] + ni .eta∘inv' x' = Nat'-path (λ _ → idl' _) + ni .inv∘eta' x' = Nat'-path (λ _ → idl' _) + ni .natural' (x₁ , x₂ , x₃) (y₁ , y₂ , y₃) (α₁ , α₂ , α₃) = Nat'-path λ z → cast[] $ + (idl' _ ∙[] symP (pushl[] _ (y₁ .F-∘')) ∙[] symP (idr' _)) + +Displayed-cat o ℓ o' ℓ' .triangle' {B' = B'} {C' = C'} f' g' = Nat'-path λ x' → C'.idr' _ where + module C' = Displayed C' +Displayed-cat o ℓ o' ℓ' .pentagon' {B' = B'} {C' = C'} {D' = D'} {E' = E'} f' g' h' i' = Nat'-path λ x' → cast[] $ + (f' .F₁' (g' .F₁' (h' .F₁' B'.id')) ∘' id') ∘' (id' ∘' f' .F₁' D'.id' ∘' id') ≡[]⟨ idr' _ ⟩∘'⟨ idl' _ ⟩ + (f' .F₁' (g' .F₁' (h' .F₁' B'.id'))) ∘' (f' .F₁' D'.id' ∘' id') ≡[]⟨ ((apd (λ _ z → f' .F₁' (g' .F₁' z)) (h' .F-id')) ⟩∘'⟨ (idr' _)) ⟩ + (f' .F₁' (g' .F₁' C'.id')) ∘' (f' .F₁' D'.id') ≡[]⟨ ((apd (λ _ → f' .F₁') (g' .F-id') ∙[] f' .F-id') ⟩∘'⟨ f' .F-id') ⟩ + id' ∘' id' ∎ + where + open Displayed E' + open DR E' + module B' = Displayed B' + module C' = Displayed C' + module D' = Displayed D' diff --git a/src/Cat/Displayed/Instances/DisplayedFunctor.agda b/src/Cat/Displayed/Instances/DisplayedFunctor.agda new file mode 100644 index 000000000..c7e4ec575 --- /dev/null +++ b/src/Cat/Displayed/Instances/DisplayedFunctor.agda @@ -0,0 +1,118 @@ + + +open import Cat.Prelude +open import Cat.Instances.Functor +open import Cat.Displayed.Base +open import Cat.Displayed.Functor +open import Cat.Reasoning as CR +import Cat.Displayed.Reasoning as DR +open import Cat.Functor.Compose +open import Cat.Displayed.Instances.TotalProduct + +module Cat.Displayed.Instances.DisplayedFunctor where + + +open _=>_ +open _=[_]=>_ +open Functor +open Displayed-functor + +module _ + {oa ℓa ob ℓb oa' ℓa' ob' ℓb'} + {A : Precategory oa ℓa} {B : Precategory ob ℓb} + (D : Displayed A oa' ℓa') (E : Displayed B ob' ℓb') + where + private + module A = CR A + module B = CR B + module D = Displayed D + module E where + open Displayed E public + open DR E public + + + + module Cat[A,B] = Precategory Cat[ A , B ] + + Disp[_,_] : Displayed (Cat[ A , B ]) _ _ + Disp[_,_] .Displayed.Ob[_] f = Displayed-functor f D E + Disp[_,_] .Displayed.Hom[_] α F' G' = F' =[ α ]=> G' + Disp[_,_] .Displayed.Hom[_]-set _ _ _ = hlevel 2 where + unquoteDecl lvl = declare-record-hlevel 2 lvl (quote _=[_]=>_) + Disp[_,_] .Displayed.id' = idnt' + Disp[_,_] .Displayed._∘'_ = _∘nt'_ + Disp[_,_] .Displayed.idr' _ = Nat'-pathp refl refl (Cat[A,B].idr _) refl refl λ x' → E.idr' _ + Disp[_,_] .Displayed.idl' _ = Nat'-pathp refl refl (Cat[A,B].idl _) refl refl λ x' → E.idl' _ + Disp[_,_] .Displayed.assoc' _ _ _ = Nat'-pathp refl refl (Cat[A,B].assoc _ _ _) refl refl λ x' → E.assoc' _ _ _ + + +module _ + {oa ℓa ob ℓb oc ℓc oa' ℓa' ob' ℓb' oc' ℓc'} + {A : Precategory oa ℓa} {B : Precategory ob ℓb} + {C : Precategory oc ℓc} + {A' : Displayed A oa' ℓa'} {B' : Displayed B ob' ℓb'} + {C' : Displayed C oc' ℓc'} + {F G : Functor B C} {H K : Functor A B} + {α : F => G} {β : H => K} + {F' : Displayed-functor F B' C'} {G' : Displayed-functor G B' C'} + {H' : Displayed-functor H A' B'} {K' : Displayed-functor K A' B'} + where + private + module B' = Displayed B' + module C' where + open Displayed C' public + open DR C' public + + + _◆'_ : F' =[ α ]=> G' → H' =[ β ]=> K' → F' F∘' H' =[ α ◆ β ]=> G' F∘' K' + (α' ◆' β') .η' x' = G' .F₁' (β' .η' _) C'.∘' α' .η' _ + (α' ◆' β') .is-natural' x' y' f' = cast[] $ + (G' .F₁' (β' .η' y') ∘' α' .η' (H' .F₀' y')) ∘' F' .F₁' (H' .F₁' f') ≡[]⟨ pullr[] _ (α' .is-natural' _ _ _) ⟩ + G' .F₁' (β' .η' y') ∘' G' .F₁' (H' .F₁' f') ∘' α' .η' (H' .F₀' x') ≡[]⟨ pulll[] _ (symP (G' .F-∘') ∙[] apd (λ _ → G' .F₁') (β' .is-natural' _ _ _) ∙[] G' .F-∘') ⟩ + (G' .F₁' (K' .F₁' f') ∘' G' .F₁' (β' .η' x')) ∘' α' .η' (H' .F₀' x') ≡[]˘⟨ assoc' _ _ _ ⟩ + G' .F₁' (K' .F₁' f') ∘' G' .F₁' (β' .η' x') ∘' α' .η' (H' .F₀' x') ∎ + where open C' + + +module _ + {oa ℓa ob ℓb oc ℓc oa' ℓa' ob' ℓb' oc' ℓc'} + {A : Precategory oa ℓa} {B : Precategory ob ℓb} + {C : Precategory oc ℓc} + {A' : Displayed A oa' ℓa'} {B' : Displayed B ob' ℓb'} + {C' : Displayed C oc' ℓc'} + where + private + module C = Precategory C + module C' = Displayed C' + + F∘'-functor : Displayed-functor F∘-functor (Disp[ B' , C' ] ×ᵀᴰ Disp[ A' , B' ]) Disp[ A' , C' ] + F∘'-functor .F₀' (F' , G') = F' F∘' G' + F∘'-functor .F₁' (α' , β') = α' ◆' β' + F∘'-functor .F-id' {F , G} {F' , G'} = + Nat'-pathp refl refl _ refl refl + λ x' → C'.idr' _ C'.∙[] F' .F-id' + F∘'-functor .F-∘' {a' = F' , G'} {H' , I'} {J' , K'} {α' , _} {β' , _} = + Nat'-pathp refl refl _ refl refl + λ x' → + -- This is just using the same combinators as the F∘-functor proof, but displayed + pushl[] _ (J' .F-∘') C'.∙[] + ((extend-inner' _ (symP (α' .is-natural' _ _ _))) C'.∙[] + (pulll' refl refl)) + where open DR C' + + + + -- F∘-functor {C = C} = go module F∘-f where + -- private module C = Cat.Reasoning C + -- go : Functor _ _ + -- go .F₀ (F , G) = F F∘ G + -- go .F₁ (α , β) = α ◆ β + + -- go .F-id {x} = ext λ _ → C.idr _ ∙ x .fst .F-id + -- go .F-∘ {x} {y , _} {z , _} (f , _) (g , _) = ext λ _ → + -- z .F₁ _ C.∘ f .η _ C.∘ g .η _ ≡⟨ C.pushl (z .F-∘ _ _) ⟩ + -- z .F₁ _ C.∘ z .F₁ _ C.∘ f .η _ C.∘ g .η _ ≡⟨ C.extend-inner (sym (f .is-natural _ _ _)) ⟩ + -- z .F₁ _ C.∘ f .η _ C.∘ y .F₁ _ C.∘ g .η _ ≡⟨ C.pulll refl ⟩ + -- (z .F₁ _ C.∘ f .η _) C.∘ (y .F₁ _ C.∘ g .η _) ∎ + + From 6297628e9f0c0f0684dac10aff6742870f0a3dd5 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Thu, 14 Aug 2025 15:12:48 -0700 Subject: [PATCH 02/24] naturality stuff --- src/Cat/Displayed/Functor.lagda.md | 111 +++++++++++++++- src/Cat/Displayed/Functor/Naturality.agda | 122 ++++++++++++++++++ .../Displayed/Instances/DisplayedFunctor.agda | 14 -- .../Displayed/Instances/TotalProduct.lagda.md | 82 +++++++++++- src/Cat/Displayed/Reasoning.lagda.md | 23 +++- 5 files changed, 330 insertions(+), 22 deletions(-) create mode 100644 src/Cat/Displayed/Functor/Naturality.agda diff --git a/src/Cat/Displayed/Functor.lagda.md b/src/Cat/Displayed/Functor.lagda.md index a72dee541..4d4451a89 100644 --- a/src/Cat/Displayed/Functor.lagda.md +++ b/src/Cat/Displayed/Functor.lagda.md @@ -127,8 +127,26 @@ module → (q1 : ∀ {x y x' y'} {f : A.Hom x y} → (f' : ℰ.Hom[ f ] x' y') → PathP (λ i → ℱ.Hom[ p i .F₁ f ] (q0 x' i) (q0 y' i)) (F' .F₁' f') (G' .F₁' f')) → PathP (λ i → Displayed-functor (p i) ℰ ℱ) F' G' - Displayed-functor-pathp {F = F} {G = G} {F' = F'} {G' = G'} p q0 q1 = - injectiveP (λ _ → eqv) ((λ i x' → q0 x' i) ,ₚ (λ i f' → q1 f' i) ,ₚ prop!) + Displayed-functor-pathp {F = F} {F' = F'} {G' = G'} p q0 q1 = dfn where + -- We need to define this directly to get nice definitional behavior on the projections + dfn : PathP (λ i → Displayed-functor (p i) ℰ ℱ) F' G' + dfn i .F₀' x' = q0 x' i + dfn i .F₁' f' = q1 f' i + dfn i .F-id' {x' = x'} j = + is-set→squarep (λ i j → ℱ.Hom[ F-id (p i) j ]-set (q0 x' i) (q0 x' i)) + (q1 ℰ.id') (F-id' F') (F-id' G') (λ _ → ℱ.id') i j + dfn i .F-∘' {f = f} {g = g} {a' = a'} {c' = c'} {f' = f'} {g' = g'} j = + is-set→squarep (λ i j → ℱ.Hom[ F-∘ (p i) f g j ]-set (q0 a' i) (q0 c' i)) + (q1 (f' ℰ.∘' g')) (F-∘' F') (F-∘' G') (λ k → q1 f' k ℱ.∘' q1 g' k) i j + + Displayed-functor-is-set : {F : Functor A B} → (∀ x → is-set ℱ.Ob[ x ]) → is-set (Displayed-functor F ℰ ℱ) + Displayed-functor-is-set fibre-set = Iso→is-hlevel! 2 eqv where instance + ℱOb[] : ∀ {x} → H-Level (ℱ.Ob[ x ]) 2 + ℱOb[] = hlevel-instance (fibre-set _) + + instance + Funlike-displayed-functor : ∀ {F : Functor A B} {x} → Funlike (Displayed-functor F ℰ ℱ) (⌞ ℰ.Ob[ x ] ⌟) λ _ → ⌞ ℱ.Ob[ F .F₀ x ] ⌟ + Funlike-displayed-functor = record { _·_ = λ F x → F .F₀' x } ``` --> @@ -405,6 +423,23 @@ module → PathP (λ i → ℱ.Hom[ f ] (p0 x' i) (p0 y' i)) (F .F₁' f') (G .F₁' f')) → F ≡ G Vertical-functor-path = Displayed-functor-pathp refl + + Vertical-functor-path-prop + : {F G : Vertical-functor ℰ ℱ} + → (∀ {x y x' y'} {f : B.Hom x y} → is-prop (ℱ.Hom[ f ] x' y')) + → (p0 : ∀ {x} → (x' : ℰ.Ob[ x ]) → F .F₀' x' ≡ G .F₀' x') + → F ≡ G + Vertical-functor-path-prop prop p0 = Vertical-functor-path p0 (λ _ → is-prop→pathp (λ _ → prop) _ _) + + Vertical-functor-path-prop! + : {F G : Vertical-functor ℰ ℱ} + → ⦃ _ : ∀ {x y x' y'} {f : B.Hom x y} → H-Level (ℱ.Hom[ f ] x' y') 1 ⦄ + → (p0 : ∀ {x} → (x' : ℰ.Ob[ x ]) → F .F₀' x' ≡ G .F₀' x') + → F ≡ G + Vertical-functor-path-prop! = Vertical-functor-path-prop (hlevel 1) + + Vertical-functor-is-set : (∀ x → is-set ℱ.Ob[ x ]) → is-set (Vertical-functor ℰ ℱ) + Vertical-functor-is-set fibre-set = Displayed-functor-is-set fibre-set ``` --> @@ -468,6 +503,7 @@ module (G' : Displayed-functor G ℰ ℱ) : Type lvl where + constructor NT' no-eta-equality field @@ -486,6 +522,75 @@ vertical. ```agda -module Cat.Displayed.Instances.TotalProduct +module Cat.Displayed.Instances.TotalProduct where + +module _ {o₁ ℓ₁ o₂ ℓ₂ o₃ ℓ₃ o₄ ℓ₄} - (C : Precategory o₁ ℓ₁) - (D : Precategory o₂ ℓ₂) + {C : Precategory o₁ ℓ₁} + {D : Precategory o₂ ℓ₂} (EC : Displayed C o₃ ℓ₃) (ED : Displayed D o₄ ℓ₄) where private module EC = Displayed EC private module ED = Displayed ED @@ -31,6 +37,7 @@ $\cE\times \cD\to \cB\times \cC$, which is again a displayed category. ```agda + infixr 20 _×ᵀᴰ_ _×ᵀᴰ_ : Displayed (C ×ᶜ D) (o₃ ⊔ o₄) (ℓ₃ ⊔ ℓ₄) ``` If displayed categories are regarded as functors, then the product of @@ -71,3 +78,72 @@ they hold for the components of the ordered pairs. _×ᵀᴰ_ .Displayed.assoc' (f₁ , f₂) (g₁ , g₂) (h₁ , h₂) = EC.assoc' f₁ g₁ h₁ ,ₚ ED.assoc' f₂ g₂ h₂ ``` + +```agda + +module _ + {oa ℓa ob ℓb oc ℓc oa' ℓa' ob' ℓb' oc' ℓc'} + {A : Precategory oa ℓa} {B : Precategory ob ℓb} {C : Precategory oc ℓc} + {A' : Displayed A oa' ℓa'} {B' : Displayed B ob' ℓb'} {C' : Displayed C oc' ℓc'} + {F : Functor (A ×ᶜ B) C} + (F' : Displayed-functor F (A' ×ᵀᴰ B') C') + where + private + module A = Precategory A + module B = Precategory B + module C = Precategory C + module A' where + open Displayed A' public + open DR A' public + module B' where + open Displayed B' public + open DR B' public + module C' where + open Displayed C' public + open DR C' public + + open Displayed-functor F' + open Cat.Functor.Bifunctor F + + first' : ∀ {a b a' b'} {f : A.Hom a b} {x} {x' : B'.Ob[ x ]} → A'.Hom[ f ] a' b' → C'.Hom[ first f ] (F₀' (a' , x')) (F₀' (b' , x')) + first' f' = F₁' (f' , B'.id') + + second' : ∀ {a b a' b'} {f : B.Hom a b} {x} {x' : A'.Ob[ x ]} → B'.Hom[ f ] a' b' → C'.Hom[ second f ] (F₀' (x' , a')) (F₀' (x' , b')) + second' f' = F₁' (A'.id' , f') + + first-id' : ∀ {a x} {a' : B'.Ob[ a ]} {x' : A'.Ob[ x ]} → first' A'.id' C'.≡[ first-id ] C'.id' {x = F₀' (x' , a')} + first-id' = F-id' + + second-id' : ∀ {a x} {a' : A'.Ob[ a ]} {x' : B'.Ob[ x ]} → second' B'.id' C'.≡[ second-id ] C'.id' {x = F₀' (a' , x')} + second-id' = F-id' + + first∘first' : ∀ {a b c a' b' c'} {x x'} {f : A.Hom b c} {g : A.Hom a b} + → {f' : A'.Hom[ f ] b' c'} {g' : A'.Hom[ g ] a' b'} + → first' {x = x} {x'} (f' A'.∘' g') C'.≡[ first∘first ] first' f' C'.∘' first' g' + first∘first' {f' = f'} {g' = g'} = C'.cast[] $ symP $ + F₁' (f' , B'.id') C'.∘' F₁' (g' , B'.id') C'.≡[]⟨ symP F-∘' ⟩ + F₁' (f' A'.∘' g' , B'.id' B'.∘' B'.id') C'.≡[]⟨ apd (λ _ e → F₁' (f' A'.∘' g' , e)) (B'.idl' _) ⟩ + F₁' (f' A'.∘' g' , B'.id') ∎ + + second∘second' : ∀ {a b c a' b' c'} {x x'} {f : B.Hom b c} {g : B.Hom a b} + → {f' : B'.Hom[ f ] b' c'} {g' : B'.Hom[ g ] a' b'} + → second' {x = x} {x'} (f' B'.∘' g') + C'.≡[ second∘second ] + second' f' C'.∘' second' g' + second∘second' {f' = f'} {g' = g'} = C'.cast[] $ symP $ + F₁' (A'.id' , f') C'.∘' F₁' (A'.id' , g') C'.≡[]⟨ symP F-∘' ⟩ + F₁' (A'.id' A'.∘' A'.id' , f' B'.∘' g') C'.≡[]⟨ apd (λ _ e → F₁' (e , f' B'.∘' g')) (A'.idl' _) ⟩ + F₁' (A'.id' , f' B'.∘' g') ∎ + + Left' : ∀ {y} → B'.Ob[ y ] → Displayed-functor (Left y) A' C' + Left' y' .F₀' x' = F₀' (x' , y') + Left' y' .F₁' = first' + Left' y' .F-id' = F-id' + Left' y' .F-∘' = first∘first' + + Right' : ∀ {x} → A'.Ob[ x ] → Displayed-functor (Right x) B' C' + Right' x .F₀' y' = F₀' (x , y') + Right' x .F₁' = second' + Right' x .F-id' = F-id' + Right' x .F-∘' = second∘second' +``` \ No newline at end of file diff --git a/src/Cat/Displayed/Reasoning.lagda.md b/src/Cat/Displayed/Reasoning.lagda.md index 90d1763b8..f3044e7ae 100644 --- a/src/Cat/Displayed/Reasoning.lagda.md +++ b/src/Cat/Displayed/Reasoning.lagda.md @@ -431,8 +431,27 @@ module _ {f' : Hom[ f ] x' y'} where abstract idr[] : {p : f ∘ id ≡ f} → hom[ p ] (f' ∘' id') ≡ f' idr[] {p = p} = reindex p (idr _) ∙ from-pathp (idr' f') - id-comm[] : {p : id ∘ f ≡ f ∘ id} → hom[ p ] (id' ∘' f') ≡ f' ∘' id' - id-comm[] {p = p} = duplicate _ _ _ ∙ ap hom[] (from-pathp (idl' _)) ∙ from-pathp (symP (idr' _)) + id-comm' : {p : f ∘ id ≡ id ∘ f} → (f' ∘' id') ≡[ p ] id' ∘' f' + id-comm' = cast[] (idr' _ ∙[] symP (idl' _)) + + id-comm[] : (f' ∘' id') ≡[ id-comm ] id' ∘' f' + id-comm[] = id-comm' + + id-comm-sym' : {p : id ∘ f ≡ f ∘ id} → (id' ∘' f') ≡[ p ] f' ∘' id' + id-comm-sym' = cast[] (idl' _ ∙[] symP (idr' _)) + + id-comm-sym[] : (id' ∘' f') ≡[ id-comm-sym ] f' ∘' id' + id-comm-sym[] = id-comm-sym' + + + id2' : ∀ {a} {x : Ob[ a ]} {p : id ∘ id ≡ id} → id' {x = x} ∘' id' ≡[ p ] id' + id2' = cast[] (idl' id') + + id2[] : ∀ {a} {x : Ob[ a ]} → id' {x = x} ∘' id' ≡[ id2 ] id' + id2[] = id2' + + + assoc[] : ∀ {a' : Hom[ a ] y' z'} {b' : Hom[ b ] x' y'} {c' : Hom[ c ] w' x'} From a2ff30712d149b3ccff7aff7b5a16969798f9de2 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Thu, 14 Aug 2025 15:15:55 -0700 Subject: [PATCH 03/24] switch to lagda files --- src/Cat/Bi/Displayed/{Base.agda => Base.lagda.md} | 9 ++++++--- ...playedFunctor.agda => DisplayedFunctor.lagda.md} | 13 +++++-------- 2 files changed, 11 insertions(+), 11 deletions(-) rename src/Cat/Bi/Displayed/{Base.agda => Base.lagda.md} (97%) rename src/Cat/Displayed/Instances/{DisplayedFunctor.agda => DisplayedFunctor.lagda.md} (85%) diff --git a/src/Cat/Bi/Displayed/Base.agda b/src/Cat/Bi/Displayed/Base.lagda.md similarity index 97% rename from src/Cat/Bi/Displayed/Base.agda rename to src/Cat/Bi/Displayed/Base.lagda.md index 5219f593d..73594ca75 100644 --- a/src/Cat/Bi/Displayed/Base.agda +++ b/src/Cat/Bi/Displayed/Base.lagda.md @@ -1,4 +1,5 @@ +```agda open import Cat.Prelude open import Cat.Displayed.Base open import Cat.Instances.Product @@ -294,12 +295,14 @@ Displayed-cat o ℓ o' ℓ' .triangle' {B' = B'} {C' = C'} f' g' = Nat'-path λ module C' = Displayed C' Displayed-cat o ℓ o' ℓ' .pentagon' {B' = B'} {C' = C'} {D' = D'} {E' = E'} f' g' h' i' = Nat'-path λ x' → cast[] $ (f' .F₁' (g' .F₁' (h' .F₁' B'.id')) ∘' id') ∘' (id' ∘' f' .F₁' D'.id' ∘' id') ≡[]⟨ idr' _ ⟩∘'⟨ idl' _ ⟩ - (f' .F₁' (g' .F₁' (h' .F₁' B'.id'))) ∘' (f' .F₁' D'.id' ∘' id') ≡[]⟨ ((apd (λ _ z → f' .F₁' (g' .F₁' z)) (h' .F-id')) ⟩∘'⟨ (idr' _)) ⟩ - (f' .F₁' (g' .F₁' C'.id')) ∘' (f' .F₁' D'.id') ≡[]⟨ ((apd (λ _ → f' .F₁') (g' .F-id') ∙[] f' .F-id') ⟩∘'⟨ f' .F-id') ⟩ - id' ∘' id' ∎ + (f' .F₁' (g' .F₁' (h' .F₁' B'.id'))) ∘' (f' .F₁' D'.id' ∘' id') ≡[]⟨ ((apd (λ _ z → f' .F₁' (g' .F₁' z)) (h' .F-id')) ⟩∘'⟨ (idr' _)) ⟩ + (f' .F₁' (g' .F₁' C'.id')) ∘' (f' .F₁' D'.id') ≡[]⟨ ((apd (λ _ → f' .F₁') (g' .F-id') ∙[] f' .F-id') ⟩∘'⟨ f' .F-id') ⟩ + id' ∘' id' ∎ where open Displayed E' open DR E' module B' = Displayed B' module C' = Displayed C' module D' = Displayed D' + +``` \ No newline at end of file diff --git a/src/Cat/Displayed/Instances/DisplayedFunctor.agda b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md similarity index 85% rename from src/Cat/Displayed/Instances/DisplayedFunctor.agda rename to src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md index 272a25910..ea3c9a68e 100644 --- a/src/Cat/Displayed/Instances/DisplayedFunctor.agda +++ b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md @@ -41,9 +41,9 @@ module _ unquoteDecl lvl = declare-record-hlevel 2 lvl (quote _=[_]=>_) Disp[_,_] .Displayed.id' = idnt' Disp[_,_] .Displayed._∘'_ = _∘nt'_ - Disp[_,_] .Displayed.idr' _ = Nat'-pathp refl refl (Cat[A,B].idr _) refl refl λ x' → E.idr' _ - Disp[_,_] .Displayed.idl' _ = Nat'-pathp refl refl (Cat[A,B].idl _) refl refl λ x' → E.idl' _ - Disp[_,_] .Displayed.assoc' _ _ _ = Nat'-pathp refl refl (Cat[A,B].assoc _ _ _) refl refl λ x' → E.assoc' _ _ _ + Disp[_,_] .Displayed.idr' _ = Nat'-path λ x' → E.idr' _ + Disp[_,_] .Displayed.idl' _ = Nat'-path λ x' → E.idl' _ + Disp[_,_] .Displayed.assoc' _ _ _ = Nat'-path λ x' → E.assoc' _ _ _ module _ @@ -89,12 +89,9 @@ module _ F∘'-functor .F₀' (F' , G') = F' F∘' G' F∘'-functor .F₁' (α' , β') = α' ◆' β' F∘'-functor .F-id' {F , G} {F' , G'} = - Nat'-pathp refl refl _ refl refl - λ x' → C'.idr' _ C'.∙[] F' .F-id' + Nat'-path λ x' → C'.idr' _ C'.∙[] F' .F-id' F∘'-functor .F-∘' {a' = F' , G'} {H' , I'} {J' , K'} {α' , _} {β' , _} = - Nat'-pathp refl refl _ refl refl - λ x' → - -- This is just using the same combinators as the F∘-functor proof, but displayed + Nat'-path λ x' → pushl[] _ (J' .F-∘') C'.∙[] ((extend-inner' _ (symP (α' .is-natural' _ _ _))) C'.∙[] (pulll' refl refl)) From 3368bf8d6ff44ffa7ba05e760696607942f23965 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Thu, 14 Aug 2025 15:36:19 -0700 Subject: [PATCH 04/24] some prose --- src/Cat/Displayed/Functor.lagda.md | 25 ++++++---- .../Instances/DisplayedFunctor.lagda.md | 49 ++++++++++++------- .../Displayed/Instances/TotalProduct.lagda.md | 8 +-- 3 files changed, 52 insertions(+), 30 deletions(-) diff --git a/src/Cat/Displayed/Functor.lagda.md b/src/Cat/Displayed/Functor.lagda.md index 4d4451a89..ba3775eb9 100644 --- a/src/Cat/Displayed/Functor.lagda.md +++ b/src/Cat/Displayed/Functor.lagda.md @@ -513,13 +513,6 @@ module → η' y' ℱ.∘' F' .F₁' f' ℱ.≡[ α .is-natural x y f ] G' .F₁' f' ℱ.∘' η' x' ``` -::: {.definition #vertical-natural-transformation} -Let $F, G : \cE \to \cF$ be two vertical functors. A displayed natural -transformation between $F$ and $G$ is called a **vertical natural -transformation** if all components of the natural transformation are -vertical. -::: - +We can define displayed versions of the indentity natural transformation and +composition of natural transformations. +```agda idnt' : ∀ {F : Functor A B} {F' : Displayed-functor F D E} → F' =[ idnt ]=> F' idnt' .η' x' = E.id' idnt' .is-natural' x' y' f' = E.id-comm-sym[] @@ -588,9 +585,17 @@ module _ module F' = Displayed-functor F' module G' = Displayed-functor G' module H' = Displayed-functor H' +``` +--> +::: {.definition #vertical-natural-transformation} +Let $F, G : \cE \to \cF$ be two vertical functors. A displayed natural +transformation between $F$ and $G$ is called a **vertical natural +transformation** if all components of the natural transformation are +vertical. +::: - - + +```agda module Cat.Displayed.Instances.DisplayedFunctor where - - +``` + +Given two displayed categories $\cD \liesover \cA$ and $\cE \liesover \cB$, we +can assemble them into a displayed category $$[\cD, \cE] \liesover [\cA, \cB]$. +The construction mirrors the construction of ordinary functor categories, +using displayed versions of all the same data. + +```agda Disp[_,_] : Displayed (Cat[ A , B ]) _ _ Disp[_,_] .Displayed.Ob[_] f = Displayed-functor f D E Disp[_,_] .Displayed.Hom[_] α F' G' = F' =[ α ]=> G' @@ -44,8 +50,9 @@ module _ Disp[_,_] .Displayed.idr' _ = Nat'-path λ x' → E.idr' _ Disp[_,_] .Displayed.idl' _ = Nat'-path λ x' → E.idl' _ Disp[_,_] .Displayed.assoc' _ _ _ = Nat'-path λ x' → E.assoc' _ _ _ - - +``` + +We can also construct a displayed version of the functor composition functor. +First we'll define displayed horizontal composition of natural transformations. +```agda _◆'_ : F' =[ α ]=> G' → H' =[ β ]=> K' → F' F∘' H' =[ α ◆ β ]=> G' F∘' K' (α' ◆' β') .η' x' = G' .F₁' (β' .η' _) C'.∘' α' .η' _ @@ -72,8 +84,9 @@ module _ (G' .F₁' (K' .F₁' f') ∘' G' .F₁' (β' .η' x')) ∘' α' .η' (H' .F₀' x') ≡[]˘⟨ assoc' _ _ _ ⟩ G' .F₁' (K' .F₁' f') ∘' G' .F₁' (β' .η' x') ∘' α' .η' (H' .F₀' x') ∎ where open C' - - +``` + +Armed with this, we can define our displayed composition functor. +```agda F∘'-functor : Displayed-functor F∘-functor (Disp[ B' , C' ] ×ᵀᴰ Disp[ A' , B' ]) Disp[ A' , C' ] F∘'-functor .F₀' (F' , G') = F' F∘' G' F∘'-functor .F₁' (α' , β') = α' ◆' β' @@ -96,6 +113,4 @@ module _ ((extend-inner' _ (symP (α' .is-natural' _ _ _))) C'.∙[] (pulll' refl refl)) where open DR C' - - - +``` \ No newline at end of file diff --git a/src/Cat/Displayed/Instances/TotalProduct.lagda.md b/src/Cat/Displayed/Instances/TotalProduct.lagda.md index 8433e6ba4..394c73435 100644 --- a/src/Cat/Displayed/Instances/TotalProduct.lagda.md +++ b/src/Cat/Displayed/Instances/TotalProduct.lagda.md @@ -78,9 +78,8 @@ they hold for the components of the ordered pairs. _×ᵀᴰ_ .Displayed.assoc' (f₁ , f₂) (g₁ , g₂) (h₁ , h₂) = EC.assoc' f₁ g₁ h₁ ,ₚ ED.assoc' f₂ g₂ h₂ ``` - + +Using the total product can define displayed versions of these familiar bifunctor constructions. +```agda first' : ∀ {a b a' b'} {f : A.Hom a b} {x} {x' : B'.Ob[ x ]} → A'.Hom[ f ] a' b' → C'.Hom[ first f ] (F₀' (a' , x')) (F₀' (b' , x')) first' f' = F₁' (f' , B'.id') From 9bb604848cbefee2d689529243ed8e6498c7e30e Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Thu, 14 Aug 2025 15:57:20 -0700 Subject: [PATCH 05/24] more prose --- src/Cat/Bi/Displayed/Base.lagda.md | 79 ++++++++++++++++++++---------- 1 file changed, 52 insertions(+), 27 deletions(-) diff --git a/src/Cat/Bi/Displayed/Base.lagda.md b/src/Cat/Bi/Displayed/Base.lagda.md index 73594ca75..46b0cbc6c 100644 --- a/src/Cat/Bi/Displayed/Base.lagda.md +++ b/src/Cat/Bi/Displayed/Base.lagda.md @@ -1,4 +1,4 @@ - + +```agda module Cat.Bi.Displayed.Base where - +``` + +Just as a displayed category $\cE \liesover \cB$ allows us to describe categorical structure over the category $\cB$, a +displayed _bi_category $\bf{E} \liesover \bf{B}$ allows us to describe _bi_categorical structure over the _bi_category $\bf{B}$. +```agda record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type (lsuc (o' ⊔ oh' ⊔ ℓh') ⊔ o ⊔ oh ⊔ ℓh) where - no-eta-equality - open Prebicategory B +``` +For each object of the base bicateogry, we have a type of displayed objects indexed over it. +```agda field Ob[_] : Ob → Type o' +``` +For any two displayed objects, we have a category displayed over the $\hom$ category of their bases. +```agda Hom[_,_] : ∀ {A B} → Ob[ A ] → Ob[ B ] → Displayed (Hom A B) oh' ℓh' module Hom[] {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} = Displayed (Hom[ A' , B' ]) - - +``` +The displayed objects of these displayed $\hom$ categories are the _displayed 1-cells_. +The displayed morphims are the _displayed 2-cells_. +```agda _[_]↦_ : ∀ {A B} → Ob[ A ] → (A ↦ B) → Ob[ B ] → Type _ A' [ f ]↦ B' = Hom[ A' , B' ] .Displayed.Ob[_] f @@ -81,27 +97,33 @@ record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type → A' [ f ]↦ B' → (f ⇒ g) → A' [ g ]↦ B' → Type _ _[_]⇒_ {A' = A'} {B' = B'} f' α g' = Hom[ A' , B' ] .Displayed.Hom[_] α f' g' - - +``` +We require an indentity 1-cell displayed over the identity 1-cell of the base bicategory. +```agda field ↦id' : ∀ {x} {x' : Ob[ x ]} → x' [ id ]↦ x' - +``` +We get displayed identity 2-cells automatically from the displayed $\hom$ structure. +```agda ⇒id' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → {f : A ↦ B} {f' : A' [ f ]↦ B'} → f' [ Hom.id ]⇒ f' ⇒id' = Hom[].id' - +``` +The displayed composition functor is between total products of displayed $\hom$ categories, and +lies over the composition functor of the base bicategory. +```agda field compose' : ∀ {A B C} {A' : Ob[ A ]} {B' : Ob[ B ]} {C' : Ob[ C ]} → Displayed-functor compose (Hom[ B' , C' ] ×ᵀᴰ Hom[ A' , B' ]) Hom[ A' , C' ] module compose' {A} {B} {C} {A'} {B'} {C'} = Displayed-functor (compose' {A} {B} {C} {A'} {B'} {C'}) - - -- Displayed 1-cell composition +``` +Displayed 1-cell and 2-cell composition proceeds in the same way. +```agda _⊗'_ : ∀ {A B C A' B' C'} {f : B ↦ C} {g : A ↦ B} → (B' [ f ]↦ C') → (A' [ g ]↦ B') → A' [ f ⊗ g ]↦ C' _⊗'_ f' g' = compose' · (f' , g') - -- Vertical displayed 2-cell composition _∘'_ : ∀ {A B A' B'} {f g h : A ↦ B} → {f' : A' [ f ]↦ B'} {g' : A' [ g ]↦ B'} {h' : A' [ h ]↦ B'} → {β : g ⇒ h} {α : f ⇒ g} @@ -109,8 +131,6 @@ record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type → f' [ β ∘ α ]⇒ h' _∘'_ = Hom[]._∘'_ - - -- Horizontal displayed 2-cell composition _◆'_ : ∀ {A B C A' B' C'} → {f₁ f₂ : B ↦ C} {β : f₁ ⇒ f₂} → {g₁ g₂ : A ↦ B} {α : g₁ ⇒ g₂} @@ -124,8 +144,6 @@ record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type infixr 25 _⊗'_ infix 35 _◀'_ _▶'_ - - -- Displayed whiskering on the right _▶'_ : ∀ {A B C A' B' C'} {f : B ↦ C} {g₁ g₂ : A ↦ B} {α : g₁ ⇒ g₂} → {g₁' : A' [ g₁ ]↦ B'} {g₂' : A' [ g₂ ]↦ B'} → (f' : B' [ f ]↦ C') @@ -134,7 +152,6 @@ record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type _▶'_ f' α' = compose'.₁' (⇒id' , α') - -- Displayed whiskering on the left _◀'_ : ∀ {A B C A' B' C'} {g : A ↦ B} {f₁ f₂ : B ↦ C} {β : f₁ ⇒ f₂} → {f₁' : B' [ f₁ ]↦ C'} {f₂' : B' [ f₂ ]↦ C'} → (β' : f₁' [ β ]⇒ f₂') @@ -142,7 +159,9 @@ record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type → f₁' ⊗' g' [ β ◀ g ]⇒ f₂' ⊗' g' _◀'_ β' g' = compose'.₁' (β' , ⇒id') - +``` +The unitors and associator are displayed isomorphims over the unitors and associator the base bicategory. +```agda -- Displayed unitor and associator isos field unitor-l' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → _≅[_]_ Disp[ Hom[ A' , B' ] , Hom[ A' , B' ] ] Id' unitor-l (Right' compose' ↦id') @@ -151,10 +170,9 @@ record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type associator' : ∀ {A B C D} {A' : Ob[ A ]} {B' : Ob[ B ]} {C' : Ob[ C ]} {D' : Ob[ D ]} → _≅[_]_ Disp[ Hom[ C' , D' ] ×ᵀᴰ (Hom[ B' , C' ] ×ᵀᴰ Hom[ A' , B' ]) , Hom[ A' , D' ] ] (compose-assocˡ' {H' = Hom[_,_]} compose') associator (compose-assocʳ' {H' = Hom[_,_]} compose') - - -- Displayed versions of all the morphism combinators - -- The naturality types are crazy lol - +``` +The associated displayed cell combinators proceed in the same way. +```agda λ←' : ∀ {A B A' B'} {f : A ↦ B} (f' : A' [ f ]↦ B') → (↦id' ⊗' f') [ λ← f ]⇒ f' λ←' = unitor-l' ._≅[_]_.from' .η' @@ -232,7 +250,9 @@ record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type ((β' ◆' (γ' ◆' δ')) ∘' α→' _ _ _) α→nat' β' γ' δ' = associator' .to' .is-natural' (_ , _ , _) (_ , _ , _) (β' , γ' , δ') - +``` +As do the triangle and pentagon identities. +```agda field triangle' : ∀ {A B C A' B' C'} {f : B ↦ C} {g : A ↦ B} @@ -249,11 +269,17 @@ record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type → ((α←' f' g' h' ◀' i') ∘' α←' f' (g' ⊗' h') i' ∘' (f' ▶' α←' g' h' i')) Hom[].≡[ pentagon f g h i ] (α←' (f' ⊗' g') h' i' ∘' α←' f' g' (h' ⊗' i')) +``` +## The displayed bicategory of displayed categories --- Lets define the displayed bicategory of displayed categories! - +Displayed categories naturally assemble into a displayed biacategory over $\bf{Cat}$. + +```agda Displayed-cat : ∀ o ℓ o' ℓ' → Bidisplayed (Cat o ℓ) _ _ _ Displayed-cat o ℓ o' ℓ' .Ob[_] C = Displayed C o' ℓ' Displayed-cat o ℓ o' ℓ' .Hom[_,_] D E = Disp[ D , E ] @@ -304,5 +330,4 @@ Displayed-cat o ℓ o' ℓ' .pentagon' {B' = B'} {C' = C'} {D' = D'} {E' = E'} f module B' = Displayed B' module C' = Displayed C' module D' = Displayed D' - ``` \ No newline at end of file From e26a01be856008d789b5ecd3f5544c9cbbcdbb60 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Thu, 14 Aug 2025 16:09:12 -0700 Subject: [PATCH 06/24] import sorting --- src/Cat/Bi/Displayed/Base.lagda.md | 24 ++++---- .../{Naturality.agda => Naturality.lagda.md} | 61 ++++++------------- .../Instances/DisplayedFunctor.lagda.md | 11 ++-- .../Displayed/Instances/TotalProduct.lagda.md | 8 +-- 4 files changed, 43 insertions(+), 61 deletions(-) rename src/Cat/Displayed/Functor/{Naturality.agda => Naturality.lagda.md} (77%) diff --git a/src/Cat/Bi/Displayed/Base.lagda.md b/src/Cat/Bi/Displayed/Base.lagda.md index 46b0cbc6c..973a86e96 100644 --- a/src/Cat/Bi/Displayed/Base.lagda.md +++ b/src/Cat/Bi/Displayed/Base.lagda.md @@ -1,18 +1,18 @@ ```agda @@ -73,6 +73,8 @@ displayed _bi_category $\bf{E} \liesover \bf{B}$ allows us to describe _bi_categ ```agda record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type (lsuc (o' ⊔ oh' ⊔ ℓh') ⊔ o ⊔ oh ⊔ ℓh) where + no-eta-equality + open Prebicategory B ``` For each object of the base bicateogry, we have a type of displayed objects indexed over it. ```agda @@ -330,4 +332,4 @@ Displayed-cat o ℓ o' ℓ' .pentagon' {B' = B'} {C' = C'} {D' = D'} {E' = E'} f module B' = Displayed B' module C' = Displayed C' module D' = Displayed D' -``` \ No newline at end of file +``` diff --git a/src/Cat/Displayed/Functor/Naturality.agda b/src/Cat/Displayed/Functor/Naturality.lagda.md similarity index 77% rename from src/Cat/Displayed/Functor/Naturality.agda rename to src/Cat/Displayed/Functor/Naturality.lagda.md index 73969f445..47cc3294a 100644 --- a/src/Cat/Displayed/Functor/Naturality.agda +++ b/src/Cat/Displayed/Functor/Naturality.lagda.md @@ -1,17 +1,22 @@ - -open import Cat.Prelude -open import Cat.Displayed.Base -open import Cat.Displayed.Functor + +We define displayed versions of the our functor naturality tech. +```agda module Cat.Displayed.Functor.Naturality where - +``` + +```agda _≅[_]ⁿ_ : {F G : Functor B C} → Displayed-functor F D E → F ≅ⁿ G → Displayed-functor G D E → Type _ F ≅[ i ]ⁿ G = F DE.≅[ i ] G @@ -86,37 +93,9 @@ module _ ; from' = record { η' = mk .inv' ; is-natural' = inverse-is-natural' i to' (mk .inv') (mk .eta∘inv') (mk .inv∘eta') } ; inverses' = record { invl' = Nat'-path (mk .eta∘inv') ; invr' = Nat'-path (mk .inv∘eta') } } - +``` + \ No newline at end of file diff --git a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md index c99af081c..895d3d878 100644 --- a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md +++ b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md @@ -1,13 +1,14 @@ ```agda @@ -113,4 +114,4 @@ Armed with this, we can define our displayed composition functor. ((extend-inner' _ (symP (α' .is-natural' _ _ _))) C'.∙[] (pulll' refl refl)) where open DR C' -``` \ No newline at end of file +``` diff --git a/src/Cat/Displayed/Instances/TotalProduct.lagda.md b/src/Cat/Displayed/Instances/TotalProduct.lagda.md index 394c73435..fc2e6d0ac 100644 --- a/src/Cat/Displayed/Instances/TotalProduct.lagda.md +++ b/src/Cat/Displayed/Instances/TotalProduct.lagda.md @@ -5,16 +5,16 @@ open import 1Lab.HLevel.Closure open import 1Lab.Type.Sigma open import Cat.Instances.Sets.Complete +open import Cat.Displayed.Functor open import Cat.Instances.Product open import Cat.Diagram.Product open import Cat.Displayed.Base open import Cat.Instances.Sets open import Cat.Prelude open import Cat.Base -open import Cat.Displayed.Functor -import Cat.Functor.Bifunctor -import Cat.Displayed.Reasoning as DR +import Cat.Displayed.Reasoning as DR +import Cat.Functor.Bifunctor ``` --> @@ -148,4 +148,4 @@ Using the total product can define displayed versions of these familiar bifuncto Right' x .F₁' = second' Right' x .F-id' = F-id' Right' x .F-∘' = second∘second' -``` \ No newline at end of file +``` From f9b955923f7477cfe5109198e3fc1df5dae961b6 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Thu, 14 Aug 2025 16:53:21 -0700 Subject: [PATCH 07/24] headers and whatnot --- src/Cat/Bi/Base.lagda.md | 2 ++ src/Cat/Bi/Displayed/Base.lagda.md | 7 +++++++ src/Cat/Bi/Instances/Displayed.lagda.md | 12 ++++++------ src/Cat/Displayed/Functor/Naturality.lagda.md | 5 ++++- src/Cat/Displayed/Instances/TotalProduct.lagda.md | 2 +- 5 files changed, 20 insertions(+), 8 deletions(-) diff --git a/src/Cat/Bi/Base.lagda.md b/src/Cat/Bi/Base.lagda.md index 602b91e2d..ae18a217d 100644 --- a/src/Cat/Bi/Base.lagda.md +++ b/src/Cat/Bi/Base.lagda.md @@ -190,6 +190,8 @@ naturally isomorphic to the identity functor. (compose-assocˡ {H = Hom} compose) (compose-assocʳ {H = Hom} compose) + module unitor-l {a} {b} = Cr._≅_ _ (unitor-l {a} {b}) + module unitor-r {a} {b} = Cr._≅_ _ (unitor-r {a} {b}) module associator {a} {b} {c} {d} = Cr._≅_ _ (associator {a} {b} {c} {d}) ``` diff --git a/src/Cat/Bi/Displayed/Base.lagda.md b/src/Cat/Bi/Displayed/Base.lagda.md index 973a86e96..b7c6cb26d 100644 --- a/src/Cat/Bi/Displayed/Base.lagda.md +++ b/src/Cat/Bi/Displayed/Base.lagda.md @@ -68,6 +68,7 @@ module _ where open DR (H' A' D') ``` --> +## Displayed bicategories Just as a displayed category $\cE \liesover \cB$ allows us to describe categorical structure over the category $\cB$, a displayed _bi_category $\bf{E} \liesover \bf{B}$ allows us to describe _bi_categorical structure over the _bi_category $\bf{B}$. @@ -172,6 +173,12 @@ The unitors and associator are displayed isomorphims over the unitors and associ associator' : ∀ {A B C D} {A' : Ob[ A ]} {B' : Ob[ B ]} {C' : Ob[ C ]} {D' : Ob[ D ]} → _≅[_]_ Disp[ Hom[ C' , D' ] ×ᵀᴰ (Hom[ B' , C' ] ×ᵀᴰ Hom[ A' , B' ]) , Hom[ A' , D' ] ] (compose-assocˡ' {H' = Hom[_,_]} compose') associator (compose-assocʳ' {H' = Hom[_,_]} compose') + + module unitor-l' {A} {B} {A'} {B'} = _≅[_]_ (unitor-l' {A} {B} {A'} {B'}) + module unitor-r' {A} {B} {A'} {B'} = _≅[_]_ (unitor-r' {A} {B} {A'} {B'}) + module associator' {A} {B} {C} {D} {A'} {B'} {C'} {D'} = _≅[_]_ (associator' {A} {B} {C} {D} {A'} {B'} {C'} {D'}) + + ``` The associated displayed cell combinators proceed in the same way. ```agda diff --git a/src/Cat/Bi/Instances/Displayed.lagda.md b/src/Cat/Bi/Instances/Displayed.lagda.md index f95fc10ea..80a2321e5 100644 --- a/src/Cat/Bi/Instances/Displayed.lagda.md +++ b/src/Cat/Bi/Instances/Displayed.lagda.md @@ -106,8 +106,8 @@ as in the nondisplayed case. module D' {x} = Cat (Fibre D x) using (_∘_ ; idl ; idr ; elimr ; pushl ; introl) ni : make-natural-iso {D = Vf _ _} _ _ - ni .eta _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] D) } - ni .inv _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] D) } + ni .eta _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → Disp.id-comm-sym[] D } + ni .inv _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → Disp.id-comm-sym[] D } ni .eta∘inv _ = ext λ _ → D'.idl _ ni .inv∘eta _ = ext λ _ → D'.idl _ ni .natural x y f = ext λ _ → D'.idr _ ∙∙ D'.pushl (F-∘↓ (y .fst)) ∙∙ D'.introl refl @@ -127,8 +127,8 @@ the structural isomorphisms being identities. Disp[] .unitor-l {B = B} = to-natural-iso ni where module B = Displayed B ni : make-natural-iso {D = Vf _ _} _ _ - ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] B) } - ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] B) } + ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → Disp.id-comm-sym[] B } + ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → Disp.id-comm-sym[] B } ni .eta∘inv _ = ext λ _ → Cat.idl (Fibre B _) _ ni .inv∘eta _ = ext λ _ → Cat.idl (Fibre B _) _ ni .natural x y f = ext λ _ → Cat.elimr (Fibre B _) refl ∙ Cat.id-comm (Fibre B _) @@ -137,8 +137,8 @@ the structural isomorphisms being identities. module B' {x} = Cat (Fibre B x) using (_∘_ ; idl ; elimr) ni : make-natural-iso {D = Vf _ _} _ _ - ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] B) } - ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] B) } + ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → Disp.id-comm-sym[] B } + ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → Disp.id-comm-sym[] B } ni .eta∘inv _ = ext λ _ → B'.idl _ ni .inv∘eta _ = ext λ _ → B'.idl _ ni .natural x y f = ext λ _ → B'.elimr refl ∙ ap₂ B'._∘_ (y .F-id') refl diff --git a/src/Cat/Displayed/Functor/Naturality.lagda.md b/src/Cat/Displayed/Functor/Naturality.lagda.md index 47cc3294a..cf7f58106 100644 --- a/src/Cat/Displayed/Functor/Naturality.lagda.md +++ b/src/Cat/Displayed/Functor/Naturality.lagda.md @@ -11,10 +11,13 @@ import Cat.Displayed.Reasoning as DR import Cat.Displayed.Morphism as DM ``` --> -We define displayed versions of the our functor naturality tech. ```agda module Cat.Displayed.Functor.Naturality where ``` +## Natural isomorhisms of displayed functors + +We define displayed versions of our functor naturality tech. + -Using the total product can define displayed versions of these familiar bifunctor constructions. +Using the total product we can define displayed versions of these familiar bifunctor constructions. ```agda first' : ∀ {a b a' b'} {f : A.Hom a b} {x} {x' : B'.Ob[ x ]} → A'.Hom[ f ] a' b' → C'.Hom[ first f ] (F₀' (a' , x')) (F₀' (b' , x')) first' f' = F₁' (f' , B'.id') From 6f56a4755603109be0c68705e6ef90ef71c45121 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Tue, 19 Aug 2025 19:56:05 -0700 Subject: [PATCH 08/24] fix some typos --- src/Cat/Bi/Displayed/Base.lagda.md | 10 +++++----- src/Cat/Displayed/Functor.lagda.md | 2 +- src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md | 1 + 3 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Cat/Bi/Displayed/Base.lagda.md b/src/Cat/Bi/Displayed/Base.lagda.md index b7c6cb26d..e26ab3450 100644 --- a/src/Cat/Bi/Displayed/Base.lagda.md +++ b/src/Cat/Bi/Displayed/Base.lagda.md @@ -70,7 +70,7 @@ module _ where --> ## Displayed bicategories Just as a displayed category $\cE \liesover \cB$ allows us to describe categorical structure over the category $\cB$, a -displayed _bi_category $\bf{E} \liesover \bf{B}$ allows us to describe _bi_categorical structure over the _bi_category $\bf{B}$. +displayed *bi*category $\bf{E} \liesover \bf{B}$ allows us to describe *bi*categorical structure over the *bi*category $\bf{B}$. ```agda record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type (lsuc (o' ⊔ oh' ⊔ ℓh') ⊔ o ⊔ oh ⊔ ℓh) where @@ -118,14 +118,14 @@ lies over the composition functor of the base bicategory. ```agda field compose' : ∀ {A B C} {A' : Ob[ A ]} {B' : Ob[ B ]} {C' : Ob[ C ]} - → Displayed-functor compose (Hom[ B' , C' ] ×ᵀᴰ Hom[ A' , B' ]) Hom[ A' , C' ] + → Displayed-functor compose (Hom[ B' , C' ] ×ᵀᴰ Hom[ A' , B' ]) Hom[ A' , C' ] module compose' {A} {B} {C} {A'} {B'} {C'} = Displayed-functor (compose' {A} {B} {C} {A'} {B'} {C'}) ``` Displayed 1-cell and 2-cell composition proceeds in the same way. ```agda _⊗'_ : ∀ {A B C A' B' C'} {f : B ↦ C} {g : A ↦ B} → (B' [ f ]↦ C') → (A' [ g ]↦ B') → A' [ f ⊗ g ]↦ C' - _⊗'_ f' g' = compose' · (f' , g') + _⊗'_ f' g' = compose'.₀' (f' , g') _∘'_ : ∀ {A B A' B'} {f g h : A ↦ B} → {f' : A' [ f ]↦ B'} {g' : A' [ g ]↦ B'} {h' : A' [ h ]↦ B'} @@ -165,7 +165,6 @@ Displayed 1-cell and 2-cell composition proceeds in the same way. ``` The unitors and associator are displayed isomorphims over the unitors and associator the base bicategory. ```agda - -- Displayed unitor and associator isos field unitor-l' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → _≅[_]_ Disp[ Hom[ A' , B' ] , Hom[ A' , B' ] ] Id' unitor-l (Right' compose' ↦id') unitor-r' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → _≅[_]_ Disp[ Hom[ A' , B' ] , Hom[ A' , B' ] ] Id' unitor-r (Left' compose' ↦id') @@ -180,7 +179,7 @@ The unitors and associator are displayed isomorphims over the unitors and associ ``` -The associated displayed cell combinators proceed in the same way. +The associated displayed cell combinators proceed in the same way. Fair warning: the types get pretty nasty. ```agda λ←' : ∀ {A B A' B'} {f : A ↦ B} (f' : A' [ f ]↦ B') → (↦id' ⊗' f') [ λ← f ]⇒ f' λ←' = unitor-l' ._≅[_]_.from' .η' @@ -282,6 +281,7 @@ As do the triangle and pentagon identities. ## The displayed bicategory of displayed categories + Displayed categories naturally assemble into a displayed biacategory over $\bf{Cat}$. + ::: {.definition #vertical-natural-transformation} Let $F, G : \cE \to \cF$ be two vertical functors. A displayed natural transformation between $F$ and $G$ is called a **vertical natural diff --git a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md index 895d3d878..5c45172c0 100644 --- a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md +++ b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md @@ -14,6 +14,7 @@ import Cat.Displayed.Reasoning as DR ```agda module Cat.Displayed.Instances.DisplayedFunctor where ``` +## Displayed functor categories Given two displayed categories $\cD \liesover \cA$ and $\cE \liesover \cB$, we can assemble them into a displayed category $$[\cD, \cE] \liesover [\cA, \cB]$. From e3876db2779a838c14626fdd6fac497e97b35a0f Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Tue, 19 Aug 2025 19:59:29 -0700 Subject: [PATCH 09/24] remove unused function --- src/Cat/Displayed/Functor.lagda.md | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/src/Cat/Displayed/Functor.lagda.md b/src/Cat/Displayed/Functor.lagda.md index f5d9432c2..8559788ad 100644 --- a/src/Cat/Displayed/Functor.lagda.md +++ b/src/Cat/Displayed/Functor.lagda.md @@ -424,20 +424,6 @@ module → F ≡ G Vertical-functor-path = Displayed-functor-pathp refl - Vertical-functor-path-prop - : {F G : Vertical-functor ℰ ℱ} - → (∀ {x y x' y'} {f : B.Hom x y} → is-prop (ℱ.Hom[ f ] x' y')) - → (p0 : ∀ {x} → (x' : ℰ.Ob[ x ]) → F .F₀' x' ≡ G .F₀' x') - → F ≡ G - Vertical-functor-path-prop prop p0 = Vertical-functor-path p0 (λ _ → is-prop→pathp (λ _ → prop) _ _) - - Vertical-functor-path-prop! - : {F G : Vertical-functor ℰ ℱ} - → ⦃ _ : ∀ {x y x' y'} {f : B.Hom x y} → H-Level (ℱ.Hom[ f ] x' y') 1 ⦄ - → (p0 : ∀ {x} → (x' : ℰ.Ob[ x ]) → F .F₀' x' ≡ G .F₀' x') - → F ≡ G - Vertical-functor-path-prop! = Vertical-functor-path-prop (hlevel 1) - Vertical-functor-is-set : (∀ x → is-set ℱ.Ob[ x ]) → is-set (Vertical-functor ℰ ℱ) Vertical-functor-is-set fibre-set = Displayed-functor-is-set fibre-set ``` From 4ae2872aa32b0f48dbedeaa0f2df7767ffdf9d87 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Tue, 19 Aug 2025 20:04:57 -0700 Subject: [PATCH 10/24] update headers --- src/Cat/Bi/Displayed/Base.lagda.md | 5 +++-- src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Cat/Bi/Displayed/Base.lagda.md b/src/Cat/Bi/Displayed/Base.lagda.md index e26ab3450..1ff826676 100644 --- a/src/Cat/Bi/Displayed/Base.lagda.md +++ b/src/Cat/Bi/Displayed/Base.lagda.md @@ -68,9 +68,10 @@ module _ where open DR (H' A' D') ``` --> -## Displayed bicategories +# Displayed bicategories {defines=displayed-bicategory} + Just as a displayed category $\cE \liesover \cB$ allows us to describe categorical structure over the category $\cB$, a -displayed *bi*category $\bf{E} \liesover \bf{B}$ allows us to describe *bi*categorical structure over the *bi*category $\bf{B}$. +**displayed bicategory** $\bf{E} \liesover \bf{B}$ allows us to describe *bi*categorical structure over the *bi*category $\bf{B}$. ```agda record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type (lsuc (o' ⊔ oh' ⊔ ℓh') ⊔ o ⊔ oh ⊔ ℓh) where diff --git a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md index 5c45172c0..e960b5a95 100644 --- a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md +++ b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md @@ -14,7 +14,7 @@ import Cat.Displayed.Reasoning as DR ```agda module Cat.Displayed.Instances.DisplayedFunctor where ``` -## Displayed functor categories +# Displayed functor categories {defines=displayed-functor-category} Given two displayed categories $\cD \liesover \cA$ and $\cE \liesover \cB$, we can assemble them into a displayed category $$[\cD, \cE] \liesover [\cA, \cB]$. From 8f5326265b7a5839193095665d33921f2833a18f Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Tue, 19 Aug 2025 20:36:41 -0700 Subject: [PATCH 11/24] nicer links --- src/Cat/Bi/Displayed/Base.lagda.md | 22 ++++++++++++++----- src/Cat/Displayed/Functor.lagda.md | 2 ++ .../Instances/DisplayedFunctor.lagda.md | 12 ++++++---- src/Cat/Functor/Compose.lagda.md | 2 ++ 4 files changed, 28 insertions(+), 10 deletions(-) diff --git a/src/Cat/Bi/Displayed/Base.lagda.md b/src/Cat/Bi/Displayed/Base.lagda.md index 1ff826676..9f89f937b 100644 --- a/src/Cat/Bi/Displayed/Base.lagda.md +++ b/src/Cat/Bi/Displayed/Base.lagda.md @@ -18,6 +18,19 @@ import Cat.Displayed.Reasoning as DR ```agda module Cat.Bi.Displayed.Base where ``` + +# Displayed bicategories {defines=displayed-bicategory} + +::: source +The definition here was adapted from the one given by Ahrens et al. +in the paper [Bicategories in Univalent Foundations] +::: + +[Bicategories in Univalent Foundations]: https://arxiv.org/abs/1903.01152 + +Just as a displayed category $\cE \liesover \cB$ allows us to describe categorical structure over the category $\cB$, a +**displayed bicategory** $\bf{E} \liesover \bf{B}$ allows us to describe *bi*categorical structure over the *bi*category $\bf{B}$. + -# Displayed bicategories {defines=displayed-bicategory} - -Just as a displayed category $\cE \liesover \cB$ allows us to describe categorical structure over the category $\cB$, a -**displayed bicategory** $\bf{E} \liesover \bf{B}$ allows us to describe *bi*categorical structure over the *bi*category $\bf{B}$. ```agda record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type (lsuc (o' ⊔ oh' ⊔ ℓh') ⊔ o ⊔ oh ⊔ ℓh) where @@ -102,7 +111,7 @@ The displayed morphims are the _displayed 2-cells_. → Type _ _[_]⇒_ {A' = A'} {B' = B'} f' α g' = Hom[ A' , B' ] .Displayed.Hom[_] α f' g' ``` -We require an indentity 1-cell displayed over the identity 1-cell of the base bicategory. +We require an identity 1-cell displayed over the identity 1-cell of the base bicategory. ```agda field ↦id' : ∀ {x} {x' : Ob[ x ]} → x' [ id ]↦ x' @@ -282,8 +291,9 @@ As do the triangle and pentagon identities. ## The displayed bicategory of displayed categories +Displayed categories naturally assemble into a displayed biacategory over $\bf{Cat}$, +with [[displayed functor categories|displayed-functor-category]] as $\hom$s. -Displayed categories naturally assemble into a displayed biacategory over $\bf{Cat}$. -We can also construct a displayed version of the functor composition functor. + +We can also construct a displayed version of the [[functor composition functor|composition-functor]]. First we'll define displayed horizontal composition of natural transformations. ```agda - _◆'_ : F' =[ α ]=> G' → H' =[ β ]=> K' → F' F∘' H' =[ α ◆ β ]=> G' F∘' K' (α' ◆' β') .η' x' = G' .F₁' (β' .η' _) C'.∘' α' .η' _ (α' ◆' β') .is-natural' x' y' f' = cast[] $ @@ -101,7 +102,10 @@ module _ module C' = Displayed C' ``` --> + +:::{.definition #displayed-composition-functor} Armed with this, we can define our displayed composition functor. +::: ```agda F∘'-functor : Displayed-functor F∘-functor (Disp[ B' , C' ] ×ᵀᴰ Disp[ A' , B' ]) Disp[ A' , C' ] diff --git a/src/Cat/Functor/Compose.lagda.md b/src/Cat/Functor/Compose.lagda.md index 08e8909ad..bdfdc1071 100644 --- a/src/Cat/Functor/Compose.lagda.md +++ b/src/Cat/Functor/Compose.lagda.md @@ -90,7 +90,9 @@ _◆_ {E = E} {F = F} {G} {H} {K} α β = nat module horizontal-comp where ``` --> +:::{.definition #composition-functor} We can now define the composition functor itself. +::: ```agda F∘-functor : Functor (Cat[ B , C ] ×ᶜ Cat[ A , B ]) Cat[ A , C ] From dcdd065ca0817a88b594ae77b256110ab50085ee Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Tue, 19 Aug 2025 20:47:56 -0700 Subject: [PATCH 12/24] remove old comment --- src/Cat/Bi/Displayed/Base.lagda.md | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Cat/Bi/Displayed/Base.lagda.md b/src/Cat/Bi/Displayed/Base.lagda.md index 9f89f937b..f7271f46e 100644 --- a/src/Cat/Bi/Displayed/Base.lagda.md +++ b/src/Cat/Bi/Displayed/Base.lagda.md @@ -1,6 +1,5 @@ @@ -305,7 +301,6 @@ Displayed-cat o ℓ o' ℓ' .Hom[_,_] D E = Disp[ D , E ] Displayed-cat o ℓ o' ℓ' .↦id' = Id' Displayed-cat o ℓ o' ℓ' .compose' = F∘'-functor Displayed-cat o ℓ o' ℓ' .unitor-l' {B' = B'} = to-natural-iso' ni where - open Displayed B' open DR B' ni : make-natural-iso[ _ ] _ _ ni .eta' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[] @@ -315,7 +310,6 @@ Displayed-cat o ℓ o' ℓ' .unitor-l' {B' = B'} = to-natural-iso' ni where ni .natural' x' y' f' = Nat'-path λ x'' → cast[] $ symP $ (idr' _ ∙[] id-comm[]) Displayed-cat o ℓ o' ℓ' .unitor-r' {B' = B'} = to-natural-iso' ni where - open Displayed B' open DR B' ni : make-natural-iso[ _ ] _ _ ni .eta' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[] @@ -325,7 +319,6 @@ Displayed-cat o ℓ o' ℓ' .unitor-r' {B' = B'} = to-natural-iso' ni where ni .natural' x' y' f' = Nat'-path λ x'' → cast[] $ (idl' _ ∙[] symP (idr' _ ∙[] ((y' .F-id' ⟩∘'⟨refl) ∙[] idl' _))) Displayed-cat o ℓ o' ℓ' .associator' {C' = C'} {D' = D'} = to-natural-iso' ni where - open Displayed D' open DR D' module C' = Displayed C' ni : make-natural-iso[ _ ] _ _ @@ -344,7 +337,6 @@ Displayed-cat o ℓ o' ℓ' .pentagon' {B' = B'} {C' = C'} {D' = D'} {E' = E'} f (f' .F₁' (g' .F₁' C'.id')) ∘' (f' .F₁' D'.id') ≡[]⟨ ((apd (λ _ → f' .F₁') (g' .F-id') ∙[] f' .F-id') ⟩∘'⟨ f' .F-id') ⟩ id' ∘' id' ∎ where - open Displayed E' open DR E' module B' = Displayed B' module C' = Displayed C' diff --git a/src/Cat/Displayed/Functor.lagda.md b/src/Cat/Displayed/Functor.lagda.md index 07eb667af..53850aa00 100644 --- a/src/Cat/Displayed/Functor.lagda.md +++ b/src/Cat/Displayed/Functor.lagda.md @@ -504,9 +504,7 @@ module _ module A = Precategory A module B = Precategory B module D = Displayed D - module E where - open Displayed E public - open DR E public + module E = DR E open _=>_ open _=[_]=>_ diff --git a/src/Cat/Displayed/Functor/Naturality.lagda.md b/src/Cat/Displayed/Functor/Naturality.lagda.md index abcd95708..d5b129607 100644 --- a/src/Cat/Displayed/Functor/Naturality.lagda.md +++ b/src/Cat/Displayed/Functor/Naturality.lagda.md @@ -29,15 +29,10 @@ module _ module B = Precategory B module C = Precategory C module DE where - open Displayed Disp[ D , E ] public open DR Disp[ D , E ] public open DM Disp[ D , E ] public - module D where - open Displayed D public - open DR D public - module E where - open Displayed E public - open DR E public + module D = DR D public + module E = DR E public open Functor open _=>_ diff --git a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md index 40c208de7..06fd5f552 100644 --- a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md +++ b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md @@ -38,9 +38,7 @@ module _ module A = CR A module B = CR B module D = Displayed D - module E where - open Displayed E public - open DR E public + module E = DR E ``` --> ```agda @@ -69,9 +67,7 @@ module _ where private module B' = Displayed B' - module C' where - open Displayed C' public - open DR C' public + module C' = DR C' ``` --> diff --git a/src/Cat/Displayed/Instances/TotalProduct.lagda.md b/src/Cat/Displayed/Instances/TotalProduct.lagda.md index 35490fd5e..49c131642 100644 --- a/src/Cat/Displayed/Instances/TotalProduct.lagda.md +++ b/src/Cat/Displayed/Instances/TotalProduct.lagda.md @@ -95,15 +95,9 @@ module _ module A = Precategory A module B = Precategory B module C = Precategory C - module A' where - open Displayed A' public - open DR A' public - module B' where - open Displayed B' public - open DR B' public - module C' where - open Displayed C' public - open DR C' public + module A' = DR A' public + module B' = DR B' public + module C' = DR C' public open Displayed-functor F' open Cat.Functor.Bifunctor F From ed1b1d87985b89e4e5bc776afe8985c72410ea26 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Tue, 19 Aug 2025 21:30:20 -0700 Subject: [PATCH 17/24] remove extra hlevel instance --- src/Cat/Displayed/Functor.lagda.md | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Cat/Displayed/Functor.lagda.md b/src/Cat/Displayed/Functor.lagda.md index 53850aa00..1636c1ace 100644 --- a/src/Cat/Displayed/Functor.lagda.md +++ b/src/Cat/Displayed/Functor.lagda.md @@ -618,9 +618,6 @@ module _ Extensional-=>↓ {F' = F'} {G' = G'} ⦃ e ⦄ = injection→extensional! {f = _=>↓_.η'} (λ p → Iso.injective eqv (Σ-prop-path! p)) e - H-Level-=>↓ : ∀ {F' G'} {n} → H-Level (F' =>↓ G') (2 + n) - H-Level-=>↓ = basic-instance 2 (Iso→is-hlevel 2 eqv (hlevel 2)) - open _=>↓_ idnt↓ : ∀ {F} → F =>↓ F From ca954141d0c4fac242764a572b1b022a5dddec98 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Wed, 20 Aug 2025 23:54:36 -0700 Subject: [PATCH 18/24] use a real citation --- src/Cat/Bi/Displayed/Base.lagda.md | 3 +-- src/Cat/Displayed/Functor/Naturality.lagda.md | 4 ++-- src/Cat/Displayed/Instances/TotalProduct.lagda.md | 6 +++--- src/bibliography.bibtex | 13 +++++++++++++ 4 files changed, 19 insertions(+), 7 deletions(-) diff --git a/src/Cat/Bi/Displayed/Base.lagda.md b/src/Cat/Bi/Displayed/Base.lagda.md index d82ca7f26..f33955e99 100644 --- a/src/Cat/Bi/Displayed/Base.lagda.md +++ b/src/Cat/Bi/Displayed/Base.lagda.md @@ -21,8 +21,7 @@ module Cat.Bi.Displayed.Base where # Displayed bicategories {defines=displayed-bicategory} ::: source -The definition here was adapted from the one given by Ahrens et al. -in [Bicategories in Univalent Foundations] +The definition here was adapted from the one given by Ahrens et al. [-@Ahrens-Frumin-Maggesi-Veltre-vanDerWeide:Bicategories] ::: [Bicategories in Univalent Foundations]: https://arxiv.org/abs/1903.01152 diff --git a/src/Cat/Displayed/Functor/Naturality.lagda.md b/src/Cat/Displayed/Functor/Naturality.lagda.md index d5b129607..617efb53a 100644 --- a/src/Cat/Displayed/Functor/Naturality.lagda.md +++ b/src/Cat/Displayed/Functor/Naturality.lagda.md @@ -31,8 +31,8 @@ module _ module DE where open DR Disp[ D , E ] public open DM Disp[ D , E ] public - module D = DR D public - module E = DR E public + module D = DR D + module E = DR E open Functor open _=>_ diff --git a/src/Cat/Displayed/Instances/TotalProduct.lagda.md b/src/Cat/Displayed/Instances/TotalProduct.lagda.md index 49c131642..eb1acf114 100644 --- a/src/Cat/Displayed/Instances/TotalProduct.lagda.md +++ b/src/Cat/Displayed/Instances/TotalProduct.lagda.md @@ -95,9 +95,9 @@ module _ module A = Precategory A module B = Precategory B module C = Precategory C - module A' = DR A' public - module B' = DR B' public - module C' = DR C' public + module A' = DR A' + module B' = DR B' + module C' = DR C' open Displayed-functor F' open Cat.Functor.Bifunctor F diff --git a/src/bibliography.bibtex b/src/bibliography.bibtex index 14155e0af..a0c3bb171 100644 --- a/src/bibliography.bibtex +++ b/src/bibliography.bibtex @@ -340,3 +340,16 @@ pages = {153–192}, numpages = {40} } + +@article{Ahrens-Frumin-Maggesi-Veltre-vanDerWeide:Bicategories, + title = {Bicategories in univalent foundations}, + author = {Ahrens B, Frumin D, Maggesi M, Veltri N, van der Weide N}, + year = {2022}, + publisher = {Cambridge University Press}, + journal = {Mathematical Structures in Computer Science}, + volume = {31}, + number = {10}, + pages = {1232-1269}, + doi = {10.1017/S0960129522000032}, + url = {https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/bicategories-in-univalent-foundations/8BFCD0A0A5DD385C130DB28BCD5E3F68} +} \ No newline at end of file From 481a21a4a96434714f7bea22a05100ebeeda166a Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Thu, 21 Aug 2025 00:00:09 -0700 Subject: [PATCH 19/24] formatting --- src/Cat/Bi/Displayed/Base.lagda.md | 23 ++++++++++++++++++- src/Cat/Displayed/Functor.lagda.md | 4 +++- src/Cat/Displayed/Functor/Naturality.lagda.md | 6 ++++- .../Instances/DisplayedFunctor.lagda.md | 4 ++++ .../Displayed/Instances/TotalProduct.lagda.md | 3 +++ src/Cat/Displayed/Reasoning.lagda.md | 4 ---- 6 files changed, 37 insertions(+), 7 deletions(-) diff --git a/src/Cat/Bi/Displayed/Base.lagda.md b/src/Cat/Bi/Displayed/Base.lagda.md index f33955e99..5f909422c 100644 --- a/src/Cat/Bi/Displayed/Base.lagda.md +++ b/src/Cat/Bi/Displayed/Base.lagda.md @@ -81,19 +81,25 @@ record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type no-eta-equality open Prebicategory B ``` + For each object of the base bicateogry, we have a type of displayed objects indexed over it. + ```agda field Ob[_] : Ob → Type o' ``` + For any two displayed objects, we have a category displayed over the $\hom$ category of their bases. + ```agda Hom[_,_] : ∀ {A B} → Ob[ A ] → Ob[ B ] → Displayed (Hom A B) oh' ℓh' module Hom[] {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} = Displayed (Hom[ A' , B' ]) ``` + The displayed objects of these displayed $\hom$ categories are the _displayed 1-cells_. The displayed morphims are the _displayed 2-cells_. + ```agda _[_]↦_ : ∀ {A B} → Ob[ A ] → (A ↦ B) → Ob[ B ] → Type _ A' [ f ]↦ B' = Hom[ A' , B' ] .Displayed.Ob[_] f @@ -105,20 +111,26 @@ The displayed morphims are the _displayed 2-cells_. → Type _ _[_]⇒_ {A' = A'} {B' = B'} f' α g' = Hom[ A' , B' ] .Displayed.Hom[_] α f' g' ``` + We require an identity 1-cell displayed over the identity 1-cell of the base bicategory. + ```agda field ↦id' : ∀ {x} {x' : Ob[ x ]} → x' [ id ]↦ x' ``` + We get displayed identity 2-cells automatically from the displayed $\hom$ structure. + ```agda ⇒id' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → {f : A ↦ B} {f' : A' [ f ]↦ B'} → f' [ Hom.id ]⇒ f' ⇒id' = Hom[].id' ``` + The displayed composition functor is between total products of displayed $\hom$ categories, and lies over the composition functor of the base bicategory. + ```agda field compose' : ∀ {A B C} {A' : Ob[ A ]} {B' : Ob[ B ]} {C' : Ob[ C ]} @@ -126,7 +138,9 @@ lies over the composition functor of the base bicategory. module compose' {A} {B} {C} {A'} {B'} {C'} = Displayed-functor (compose' {A} {B} {C} {A'} {B'} {C'}) ``` + Displayed 1-cell and 2-cell composition proceeds in the same way. + ```agda _⊗'_ : ∀ {A B C A' B' C'} {f : B ↦ C} {g : A ↦ B} → (B' [ f ]↦ C') → (A' [ g ]↦ B') → A' [ f ⊗ g ]↦ C' _⊗'_ f' g' = compose'.₀' (f' , g') @@ -167,7 +181,9 @@ Displayed 1-cell and 2-cell composition proceeds in the same way. _◀'_ β' g' = compose'.₁' (β' , ⇒id') ``` + The unitors and associator are displayed isomorphims over the unitors and associator the base bicategory. + ```agda field unitor-l' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → _≅[_]_ Disp[ Hom[ A' , B' ] , Hom[ A' , B' ] ] Id' unitor-l (Right' compose' ↦id') @@ -183,7 +199,9 @@ The unitors and associator are displayed isomorphims over the unitors and associ ``` -The associated displayed cell combinators proceed in the same way. Fair warning: the types get pretty nasty. + +The associated displayed cell combinators proceed in the same way. + ```agda λ←' : ∀ {A B A' B'} {f : A ↦ B} (f' : A' [ f ]↦ B') → (↦id' ⊗' f') [ λ← f ]⇒ f' λ←' = unitor-l' ._≅[_]_.from' .η' @@ -263,7 +281,9 @@ The associated displayed cell combinators proceed in the same way. Fair warning: α→nat' β' γ' δ' = associator' .to' .is-natural' (_ , _ , _) (_ , _ , _) (β' , γ' , δ') ``` + As do the triangle and pentagon identities. + ```agda field triangle' @@ -293,6 +313,7 @@ with [[displayed functor categories|displayed-functor-category]] as $\hom$s. open Bidisplayed hiding (_∘'_) ``` --> + ```agda Displayed-cat : ∀ o ℓ o' ℓ' → Bidisplayed (Cat o ℓ) _ _ _ Displayed-cat o ℓ o' ℓ' .Ob[_] C = Displayed C o' ℓ' diff --git a/src/Cat/Displayed/Functor.lagda.md b/src/Cat/Displayed/Functor.lagda.md index 1636c1ace..8d671d44e 100644 --- a/src/Cat/Displayed/Functor.lagda.md +++ b/src/Cat/Displayed/Functor.lagda.md @@ -536,8 +536,10 @@ module _ Nat'-path = Nat'-pathp refl refl _ refl refl ``` --> -We can define displayed versions of the indentity natural transformation and + +We can define displayed versions of the identity natural transformation and composition of natural transformations. + ```agda idnt' : ∀ {F : Functor A B} {F' : Displayed-functor F D E} → F' =[ idnt ]=> F' idnt' .η' x' = E.id' diff --git a/src/Cat/Displayed/Functor/Naturality.lagda.md b/src/Cat/Displayed/Functor/Naturality.lagda.md index 617efb53a..ffc12dc97 100644 --- a/src/Cat/Displayed/Functor/Naturality.lagda.md +++ b/src/Cat/Displayed/Functor/Naturality.lagda.md @@ -11,9 +11,11 @@ import Cat.Displayed.Reasoning as DR import Cat.Displayed.Morphism as DM ``` --> + ```agda module Cat.Displayed.Functor.Naturality where ``` + # Natural isomorhisms of displayed functors We define displayed versions of our functor naturality tech. @@ -40,6 +42,7 @@ module _ open _=[_]=>_ ``` --> + ```agda _≅[_]ⁿ_ : {F G : Functor B C} → Displayed-functor F D E → F ≅ⁿ G → Displayed-functor G D E → Type _ @@ -92,8 +95,9 @@ module _ ; inverses' = record { invl' = Nat'-path (mk .eta∘inv') ; invr' = Nat'-path (mk .inv∘eta') } } ``` + \ No newline at end of file +--> diff --git a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md index 06fd5f552..ffd29e40e 100644 --- a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md +++ b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md @@ -11,6 +11,7 @@ open import Cat.Prelude import Cat.Displayed.Reasoning as DR ``` --> + ```agda module Cat.Displayed.Instances.DisplayedFunctor where ``` @@ -41,6 +42,7 @@ module _ module E = DR E ``` --> + ```agda Disp[_,_] : Displayed (Cat[ A , B ]) _ _ Disp[_,_] .Displayed.Ob[_] f = Displayed-functor f D E @@ -52,6 +54,7 @@ module _ Disp[_,_] .Displayed.idl' _ = Nat'-path λ x' → E.idl' _ Disp[_,_] .Displayed.assoc' _ _ _ = Nat'-path λ x' → E.assoc' _ _ _ ``` + + Using the total product we can define displayed versions of these familiar bifunctor constructions. + ```agda first' : ∀ {a b a' b'} {f : A.Hom a b} {x} {x' : B'.Ob[ x ]} → A'.Hom[ f ] a' b' → C'.Hom[ first f ] (F₀' (a' , x')) (F₀' (b' , x')) first' f' = F₁' (f' , B'.id') diff --git a/src/Cat/Displayed/Reasoning.lagda.md b/src/Cat/Displayed/Reasoning.lagda.md index e49765c2c..9836b0ca9 100644 --- a/src/Cat/Displayed/Reasoning.lagda.md +++ b/src/Cat/Displayed/Reasoning.lagda.md @@ -444,16 +444,12 @@ module _ {f' : Hom[ f ] x' y'} where abstract id-comm-sym[] : (id' ∘' f') ≡[ id-comm-sym ] f' ∘' id' id-comm-sym[] = id-comm-sym' - id2' : ∀ {a} {x : Ob[ a ]} {p : id ∘ id ≡ id} → id' {x = x} ∘' id' ≡[ p ] id' id2' = cast[] (idl' id') id2[] : ∀ {a} {x : Ob[ a ]} → id' {x = x} ∘' id' ≡[ id2 ] id' id2[] = id2' - - - assoc[] : ∀ {a' : Hom[ a ] y' z'} {b' : Hom[ b ] x' y'} {c' : Hom[ c ] w' x'} → {p : a ∘ (b ∘ c) ≡ d} {q : (a ∘ b) ∘ c ≡ d} From 0b00a24289efa0a302078d30fa498127f4473dc1 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Thu, 21 Aug 2025 00:01:04 -0700 Subject: [PATCH 20/24] extra line --- src/bibliography.bibtex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/bibliography.bibtex b/src/bibliography.bibtex index a0c3bb171..f29e804e5 100644 --- a/src/bibliography.bibtex +++ b/src/bibliography.bibtex @@ -352,4 +352,4 @@ pages = {1232-1269}, doi = {10.1017/S0960129522000032}, url = {https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/bicategories-in-univalent-foundations/8BFCD0A0A5DD385C130DB28BCD5E3F68} -} \ No newline at end of file +} From 30a4e657986a063354180ac485e61a0fc4ae5070 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Thu, 21 Aug 2025 00:02:15 -0700 Subject: [PATCH 21/24] remove old link --- src/Cat/Bi/Displayed/Base.lagda.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Cat/Bi/Displayed/Base.lagda.md b/src/Cat/Bi/Displayed/Base.lagda.md index 5f909422c..c8cbc3948 100644 --- a/src/Cat/Bi/Displayed/Base.lagda.md +++ b/src/Cat/Bi/Displayed/Base.lagda.md @@ -24,8 +24,6 @@ module Cat.Bi.Displayed.Base where The definition here was adapted from the one given by Ahrens et al. [-@Ahrens-Frumin-Maggesi-Veltre-vanDerWeide:Bicategories] ::: -[Bicategories in Univalent Foundations]: https://arxiv.org/abs/1903.01152 - Just as a displayed category $\cE \liesover \cB$ allows us to describe categorical structure over the category $\cB$, a **displayed bicategory** $\bf{E} \liesover \bf{B}$ allows us to describe *bi*categorical structure over the *bi*category $\bf{B}$. From d597177f87e3a088b0ccf21b949b5ffc8f26410c Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Wed, 27 Aug 2025 10:27:08 -0700 Subject: [PATCH 22/24] less annotation --- src/Cat/Bi/Displayed/Base.lagda.md | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/Cat/Bi/Displayed/Base.lagda.md b/src/Cat/Bi/Displayed/Base.lagda.md index c8cbc3948..83dbf6e0d 100644 --- a/src/Cat/Bi/Displayed/Base.lagda.md +++ b/src/Cat/Bi/Displayed/Base.lagda.md @@ -184,8 +184,8 @@ The unitors and associator are displayed isomorphims over the unitors and associ ```agda field - unitor-l' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → _≅[_]_ Disp[ Hom[ A' , B' ] , Hom[ A' , B' ] ] Id' unitor-l (Right' compose' ↦id') - unitor-r' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → _≅[_]_ Disp[ Hom[ A' , B' ] , Hom[ A' , B' ] ] Id' unitor-r (Left' compose' ↦id') + unitor-l' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → Id' {ℰ = Hom[ A' , B' ]} ≅[ unitor-l ]ⁿ (Right' compose' ↦id') + unitor-r' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → Id' {ℰ = Hom[ A' , B' ]} ≅[ unitor-r ]ⁿ (Left' compose' ↦id') associator' : ∀ {A B C D} {A' : Ob[ A ]} {B' : Ob[ B ]} {C' : Ob[ C ]} {D' : Ob[ D ]} → _≅[_]_ Disp[ Hom[ C' , D' ] ×ᵀᴰ (Hom[ B' , C' ] ×ᵀᴰ Hom[ A' , B' ]) , Hom[ A' , D' ] ] @@ -202,58 +202,58 @@ The associated displayed cell combinators proceed in the same way. ```agda λ←' : ∀ {A B A' B'} {f : A ↦ B} (f' : A' [ f ]↦ B') → (↦id' ⊗' f') [ λ← f ]⇒ f' - λ←' = unitor-l' ._≅[_]_.from' .η' + λ←' = unitor-l'.from' .η' λ→' : ∀ {A B A' B'} {f : A ↦ B} → (f' : A' [ f ]↦ B') → f' [ λ→ f ]⇒ (↦id' ⊗' f') - λ→' = unitor-l' ._≅[_]_.to' .η' + λ→' = unitor-l'.to' .η' ρ←' : ∀ {A B A' B'} {f : A ↦ B} → (f' : A' [ f ]↦ B') → (f' ⊗' ↦id') [ ρ← f ]⇒ f' - ρ←' = unitor-r' ._≅[_]_.from' .η' + ρ←' = unitor-r'.from' .η' ρ→' : ∀ {A B A' B'} {f : A ↦ B} → (f' : A' [ f ]↦ B') → f' [ ρ→ f ]⇒ (f' ⊗' ↦id') - ρ→' = unitor-r' ._≅[_]_.to' .η' + ρ→' = unitor-r'.to' .η' ρ←nat' : ∀ {A B A' B'} {f₁ f₂ : A ↦ B} {β : f₁ ⇒ f₂} → {f₁' : A' [ f₁ ]↦ B'} {f₂' : A' [ f₂ ]↦ B'} → (β' : f₁' [ β ]⇒ f₂') → (ρ←' _ ∘' (β' ◀' ↦id')) Hom[].≡[ ρ←nat β ] (β' ∘' ρ←' _) - ρ←nat' β' = unitor-r' .from' .is-natural' _ _ β' + ρ←nat' β' = unitor-r'.from' .is-natural' _ _ β' λ←nat' : ∀ {A B A' B'} {f₁ f₂ : A ↦ B} {β : f₁ ⇒ f₂} → {f₁' : A' [ f₁ ]↦ B'} {f₂' : A' [ f₂ ]↦ B'} → (β' : f₁' [ β ]⇒ f₂') → (λ←' _ ∘' (↦id' ▶' β')) Hom[].≡[ λ←nat β ] (β' ∘' λ←' _) - λ←nat' β' = unitor-l' .from' .is-natural' _ _ β' + λ←nat' β' = unitor-l'.from' .is-natural' _ _ β' ρ→nat' : ∀ {A B A' B'} {f₁ f₂ : A ↦ B} {β : f₁ ⇒ f₂} → {f₁' : A' [ f₁ ]↦ B'} {f₂' : A' [ f₂ ]↦ B'} → (β' : f₁' [ β ]⇒ f₂') → (ρ→' _ ∘' β') Hom[].≡[ ρ→nat β ] ((β' ◀' ↦id') ∘' ρ→' _) - ρ→nat' β' = unitor-r' .to' .is-natural' _ _ β' + ρ→nat' β' = unitor-r'.to' .is-natural' _ _ β' λ→nat' : ∀ {A B A' B'} {f₁ f₂ : A ↦ B} {β : f₁ ⇒ f₂} → {f₁' : A' [ f₁ ]↦ B'} {f₂' : A' [ f₂ ]↦ B'} → (β' : f₁' [ β ]⇒ f₂') → (λ→' _ ∘' β') Hom[].≡[ λ→nat β ] ((↦id' ▶' β') ∘' λ→' _) - λ→nat' β' = unitor-l' .to' .is-natural' _ _ β' + λ→nat' β' = unitor-l'.to' .is-natural' _ _ β' α→' : ∀ {A B C D A' B' C' D'} {f : C ↦ D} {g : B ↦ C} {h : A ↦ B} → (f' : C' [ f ]↦ D') (g' : B' [ g ]↦ C') (h' : A' [ h ]↦ B') → ((f' ⊗' g') ⊗' h') [ α→ f g h ]⇒ (f' ⊗' (g' ⊗' h')) - α→' f' g' h' = associator' ._≅[_]_.to' .η' (f' , g' , h') + α→' f' g' h' = associator'.to' .η' (f' , g' , h') α←' : ∀ {A B C D A' B' C' D'} {f : C ↦ D} {g : B ↦ C} {h : A ↦ B} → (f' : C' [ f ]↦ D') (g' : B' [ g ]↦ C') (h' : A' [ h ]↦ B') → (f' ⊗' (g' ⊗' h')) [ α← f g h ]⇒ ((f' ⊗' g') ⊗' h') - α←' f' g' h' = associator' ._≅[_]_.from' .η' (f' , g' , h') + α←' f' g' h' = associator'.from' .η' (f' , g' , h') α←nat' : ∀ {A B C D A' B' C' D'} {f₁ f₂ : C ↦ D} {g₁ g₂ : B ↦ C} {h₁ h₂ : A ↦ B} @@ -265,7 +265,7 @@ The associated displayed cell combinators proceed in the same way. → (α←' _ _ _ ∘' (β' ◆' (γ' ◆' δ'))) Hom[].≡[ α←nat β γ δ ] (((β' ◆' γ') ◆' δ') ∘' α←' _ _ _) α←nat' β' γ' δ' = - associator' .from' .is-natural' (_ , _ , _) (_ , _ , _) (β' , γ' , δ') + associator'.from' .is-natural' (_ , _ , _) (_ , _ , _) (β' , γ' , δ') α→nat' : ∀ {A B C D A' B' C' D'} {f₁ f₂ : C ↦ D} {g₁ g₂ : B ↦ C} {h₁ h₂ : A ↦ B} @@ -277,7 +277,7 @@ The associated displayed cell combinators proceed in the same way. → (α→' _ _ _ ∘' ((β' ◆' γ') ◆' δ')) Hom[].≡[ α→nat β γ δ ] ((β' ◆' (γ' ◆' δ')) ∘' α→' _ _ _) α→nat' β' γ' δ' = - associator' .to' .is-natural' (_ , _ , _) (_ , _ , _) (β' , γ' , δ') + associator'.to' .is-natural' (_ , _ , _) (_ , _ , _) (β' , γ' , δ') ``` As do the triangle and pentagon identities. From 27067cb98a463087a6a712031a6859b926833760 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Wed, 27 Aug 2025 11:41:45 -0700 Subject: [PATCH 23/24] add new fields to Disp[_,_] --- src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md index ffd29e40e..af439ce25 100644 --- a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md +++ b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md @@ -53,6 +53,9 @@ module _ Disp[_,_] .Displayed.idr' _ = Nat'-path λ x' → E.idr' _ Disp[_,_] .Displayed.idl' _ = Nat'-path λ x' → E.idl' _ Disp[_,_] .Displayed.assoc' _ _ _ = Nat'-path λ x' → E.assoc' _ _ _ + Disp[_,_] .Displayed.hom[_] {x = F} {y = G} p α' = NT' (λ {x} x' → E.hom[ p ηₚ x ] (α' .η' x')) + λ {x} {y} x' y' f' → E.cast[] $ E.unwrapl _ E.∙[] α' .is-natural' x' y' f' E.∙[] E.wrapr _ + Disp[_,_] .Displayed.coh[_] p f = Nat'-path (λ {x} x' → E.coh[ p ηₚ x ] (f .η' x')) ```