From 719fb96f731c34178f6fc90ea7df8233fc25fa99 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20=C3=85gren=20Thun=C3=A9?= Date: Sun, 17 Aug 2025 15:19:56 +0200 Subject: [PATCH 1/6] chore: Define bicategorical pre- and postactions by bifunctor defs --- src/Cat/Bi/Base.lagda.md | 17 ++--------------- 1 file changed, 2 insertions(+), 15 deletions(-) diff --git a/src/Cat/Bi/Base.lagda.md b/src/Cat/Bi/Base.lagda.md index d08ddcd76..94b8bbb4a 100644 --- a/src/Cat/Bi/Base.lagda.md +++ b/src/Cat/Bi/Base.lagda.md @@ -294,25 +294,12 @@ $\bf{B}$, $\bf{C}$. ```agda module _ (B : Prebicategory o ℓ ℓ') where open Prebicategory B - open Functor postaction : ∀ {a b c} (f : a ↦ b) → Functor (Hom c a) (Hom c b) - postaction f .F₀ g = f ⊗ g - postaction f .F₁ g = f ▶ g - postaction f .F-id = compose.F-id - postaction f .F-∘ g h = - f ▶ (g ∘ h) ≡˘⟨ ap (_◆ g ∘ h) (Hom.idl Hom.id) ⟩ - (Hom.id ∘ Hom.id) ◆ (g ∘ h) ≡⟨ compose.F-∘ _ _ ⟩ - (f ▶ g) ∘ (f ▶ h) ∎ + postaction = Bi.Right compose preaction : ∀ {a b c} (f : a ↦ b) → Functor (Hom b c) (Hom a c) - preaction f .F₀ g = g ⊗ f - preaction f .F₁ g = g ◀ f - preaction f .F-id = compose.F-id - preaction f .F-∘ g h = - (g ∘ h) ◀ f ≡˘⟨ ap (g ∘ h ◆_) (Hom.idl Hom.id) ⟩ - (g ∘ h) ◆ (Hom.id ∘ Hom.id) ≡⟨ compose.F-∘ _ _ ⟩ - (g ◀ f) ∘ (h ◀ f) ∎ + preaction = Bi.Left compose ``` --> From 982bc5239b4c687ed9440217e09d610aa36fac0d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20=C3=85gren=20Thun=C3=A9?= Date: Sun, 8 Mar 2026 18:13:22 +0100 Subject: [PATCH 2/6] chore: Add no-eta-equality to bicategory-related records --- src/Cat/Bi/Base.lagda.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Cat/Bi/Base.lagda.md b/src/Cat/Bi/Base.lagda.md index 94b8bbb4a..98c022918 100644 --- a/src/Cat/Bi/Base.lagda.md +++ b/src/Cat/Bi/Base.lagda.md @@ -407,6 +407,7 @@ When they _are_, we talk about **pseudofunctors** instead. record Lax-functor (B : Prebicategory o ℓ ℓ') (C : Prebicategory o₁ ℓ₁ ℓ₁') : Type (o ⊔ o₁ ⊔ ℓ ⊔ ℓ₁ ⊔ ℓ' ⊔ ℓ₁') where + no-eta-equality private module B = Prebicategory B @@ -499,6 +500,7 @@ functors, not additional structure on lax functors. record Pseudofunctor (B : Prebicategory o ℓ ℓ') (C : Prebicategory o₁ ℓ₁ ℓ₁') : Type (o ⊔ o₁ ⊔ ℓ ⊔ ℓ₁ ⊔ ℓ' ⊔ ℓ₁') where + no-eta-equality private module B = Prebicategory B @@ -568,6 +570,7 @@ and thus consists of a natural family of 2-cells $G(f)\sigma_a \To ```agda record Lax-transfor : Type (o ⊔ ℓ ⊔ ℓ₁ ⊔ ℓ' ⊔ ℓ₁') where + no-eta-equality field σ : ∀ A → F.₀ A C.↦ G.₀ A naturator @@ -606,6 +609,7 @@ A lax transformation with invertible naturator is called a ```agda record Pseudonatural : Type (o ⊔ ℓ ⊔ ℓ₁ ⊔ ℓ' ⊔ ℓ₁') where + no-eta-equality field lax : Lax-transfor @@ -658,6 +662,7 @@ module ```agda record Modification : Type (o ⊔ ℓ ⊔ ℓ₁') where + no-eta-equality field Γ : ∀ a → σ.σ a C.⇒ σ'.σ a From c2f9324d88c7bbc66f394568d2bc9cbb5be04f05 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20=C3=85gren=20Thun=C3=A9?= Date: Tue, 17 Mar 2026 22:46:56 +0100 Subject: [PATCH 3/6] chore: Define bicategory associators and unitors by re-export --- src/Cat/Bi/Base.lagda.md | 58 +++++++++++-------------- src/Cat/Bi/Diagram/Adjunction.lagda.md | 4 +- src/Cat/Bi/Diagram/Monad.lagda.md | 24 +++++----- src/Cat/Bi/Diagram/Monad/Spans.lagda.md | 4 +- src/Cat/LocallyGraded/Base.lagda.md | 2 +- src/Cat/Monoidal/Base.lagda.md | 4 +- 6 files changed, 45 insertions(+), 51 deletions(-) diff --git a/src/Cat/Bi/Base.lagda.md b/src/Cat/Bi/Base.lagda.md index 98c022918..ad62c1b7b 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}) ``` @@ -198,54 +200,46 @@ unitor as $\rho$, and to the associator as $\alpha$, so we set up those abbreviations here too: ```agda - λ← : ∀ {A B} (f : A ↦ B) → id ⊗ f ⇒ f - λ← = unitor-l .Cr._≅_.from .η + private + open module λ← {a b} = _=>_ (unitor-l.from {a} {b}) renaming (η to λ←) using () public + + open module λ→ {a b} = _=>_ (unitor-l.to {a} {b}) renaming (η to λ→) using () public + + open module ρ← {a b} = _=>_ (unitor-r.from {a} {b}) renaming (η to ρ←) using () public - λ→ : ∀ {A B} (f : A ↦ B) → f ⇒ id ⊗ f - λ→ = unitor-l .Cr._≅_.to .η + open module ρ→ {a b} = _=>_ (unitor-r.to {a} {b}) renaming (η to ρ→) using () public - ρ← : ∀ {A B} (f : A ↦ B) → f ⊗ id ⇒ f - ρ← = unitor-r .Cr._≅_.from .η + open module α→ {a b c d} = _=>_ (associator.to {a} {b} {c} {d}) renaming (η to α→) using () public - ρ→ : ∀ {A B} (f : A ↦ B) → f ⇒ f ⊗ id - ρ→ = unitor-r .Cr._≅_.to .η + open module α← {a b c d} = _=>_ (associator.from {a} {b} {c} {d}) renaming (η to α←) using () public ρ←nat : ∀ {A B} {f f' : A ↦ B} (β : f ⇒ f') → Path ((f ⊗ id) ⇒ f') (ρ← _ ∘ (β ◀ id)) (β ∘ ρ← _) - ρ←nat {A} {B} {f} {f'} β = unitor-r .Cr.from .is-natural f f' β + ρ←nat {A} {B} {f} {f'} β = unitor-r.from .is-natural f f' β λ←nat : ∀ {A B} {f f' : A ↦ B} (β : f ⇒ f') → Path ((id ⊗ f) ⇒ f') (λ← _ ∘ (id ▶ β)) (β ∘ λ← _) - λ←nat {A} {B} {f} {f'} β = unitor-l .Cr.from .is-natural f f' β + λ←nat {A} {B} {f} {f'} β = unitor-l.from .is-natural f f' β ρ→nat : ∀ {A B} {f f' : A ↦ B} (β : f ⇒ f') → Path (f ⇒ f' ⊗ id) (ρ→ _ ∘ β) ((β ◀ id) ∘ ρ→ _) - ρ→nat {A} {B} {f} {f'} β = unitor-r .Cr.to .is-natural f f' β + ρ→nat {A} {B} {f} {f'} β = unitor-r.to .is-natural f f' β λ→nat : ∀ {A B} {f f' : A ↦ B} (β : f ⇒ f') → Path (f ⇒ id ⊗ f') (λ→ _ ∘ β) ((id ▶ β) ∘ λ→ _) - λ→nat {A} {B} {f} {f'} β = unitor-l .Cr.to .is-natural f f' β - - α→ : ∀ {A B C D} (f : C ↦ D) (g : B ↦ C) (h : A ↦ B) - → (f ⊗ g) ⊗ h ⇒ f ⊗ (g ⊗ h) - α→ f g h = associator.to .η (f , g , h) - - α← : ∀ {A B C D} (f : C ↦ D) (g : B ↦ C) (h : A ↦ B) - → f ⊗ (g ⊗ h) ⇒ (f ⊗ g) ⊗ h - α← f g h = associator.from .η (f , g , h) - + λ→nat {A} {B} {f} {f'} β = unitor-l.to .is-natural f f' β + α←nat : ∀ {A B C D} {f f' : C ↦ D} {g g' : B ↦ C} {h h' : A ↦ B} → (β : f ⇒ f') (γ : g ⇒ g') (δ : h ⇒ h') → Path (f ⊗ g ⊗ h ⇒ ((f' ⊗ g') ⊗ h')) - (α← _ _ _ ∘ (β ◆ (γ ◆ δ))) (((β ◆ γ) ◆ δ) ∘ α← _ _ _) + (α← _ ∘ (β ◆ (γ ◆ δ))) (((β ◆ γ) ◆ δ) ∘ α← _) α←nat {A} {B} {C} {D} {f} {f'} {g} {g'} {h} {h'} β γ δ = associator.from .is-natural (f , g , h) (f' , g' , h') (β , γ , δ) α→nat : ∀ {A B C D} {f f' : C ↦ D} {g g' : B ↦ C} {h h' : A ↦ B} → (β : f ⇒ f') (γ : g ⇒ g') (δ : h ⇒ h') → Path ((f ⊗ g) ⊗ h ⇒ (f' ⊗ g' ⊗ h')) - (α→ _ _ _ ∘ ((β ◆ γ) ◆ δ)) - ((β ◆ (γ ◆ δ)) ∘ α→ _ _ _) + (α→ _ ∘ ((β ◆ γ) ◆ δ)) ((β ◆ (γ ◆ δ)) ∘ α→ _) α→nat {A} {B} {C} {D} {f} {f'} {g} {g'} {h} {h'} β γ δ = associator.to .is-natural (f , g , h) (f' , g' , h') (β , γ , δ) ``` @@ -275,12 +269,12 @@ witnesses commutativity of the diagram field triangle : ∀ {A B C} (f : B ↦ C) (g : A ↦ B) - → (ρ← f ◀ g) ∘ α← f id g ≡ f ▶ λ← g + → (ρ← f ◀ g) ∘ α← (f , id , g) ≡ f ▶ λ← g pentagon : ∀ {A B C D E} (f : D ↦ E) (g : C ↦ D) (h : B ↦ C) (i : A ↦ B) - → (α← f g h ◀ i) ∘ α← f (g ⊗ h) i ∘ (f ▶ α← g h i) - ≡ α← (f ⊗ g) h i ∘ α← f g (h ⊗ i) + → (α← (f , g , h) ◀ i) ∘ α← (f , g ⊗ h , i) ∘ (f ▶ α← (g , h , i)) + ≡ α← (f ⊗ g , h , i) ∘ α← (f , g , h ⊗ i) ``` Our coherence diagrams for bicategorical data are taken from @@ -476,8 +470,8 @@ squares). field hexagon : ∀ {a b c d} (f : c B.↦ d) (g : b B.↦ c) (h : a B.↦ b) - → ₂ (B.α→ f g h) C.∘ γ→ (f B.⊗ g) h C.∘ (γ→ f g C.◀ ₁ h) - ≡ γ→ f (g B.⊗ h) C.∘ (₁ f C.▶ γ→ g h) C.∘ C.α→ (₁ f) (₁ g) (₁ h) + → ₂ (B.α→ (f , g , h)) C.∘ γ→ (f B.⊗ g) h C.∘ (γ→ f g C.◀ ₁ h) + ≡ γ→ f (g B.⊗ h) C.∘ (₁ f C.▶ γ→ g h) C.∘ C.α→ (₁ f , ₁ g , ₁ h) right-unit : ∀ {a b} (f : a B.↦ b) @@ -592,11 +586,11 @@ boil down to commutativity of the nightmarish diagrams in [@basicbicats, : ∀ {a b c} (f : b B.↦ c) (g : a B.↦ b) → ν→ (f B.⊗ g) C.∘ (G.γ→ f g C.◀ σ a) ≡ (σ c C.▶ F.γ→ f g) - C.∘ C.α→ (σ c) (F.₁ f) (F.₁ g) + C.∘ C.α→ (σ c , F.₁ f , F.₁ g) C.∘ (ν→ f C.◀ F.₁ g) - C.∘ C.α← (G.₁ f) (σ b) (F.₁ g) + C.∘ C.α← (G.₁ f , σ b , F.₁ g) C.∘ (G.₁ f C.▶ ν→ g) - C.∘ C.α→ (G.₁ f) (G.₁ g) (σ a) + C.∘ C.α→ (G.₁ f , G.₁ g , σ a) ν-unitor : ∀ {a} diff --git a/src/Cat/Bi/Diagram/Adjunction.lagda.md b/src/Cat/Bi/Diagram/Adjunction.lagda.md index 63cd28354..06d20a1b6 100644 --- a/src/Cat/Bi/Diagram/Adjunction.lagda.md +++ b/src/Cat/Bi/Diagram/Adjunction.lagda.md @@ -63,8 +63,8 @@ above into equations that are well-typed in a (weak) bicategory. η : B.id B.⇒ (g B.⊗ f) ε : (f B.⊗ g) B.⇒ B.id - zig : B.Hom.id ≡ B.λ← f B.∘ (ε B.◀ f) B.∘ B.α← f g f B.∘ (f B.▶ η) B.∘ B.ρ→ f - zag : B.Hom.id ≡ B.ρ← g B.∘ (g B.▶ ε) B.∘ B.α→ g f g B.∘ (η B.◀ g) B.∘ B.λ→ g + zig : B.Hom.id ≡ B.λ← f B.∘ (ε B.◀ f) B.∘ B.α← (f , g , f) B.∘ (f B.▶ η) B.∘ B.ρ→ f + zag : B.Hom.id ≡ B.ρ← g B.∘ (g B.▶ ε) B.∘ B.α→ (g , f , g) B.∘ (η B.◀ g) B.∘ B.λ→ g ``` This means the triangle identities, rather diff --git a/src/Cat/Bi/Diagram/Monad.lagda.md b/src/Cat/Bi/Diagram/Monad.lagda.md index bcf495e3b..86dad2b2b 100644 --- a/src/Cat/Bi/Diagram/Monad.lagda.md +++ b/src/Cat/Bi/Diagram/Monad.lagda.md @@ -53,7 +53,7 @@ the unit $\eta$ must be appropriately compatible with the left and right unitors $\lambda, \rho$. ```agda - μ-assoc : μ B.∘ (M B.▶ μ) ≡ μ B.∘ (μ B.◀ M) B.∘ B.α← M M M + μ-assoc : μ B.∘ (M B.▶ μ) ≡ μ B.∘ (μ B.◀ M) B.∘ B.α← (M , M , M) μ-unitr : μ B.∘ (M B.▶ η) ≡ B.ρ← M μ-unitl : μ B.∘ (η B.◀ M) ≡ B.λ← M ``` @@ -177,11 +177,11 @@ $\cB$ on $a$. P .compositor .is-natural _ _ _ = Hom.elimr (B.compose .F-id) ∙ sym (Hom.idl _) P .unitor = η P .hexagon _ _ _ = - Hom.id ∘ μ ∘ (μ ◀ M) ≡⟨ Hom.pulll (Hom.idl _) ⟩ - μ ∘ (μ ◀ M) ≡⟨ Hom.intror $ ap (λ nt → nt ._=>_.η (M , M , M)) associator.invr ⟩ - (μ ∘ μ ◀ M) ∘ (α← M M M ∘ α→ M M M) ≡⟨ cat! (Hom a a) ⟩ - (μ ∘ μ ◀ M ∘ α← M M M) ∘ α→ M M M ≡˘⟨ Hom.pulll μ-assoc ⟩ - μ ∘ (M ▶ μ) ∘ (α→ M M M) ∎ + Hom.id ∘ μ ∘ (μ ◀ M) ≡⟨ Hom.pulll (Hom.idl _) ⟩ + μ ∘ (μ ◀ M) ≡⟨ Hom.intror $ ap (λ nt → nt ._=>_.η (M , M , M)) associator.invr ⟩ + (μ ∘ μ ◀ M) ∘ (α← (M , M , M) ∘ α→ (M , M , M)) ≡⟨ cat! (Hom a a) ⟩ + (μ ∘ μ ◀ M ∘ α← (M , M , M)) ∘ α→ (M , M , M) ≡˘⟨ Hom.pulll μ-assoc ⟩ + μ ∘ (M ▶ μ) ∘ α→ (M , M , M) ∎ P .right-unit _ = Hom.id ∘ μ ∘ M ▶ η ≡⟨ Hom.idl _ ∙ μ-unitr ⟩ ρ← M ∎ P .left-unit _ = Hom.id ∘ μ ∘ (η ◀ M) ≡⟨ Hom.idl _ ∙ μ-unitl ⟩ λ← M ∎ @@ -197,12 +197,12 @@ $\cB$ on $a$. μ = γ→ _ _ η = unitor μ-assoc = - μ ∘ M ▶ μ ≡⟨ (Hom.intror $ ap (λ nt → nt ._=>_.η (M , M , M)) associator.invl) ⟩ - (μ ∘ M ▶ μ) ∘ (α→ M M M ∘ α← M M M) ≡⟨ cat! (Hom a a) ⟩ - (μ ∘ M ▶ μ ∘ α→ M M M) ∘ α← M M M ≡˘⟨ hexagon _ _ _ Hom.⟩∘⟨refl ⟩ - (P₁.F₁ _ ∘ μ ∘ μ ◀ M) ∘ α← M M M ≡⟨ ( P₁.F-id Hom.⟩∘⟨refl) Hom.⟩∘⟨refl ⟩ - (Hom.id ∘ μ ∘ μ ◀ M) ∘ α← M M M ≡⟨ cat! (Hom a a) ⟩ - μ ∘ μ ◀ M ∘ α← M M M ∎ + μ ∘ M ▶ μ ≡⟨ (Hom.intror $ ap (λ nt → nt ._=>_.η (M , M , M)) associator.invl) ⟩ + (μ ∘ M ▶ μ) ∘ (α→ (M , M , M) ∘ α← (M , M , M)) ≡⟨ cat! (Hom a a) ⟩ + (μ ∘ M ▶ μ ∘ α→ (M , M , M)) ∘ α← (M , M , M) ≡˘⟨ hexagon _ _ _ Hom.⟩∘⟨refl ⟩ + (P₁.F₁ _ ∘ μ ∘ μ ◀ M) ∘ α← (M , M , M) ≡⟨ ( P₁.F-id Hom.⟩∘⟨refl) Hom.⟩∘⟨refl ⟩ + (Hom.id ∘ μ ∘ μ ◀ M) ∘ α← (M , M , M) ≡⟨ cat! (Hom a a) ⟩ + μ ∘ μ ◀ M ∘ α← (M , M , M) ∎ μ-unitr = Fr.introl P₁ refl ∙ right-unit _ μ-unitl = Fr.introl P₁ refl ∙ left-unit _ ``` diff --git a/src/Cat/Bi/Diagram/Monad/Spans.lagda.md b/src/Cat/Bi/Diagram/Monad/Spans.lagda.md index 8c742b099..a231dd8ff 100644 --- a/src/Cat/Bi/Diagram/Monad/Spans.lagda.md +++ b/src/Cat/Bi/Diagram/Monad/Spans.lagda.md @@ -130,10 +130,10 @@ instruct the curious reader to check the proof on GitHub. J' (λ w z q → ∀ (f : C.Hom w x) {y b} (p : y ≡ b) (g : C .Hom y z) (h : C.Hom a b) → (mult Sb.∘ (homs Sb.▶ mult)) .map ((w , x , f) , ((y , z , g) , (a , b , h) , p) , q) - ≡ (mult Sb.∘ (mult Sb.◀ homs) Sb.∘ Sb.α← homs homs homs) .map ((w , x , f) , ((y , z , g) , (a , b , h) , p) , q)) + ≡ (mult Sb.∘ (mult Sb.◀ homs) Sb.∘ Sb.α← (homs , homs , homs)) .map ((w , x , f) , ((y , z , g) , (a , b , h) , p) , q)) (λ w f → J' (λ y b p → (g : C.Hom y w) (h : C.Hom a b) → (mult Sb.∘ (homs Sb.▶ mult)) .map ((w , x , f) , ((y , w , g) , (a , b , h) , p) , refl) - ≡ (mult Sb.∘ (mult Sb.◀ homs) Sb.∘ Sb.α← homs homs homs) .map ((w , x , f) , ((y , w , g) , (a , b , h) , p) , refl)) + ≡ (mult Sb.∘ (mult Sb.◀ homs) Sb.∘ Sb.α← (homs , homs , homs)) .map ((w , x , f) , ((y , w , g) , (a , b , h) , p) , refl)) λ y g h → Σ-pathp refl (Σ-pathp refl (C.assoc _ _ _ ∙ ap₂ C._∘_ (ap₂ C._∘_ (ap (λ p → subst (λ e → C.Hom e x) p f) (hlevel 2 w w _ refl) ∙ transport-refl _) (ap (λ p → subst (λ e → C.Hom e w) p g) (hlevel 2 y y _ refl) ∙ transport-refl _) diff --git a/src/Cat/LocallyGraded/Base.lagda.md b/src/Cat/LocallyGraded/Base.lagda.md index d7be0a20f..d2c973f1d 100644 --- a/src/Cat/LocallyGraded/Base.lagda.md +++ b/src/Cat/LocallyGraded/Base.lagda.md @@ -102,7 +102,7 @@ suitably adjusted by an associator or unitor. : ∀ {a b c d a' b' c' d'} → {u : c B.↦ d} {v : b B.↦ c} {w : a B.↦ b} → (f : Hom[ u ] c' d') (g : Hom[ v ] b' c') (h : Hom[ w ] a' b') - → (f ∘' (g ∘' h)) [ B.α→ u v w ] ≡ (f ∘' g) ∘' h + → (f ∘' (g ∘' h)) [ B.α→ (u , v , w) ] ≡ (f ∘' g) ∘' h ``` Finally, we require that the action of 2-cells is functorial, and that diff --git a/src/Cat/Monoidal/Base.lagda.md b/src/Cat/Monoidal/Base.lagda.md index 29f1366d6..ca782b1ea 100644 --- a/src/Cat/Monoidal/Base.lagda.md +++ b/src/Cat/Monoidal/Base.lagda.md @@ -239,8 +239,8 @@ Endomorphisms B a = mon where open make-natural-iso open Cr ni : make-natural-iso _ _ - ni .eta _ = B.α→ _ _ _ - ni .inv _ = B.α← _ _ _ + ni .eta _ = B.α→ _ + ni .inv _ = B.α← _ ni .eta∘inv _ = Cr.invl _ B.associator ηₚ _ ni .inv∘eta _ = Cr.invr _ B.associator ηₚ _ ni .natural x y f = sym $ Cr.to B.associator .is-natural _ _ _ From e76d3ce11ae74b2e2b817d85fdcdb42ef8c5ade8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20=C3=85gren=20Thun=C3=A9?= Date: Tue, 17 Mar 2026 23:20:21 +0100 Subject: [PATCH 4/6] chore: Add short alias for bicat compose module, shorten definitions --- src/Cat/Bi/Base.lagda.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Cat/Bi/Base.lagda.md b/src/Cat/Bi/Base.lagda.md index ad62c1b7b..f014fbbdf 100644 --- a/src/Cat/Bi/Base.lagda.md +++ b/src/Cat/Bi/Base.lagda.md @@ -145,6 +145,8 @@ whence the name **horizontal composition**. _⇒_ : ∀ {A B} (f g : A ↦ B) → Type ℓ' _⇒_ {A} {B} f g = Hom.Hom f g + module ⊗ = compose + -- 1-cell composition _⊗_ : ∀ {A B C} (f : B ↦ C) (g : A ↦ B) → A ↦ C f ⊗ g = compose · (f , g) @@ -156,7 +158,7 @@ whence the name **horizontal composition**. -- horizontal 2-cell composition _◆_ : ∀ {A B C} {f₁ f₂ : B ↦ C} (β : f₁ ⇒ f₂) {g₁ g₂ : A ↦ B} (α : g₁ ⇒ g₂) → (f₁ ⊗ g₁) ⇒ (f₂ ⊗ g₂) - _◆_ β α = compose .Functor.F₁ (β , α) + _◆_ β α = compose.F₁ (β , α) infixr 30 _∘_ infixr 25 _⊗_ @@ -164,11 +166,11 @@ whence the name **horizontal composition**. -- whiskering on the right _▶_ : ∀ {A B C} (f : B ↦ C) {a b : A ↦ B} (g : a ⇒ b) → f ⊗ a ⇒ f ⊗ b - _▶_ {A} {B} {C} f g = compose .Functor.F₁ (Hom.id , g) + _▶_ {A} {B} {C} f g = compose.F₁ (Hom.id , g) -- whiskering on the left _◀_ : ∀ {A B C} {a b : B ↦ C} (g : a ⇒ b) (f : A ↦ B) → a ⊗ f ⇒ b ⊗ f - _◀_ {A} {B} {C} g f = compose .Functor.F₁ (g , Hom.id) + _◀_ {A} {B} {C} g f = compose.F₁ (g , Hom.id) ``` We now move onto the invertible 2-cells witnessing that the chosen From 2681032e0779ff7a2d42cf0372492aa89551b7ac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20=C3=85gren=20Thun=C3=A9?= Date: Wed, 18 Mar 2026 01:18:37 +0100 Subject: [PATCH 5/6] chore: Define lax functor fields by re-export, shorten definitions --- src/Cat/Bi/Base.lagda.md | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/src/Cat/Bi/Base.lagda.md b/src/Cat/Bi/Base.lagda.md index f014fbbdf..ccc012806 100644 --- a/src/Cat/Bi/Base.lagda.md +++ b/src/Cat/Bi/Base.lagda.md @@ -217,33 +217,33 @@ abbreviations here too: ρ←nat : ∀ {A B} {f f' : A ↦ B} (β : f ⇒ f') → Path ((f ⊗ id) ⇒ f') (ρ← _ ∘ (β ◀ id)) (β ∘ ρ← _) - ρ←nat {A} {B} {f} {f'} β = unitor-r.from .is-natural f f' β + ρ←nat {A} {B} {f} {f'} β = ρ←.is-natural f f' β λ←nat : ∀ {A B} {f f' : A ↦ B} (β : f ⇒ f') → Path ((id ⊗ f) ⇒ f') (λ← _ ∘ (id ▶ β)) (β ∘ λ← _) - λ←nat {A} {B} {f} {f'} β = unitor-l.from .is-natural f f' β + λ←nat {A} {B} {f} {f'} β = λ←.is-natural f f' β ρ→nat : ∀ {A B} {f f' : A ↦ B} (β : f ⇒ f') → Path (f ⇒ f' ⊗ id) (ρ→ _ ∘ β) ((β ◀ id) ∘ ρ→ _) - ρ→nat {A} {B} {f} {f'} β = unitor-r.to .is-natural f f' β + ρ→nat {A} {B} {f} {f'} β = ρ→.is-natural f f' β λ→nat : ∀ {A B} {f f' : A ↦ B} (β : f ⇒ f') → Path (f ⇒ id ⊗ f') (λ→ _ ∘ β) ((id ▶ β) ∘ λ→ _) - λ→nat {A} {B} {f} {f'} β = unitor-l.to .is-natural f f' β + λ→nat {A} {B} {f} {f'} β = λ→.is-natural f f' β α←nat : ∀ {A B C D} {f f' : C ↦ D} {g g' : B ↦ C} {h h' : A ↦ B} → (β : f ⇒ f') (γ : g ⇒ g') (δ : h ⇒ h') → Path (f ⊗ g ⊗ h ⇒ ((f' ⊗ g') ⊗ h')) (α← _ ∘ (β ◆ (γ ◆ δ))) (((β ◆ γ) ◆ δ) ∘ α← _) α←nat {A} {B} {C} {D} {f} {f'} {g} {g'} {h} {h'} β γ δ = - associator.from .is-natural (f , g , h) (f' , g' , h') (β , γ , δ) + α←.is-natural (f , g , h) (f' , g' , h') (β , γ , δ) α→nat : ∀ {A B C D} {f f' : C ↦ D} {g g' : B ↦ C} {h h' : A ↦ B} → (β : f ⇒ f') (γ : g ⇒ g') (δ : h ⇒ h') → Path ((f ⊗ g) ⊗ h ⇒ (f' ⊗ g' ⊗ h')) (α→ _ ∘ ((β ◆ γ) ◆ δ)) ((β ◆ (γ ◆ δ)) ∘ α→ _) α→nat {A} {B} {C} {D} {f} {f'} {g} {g'} {h} {h'} β γ δ = - associator.to .is-natural (f , g , h) (f' , g' , h') (β , γ , δ) + α→.is-natural (f , g , h) (f' , g' , h') (β , γ , δ) ``` The final data we need are coherences relating the left and right @@ -428,17 +428,11 @@ have components $F_1(f)F_1(g) \To F_1(fg)$ and $\id \To F_1(\id)$. @@ -466,16 +473,16 @@ squares). field hexagon : ∀ {a b c d} (f : c B.↦ d) (g : b B.↦ c) (h : a B.↦ b) - → ₂ (B.α→ (f , g , h)) C.∘ γ→ (f B.⊗ g) h C.∘ (γ→ f g C.◀ ₁ h) - ≡ γ→ f (g B.⊗ h) C.∘ (₁ f C.▶ γ→ g h) C.∘ C.α→ (₁ f , ₁ g , ₁ h) + → ₂ (B.α→ (f , g , h)) C.∘ γ→ (f B.⊗ g , h) C.∘ (γ→ (f , g) C.◀ ₁ h) + ≡ γ→ (f , g B.⊗ h) C.∘ (₁ f C.▶ γ→ (g , h)) C.∘ C.α→ (₁ f , ₁ g , ₁ h) right-unit : ∀ {a b} (f : a B.↦ b) - → ₂ (B.ρ← f) C.∘ γ→ f B.id C.∘ (₁ f C.▶ unitor) ≡ C.ρ← (₁ f) + → ₂ (B.ρ← f) C.∘ γ→ (f , B.id) C.∘ (₁ f C.▶ unitor) ≡ C.ρ← (₁ f) left-unit : ∀ {a b} (f : a B.↦ b) - → ₂ (B.λ← f) C.∘ γ→ B.id f C.∘ (unitor C.◀ ₁ f) ≡ C.λ← (₁ f) + → ₂ (B.λ← f) C.∘ γ→ (B.id , f) C.∘ (unitor C.◀ ₁ f) ≡ C.λ← (₁ f) ``` ## Pseudofunctors {defines="pseudofunctor"} @@ -503,17 +510,31 @@ record field unitor-inv - : ∀ {a} → Cr.is-invertible (C.Hom _ _) (unitor {a}) + : ∀ {a} → Cr.is-invertible (C.Hom _ _) (υ→ {a}) compositor-inv - : ∀ {a b c} (f : b B.↦ c) (g : a B.↦ b) → Cr.is-invertible (C.Hom _ _) (γ→ f g) - - γ← : ∀ {a b c} (f : b B.↦ c) (g : a B.↦ b) - → ₁ (f B.⊗ g) C.⇒ ₁ f C.⊗ ₁ g - γ← f g = compositor-inv f g .Cr.is-invertible.inv + : ∀ {a b c} (fg : b B.↦ c × a B.↦ b) → Cr.is-invertible (C.Hom _ _) (γ→ fg) +``` - υ← : ∀ {a} → ₁ B.id C.⇒ C.id - υ← {a} = unitor-inv {a = a} .Cr.is-invertible.inv + # Lax transformations {defines="lax-transformation"} @@ -567,8 +588,13 @@ and thus consists of a natural family of 2-cells $G(f)\sigma_a \To : ∀ {a b} → preaction C (σ b) F∘ G.P₁ => postaction C (σ a) F∘ F.P₁ - ν→ : ∀ {a b} (f : a B.↦ b) → G.₁ f C.⊗ σ a C.⇒ σ b C.⊗ F.₁ f - ν→ = naturator .η + private + open module ν→ {a} {b} = _=>_ (naturator {a} {b}) renaming (η to ν→) using () public + + ν→nat : + ∀ {A B} {f g : B B.↦ A} (α : f B.⇒ g) + → ν→ g C.∘ G.₂ α C.◀ σ B ≡ σ A C.▶ F.₂ α C.∘ ν→ f + ν→nat {A} {B} {f} {g} α = ν→.is-natural f g α ``` The naturator $\nu$ is required to be compatible with the compositor and @@ -580,8 +606,8 @@ boil down to commutativity of the nightmarish diagrams in [@basicbicats, field ν-compositor : ∀ {a b c} (f : b B.↦ c) (g : a B.↦ b) - → ν→ (f B.⊗ g) C.∘ (G.γ→ f g C.◀ σ a) - ≡ (σ c C.▶ F.γ→ f g) + → ν→ (f B.⊗ g) C.∘ (G.γ→ (f , g) C.◀ σ a) + ≡ (σ c C.▶ F.γ→ (f , g)) C.∘ C.α→ (σ c , F.₁ f , F.₁ g) C.∘ (ν→ f C.◀ F.₁ g) C.∘ C.α← (G.₁ f , σ b , F.₁ g) @@ -608,8 +634,17 @@ A lax transformation with invertible naturator is called a field naturator-inv : ∀ {a b} (f : a B.↦ b) → Cr.is-invertible (C.Hom _ _) (ν→ f) - ν← : ∀ {a b} (f : a B.↦ b) → σ b C.⊗ F.₁ f C.⇒ G.₁ f C.⊗ σ a - ν← f = naturator-inv f .Cr.is-invertible.inv + private + open module ν← {a b} f = + Cr.is-invertible (C.Hom _ _) (naturator-inv {a} {b} f) + renaming (inv to ν←) using () public + + ν←nat : + ∀ {A B} {f g : B B.↦ A} (α : f B.⇒ g) + → ν← g C.∘ σ A C.▶ F.₂ α ≡ G.₂ α C.◀ σ B C.∘ ν← f + ν←nat {A} {B} {f} {g} α = inverse-is-natural naturator ν← + (λ f → ν←.inverses f .invl) (λ f → ν←.inverses f .invr) f g α + where open Cr.Inverses ``` We abbreviate the types of lax- and pseudonatural transformations by diff --git a/src/Cat/Bi/Diagram/Monad.lagda.md b/src/Cat/Bi/Diagram/Monad.lagda.md index 86dad2b2b..341462181 100644 --- a/src/Cat/Bi/Diagram/Monad.lagda.md +++ b/src/Cat/Bi/Diagram/Monad.lagda.md @@ -194,7 +194,7 @@ $\cB$ on $a$. module monad where M = P₁.F₀ _ - μ = γ→ _ _ + μ = γ→ _ η = unitor μ-assoc = μ ∘ M ▶ μ ≡⟨ (Hom.intror $ ap (λ nt → nt ._=>_.η (M , M , M)) associator.invl) ⟩ diff --git a/src/Cat/Displayed/Cartesian/Indexing.lagda.md b/src/Cat/Displayed/Cartesian/Indexing.lagda.md index 59e991aea..2da2ebfbe 100644 --- a/src/Cat/Displayed/Cartesian/Indexing.lagda.md +++ b/src/Cat/Displayed/Cartesian/Indexing.lagda.md @@ -221,7 +221,7 @@ Fibres .lax .P₁ = base-changes Fibres .lax .compositor = Disc-natural₂ λ (f , g) → base-change-comp g f .Mor.from Fibres .lax .unitor = base-change-id .Mor.from Fibres .unitor-inv = FC.iso→invertible (base-change-id FC.Iso⁻¹) -Fibres .compositor-inv f g = FC.iso→invertible (base-change-comp g f FC.Iso⁻¹) +Fibres .compositor-inv (f , g) = FC.iso→invertible (base-change-comp g f FC.Iso⁻¹) ``` It remains to verify that this data is *coherent*, which is so tedious