From b768eacba6caed2ce10d631a5d6778bc3b0c6dcf Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 25 Jan 2024 16:28:43 +0100 Subject: [PATCH] properties of distributive categories --- src/Categories/Category/Distributive.agda | 94 +++++++++++++++++++++++ 1 file changed, 94 insertions(+) diff --git a/src/Categories/Category/Distributive.agda b/src/Categories/Category/Distributive.agda index bc4bcdad..8be2ff84 100644 --- a/src/Categories/Category/Distributive.agda +++ b/src/Categories/Category/Distributive.agda @@ -7,6 +7,8 @@ open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Cocartesian using (Cocartesian) import Categories.Morphism as M import Categories.Morphism.Reasoning as MR +import Categories.Morphism.Properties as MP + -- A distributive category is a cartesian, cocartesian category -- where the canonical distributivity morphism is an iso @@ -16,6 +18,7 @@ module Categories.Category.Distributive {o ℓ e} (𝒞 : Category o ℓ e) wher open Category 𝒞 open M 𝒞 open MR 𝒞 +open MP 𝒞 open HomReasoning open Equiv @@ -63,3 +66,94 @@ record Distributive : Set (levelOfTerm 𝒞) where } where open IsIso (isIsoˡ {A} {B} {C}) + + -- the inverse is what one is usually interested in + distributeˡ⁻¹ : ∀ {A B C : Obj} → A × (B + C) ⇒ A × B + A × C + distributeˡ⁻¹ = IsIso.inv isIsoˡ + + distributeʳ⁻¹ : ∀ {A B C : Obj} → (B + C) × A ⇒ B × A + C × A + distributeʳ⁻¹ = IsIso.inv isIsoʳ + + -- distribution and injection + distributeˡ⁻¹-i₁ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (id ⁂ i₁) ≈ i₁ + distributeˡ⁻¹-i₁ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ)) + + distributeˡ⁻¹-i₂ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (id ⁂ i₂) ≈ i₂ + distributeˡ⁻¹-i₂ = (refl⟩∘⟨ (sym inject₂)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ)) + + distributeʳ⁻¹-i₁ : ∀ {A B C} → distributeʳ⁻¹ {A} {B} {C} ∘ (i₁ ⁂ id) ≈ i₁ + distributeʳ⁻¹-i₁ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoʳ)) + + distributeʳ⁻¹-i₂ : ∀ {A B C} → distributeʳ⁻¹ {A} {B} {C} ∘ (i₂ ⁂ id) ≈ i₂ + distributeʳ⁻¹-i₂ = (refl⟩∘⟨ (sym inject₂)) ○ (cancelˡ (IsIso.isoˡ isIsoʳ)) + + -- distribution and projection + distributeˡ⁻¹-π₁ : ∀ {A B C} → [ π₁ , π₁ ] ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₁ + distributeˡ⁻¹-π₁ = sym (begin + π₁ ≈⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩ + π₁ ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ pullˡ ∘[] ⟩ + ([ π₁ ∘ ((id ⁂ i₁)) , π₁ ∘ (id ⁂ i₂) ] ∘ distributeˡ⁻¹) ≈⟨ (([]-cong₂ (π₁∘⁂ ○ identityˡ) (π₁∘⁂ ○ identityˡ)) ⟩∘⟨refl) ⟩ + [ π₁ , π₁ ] ∘ distributeˡ⁻¹ ∎) + + distributeʳ⁻¹-π₁ : ∀ {A B C} → (π₁ +₁ π₁) ∘ distributeʳ⁻¹ {A} {B} {C} ≈ π₁ + distributeʳ⁻¹-π₁ = sym (begin + π₁ ≈⟨ introʳ (IsIso.isoʳ isIsoʳ) ⟩ + π₁ ∘ distributeʳ ∘ distributeʳ⁻¹ ≈⟨ pullˡ ∘[] ⟩ + [ π₁ ∘ (i₁ ⁂ id) , π₁ ∘ (i₂ ⁂ id) ] ∘ distributeʳ⁻¹ ≈⟨ (([]-cong₂ π₁∘⁂ π₁∘⁂) ⟩∘⟨refl) ⟩ + ((π₁ +₁ π₁) ∘ distributeʳ⁻¹) ∎) + + distributeˡ⁻¹-π₂ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂ + distributeˡ⁻¹-π₂ = sym (begin + π₂ ≈⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩ + π₂ ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ pullˡ ∘[] ⟩ + [ π₂ ∘ ((id ⁂ i₁)) , π₂ ∘ (id ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩ + (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∎) + + distributeʳ⁻¹-π₂ : ∀ {A B C} → [ π₂ , π₂ ] ∘ distributeʳ⁻¹ {A} {B} {C} ≈ π₂ + distributeʳ⁻¹-π₂ = sym (begin + π₂ ≈⟨ introʳ (IsIso.isoʳ isIsoʳ) ⟩ + π₂ ∘ distributeʳ ∘ distributeʳ⁻¹ ≈⟨ pullˡ ∘[] ⟩ + ([ π₂ ∘ ((i₁ ⁂ id)) , π₂ ∘ (i₂ ⁂ id) ] ∘ distributeʳ⁻¹) ≈⟨ (([]-cong₂ (π₂∘⁂ ○ identityˡ) (π₂∘⁂ ○ identityˡ)) ⟩∘⟨refl) ⟩ + [ π₂ , π₂ ] ∘ distributeʳ⁻¹ ∎) + + -- distribute over products + distributeˡ⁻¹-natural : ∀ {X Y Z U V W} (f : X ⇒ U) (g : Y ⇒ V) (h : Z ⇒ W) → ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈ distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h)) + distributeˡ⁻¹-natural f g h = begin + ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈⟨ introˡ (IsIso.isoˡ isIsoˡ) ⟩ + (distributeˡ⁻¹ ∘ distributeˡ) ∘ ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈⟨ pullˡ (pullʳ []∘+₁) ⟩ + (distributeˡ⁻¹ ∘ [(id ⁂ i₁) ∘ (f ⁂ g) , (id ⁂ i₂) ∘ (f ⁂ h)]) ∘ distributeˡ⁻¹ ≈⟨ (refl⟩∘⟨ ([]-cong₂ ⁂∘⁂ ⁂∘⁂)) ⟩∘⟨refl ⟩ + (distributeˡ⁻¹ ∘ [ id ∘ f ⁂ i₁ ∘ g , id ∘ f ⁂ i₂ ∘ h ]) ∘ distributeˡ⁻¹ ≈˘⟨ (refl⟩∘⟨ ([]-cong₂ (⁂-cong₂ id-comm +₁∘i₁) (⁂-cong₂ id-comm +₁∘i₂))) ⟩∘⟨refl ⟩ + (distributeˡ⁻¹ ∘ [ f ∘ id ⁂ (g +₁ h) ∘ i₁ , f ∘ id ⁂ (g +₁ h) ∘ i₂ ]) ∘ distributeˡ⁻¹ ≈˘⟨ (refl⟩∘⟨ ([]-cong₂ ⁂∘⁂ ⁂∘⁂)) ⟩∘⟨refl ⟩ + (distributeˡ⁻¹ ∘ [ ((f ⁂ (g +₁ h)) ∘ (id ⁂ i₁)) , ((f ⁂ (g +₁ h)) ∘ (id ⁂ i₂)) ]) ∘ distributeˡ⁻¹ ≈˘⟨ pullˡ (pullʳ ∘[]) ⟩ + (distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h))) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈˘⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩ + distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h)) ∎ + + distributeʳ⁻¹-natural : ∀ {X Y Z U V W} (f : X ⇒ U) (g : Y ⇒ V) (h : Z ⇒ W) → ((g ⁂ f) +₁ (h ⁂ f)) ∘ distributeʳ⁻¹ ≈ distributeʳ⁻¹ ∘ ((g +₁ h) ⁂ f) + distributeʳ⁻¹-natural f g h = begin + ((g ⁂ f) +₁ (h ⁂ f)) ∘ distributeʳ⁻¹ ≈⟨ introˡ (IsIso.isoˡ isIsoʳ) ⟩ + (distributeʳ⁻¹ ∘ distributeʳ) ∘ (g ⁂ f +₁ h ⁂ f) ∘ distributeʳ⁻¹ ≈⟨ pullˡ (pullʳ []∘+₁) ⟩ + (distributeʳ⁻¹ ∘ [ (i₁ ⁂ id) ∘ (g ⁂ f) , (i₂ ⁂ id) ∘ (h ⁂ f) ]) ∘ distributeʳ⁻¹ ≈⟨ (refl⟩∘⟨ ([]-cong₂ ⁂∘⁂ ⁂∘⁂)) ⟩∘⟨refl ⟩ + (distributeʳ⁻¹ ∘ [ (i₁ ∘ g ⁂ id ∘ f) , (i₂ ∘ h ⁂ id ∘ f) ]) ∘ distributeʳ⁻¹ ≈˘⟨ (refl⟩∘⟨ ([]-cong₂ (⁂-cong₂ +₁∘i₁ id-comm) (⁂-cong₂ +₁∘i₂ id-comm))) ⟩∘⟨refl ⟩ + (distributeʳ⁻¹ ∘ [ ((g +₁ h) ∘ i₁ ⁂ f ∘ id) , ((g +₁ h) ∘ i₂ ⁂ f ∘ id) ]) ∘ distributeʳ⁻¹ ≈˘⟨ (refl⟩∘⟨ ([]-cong₂ ⁂∘⁂ ⁂∘⁂)) ⟩∘⟨refl ⟩ + (distributeʳ⁻¹ ∘ [ ((g +₁ h) ⁂ f) ∘ (i₁ ⁂ id) , ((g +₁ h) ⁂ f) ∘ (i₂ ⁂ id) ]) ∘ distributeʳ⁻¹ ≈˘⟨ pullˡ (pullʳ ∘[]) ⟩ + (distributeʳ⁻¹ ∘ ((g +₁ h) ⁂ f)) ∘ distributeʳ ∘ distributeʳ⁻¹ ≈˘⟨ introʳ (IsIso.isoʳ isIsoʳ) ⟩ + distributeʳ⁻¹ ∘ ((g +₁ h) ⁂ f) ∎ + + -- distribute and swap + distributeˡ⁻¹∘swap : ∀ {A B C : Obj} → distributeˡ⁻¹ ∘ swap ≈ (swap +₁ swap) ∘ distributeʳ⁻¹ {A} {B} {C} + distributeˡ⁻¹∘swap = Iso⇒Mono (IsIso.iso isIsoˡ) (distributeˡ⁻¹ ∘ swap) ((swap +₁ swap) ∘ distributeʳ⁻¹) (begin + (distributeˡ ∘ distributeˡ⁻¹ ∘ swap) ≈⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩ + swap ≈˘⟨ cancelʳ (IsIso.isoʳ isIsoʳ) ⟩ + ((swap ∘ distributeʳ) ∘ distributeʳ⁻¹) ≈⟨ ∘[] ⟩∘⟨refl ⟩ + [ swap ∘ (i₁ ⁂ id) , swap ∘ (i₂ ⁂ id) ] ∘ distributeʳ⁻¹ ≈˘⟨ []-cong₂ (sym swap∘⁂) (sym swap∘⁂) ⟩∘⟨refl ⟩ + [ (id ⁂ i₁) ∘ swap , (id ⁂ i₂) ∘ swap ] ∘ distributeʳ⁻¹ ≈˘⟨ pullˡ []∘+₁ ⟩ + distributeˡ ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ ∎) + + distributeʳ⁻¹∘swap : ∀ {A B C : Obj} → distributeʳ⁻¹ ∘ swap ≈ (swap +₁ swap) ∘ distributeˡ⁻¹ {A} {B} {C} + distributeʳ⁻¹∘swap = Iso⇒Mono (IsIso.iso isIsoʳ) (distributeʳ⁻¹ ∘ swap) ((swap +₁ swap) ∘ distributeˡ⁻¹) (begin + (distributeʳ ∘ distributeʳ⁻¹ ∘ swap) ≈⟨ cancelˡ (IsIso.isoʳ isIsoʳ) ⟩ + swap ≈˘⟨ cancelʳ (IsIso.isoʳ isIsoˡ) ⟩ + ((swap ∘ distributeˡ) ∘ distributeˡ⁻¹) ≈⟨ (∘[] ⟩∘⟨refl) ⟩ + [ swap ∘ (id ⁂ i₁) , swap ∘ (id ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈˘⟨ ([]-cong₂ (sym swap∘⁂) (sym swap∘⁂)) ⟩∘⟨refl ⟩ + [ (i₁ ⁂ id) ∘ swap , (i₂ ⁂ id) ∘ swap ] ∘ distributeˡ⁻¹ ≈˘⟨ pullˡ []∘+₁ ⟩ + (distributeʳ ∘ (swap +₁ swap) ∘ distributeˡ⁻¹) ∎)