Skip to content

Bring End and Coend properties to parity #453

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Taneb wants to merge 4 commits into
base: master
Choose a base branch
from
+80 −50
Draft

Bring End and Coend properties to parity #453

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
f7ec508
Clean up imports in Coend/End
Taneb Feb 24, 2025
4d12561
Implement EndF as counterpart to CoendF
Taneb Feb 24, 2025
f442c88
Add coend-unique
Taneb Feb 24, 2025
665e407
Hide EndF from Properties import in End.PArameterized
Taneb Feb 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 5 additions & 12 deletions src/Categories/Diagram/Coend.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,25 +6,18 @@ open import Categories.Functor.Bifunctor using (Bifunctor)
module Categories.Diagram.Coend {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
(F : Bifunctor (Category.op C) C D) where

open Category D
open HomReasoning
open Equiv

private
module C = Category C
module D = Category D
open D
open HomReasoning
open Equiv
variable
A B : Obj
f g : A ⇒ B

open import Level

open import Categories.Diagram.Cowedge F
open import Categories.Functor
open import Categories.Functor.Construction.Constant
open import Categories.NaturalTransformation.Dinatural
open import Categories.Morphism.Reasoning D

open Functor F

record Coend : Set (levelOfTerm F) where
field
Expand All @@ -39,7 +32,7 @@ record Coend : Set (levelOfTerm F) where
universal : ∀ {W : Cowedge} {A} → factor W ∘ cowedge.dinatural.α A ≈ dinatural.α W A
unique : ∀ {W : Cowedge} {g : cowedge.E ⇒ E W} → (∀ {A} → g ∘ cowedge.dinatural.α A ≈ dinatural.α W A) → factor W ≈ g

η-id : factor cowedge ≈ D.id
η-id : factor cowedge ≈ id
η-id = unique identityˡ

unique′ :(∀ {A} → f ∘ cowedge.dinatural.α A ≈ g ∘ cowedge.dinatural.α A) → f ≈ g
Expand Down
55 changes: 32 additions & 23 deletions src/Categories/Diagram/Coend/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,11 @@ import Categories.Category.Construction.Cowedges as Cowedges
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR

private
variable
o ℓ e : Level
C D E : Category o ℓ e

module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
(F : Bifunctor (Category.op C) C D) where
open Cowedges F
Expand Down Expand Up @@ -48,44 +53,29 @@ module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′
open Initial.Initial i
open Cowedge-Morphism

private
variable
o ℓ e : Level
C D E : Category o ℓ e

module _ (F : Functor E (Functors (Product (Category.op C) C) D)) where
private
module C = Category C
module D = Category D
module E = Category E
module NT = NaturalTransformation
open D
open Category D
open HomReasoning

open MR D
open Functor F
open Coend hiding (E)
open NT using (η)
open NaturalTransformation using (η)

CoendF : (∀ X → Coend (F₀ X)) → Functor E D
CoendF coend = record
{ F₀ = λ X → Coend.E (coend X)
; F₁ = F₁′
; identity = λ {A} → unique (coend A) (id-comm-sym ○ ∘-resp-≈ʳ (⟺ identity))
; homomorphism = λ {A B C} {f g} → unique (coend A) $ λ {Z} → begin
(F₁′ g ∘ F₁′ f) ∘ dinatural.α (coend A) Z ≈⟨ pullʳ (universal (coend A)) ⟩
(F₁′ g ∘ (dinatural.α (coend B) Z ∘ η (F₁ f) (Z , Z) ) ) ≈⟨ pullˡ (universal (coend B)) ⟩
((dinatural.α (coend C) Z ∘ η (F₁ g) (Z , Z)) ∘ η (F₁ f) (Z , Z)) ≈˘⟨ pushʳ homomorphism ⟩
dinatural.α (coend C) Z ∘ η (F₁ (g E.∘ f)) (Z , Z) ∎
; F-resp-≈ = λ {A B f g} eq → unique (coend A) $ λ {Z} → begin
F₁′ g ∘ dinatural.α (coend A) Z ≈⟨ universal (coend A) ⟩
dinatural.α (coend B) Z ∘ η (F₁ g) (Z , Z) ≈˘⟨ refl⟩∘⟨ F-resp-≈ eq ⟩
dinatural.α (coend B) Z ∘ η (F₁ f) (Z , Z) ∎
; identity = unique (coend _) (id-comm-sym ○ ∘-resp-≈ʳ (⟺ identity))
; homomorphism = unique (coend _) $ glue (universal (coend _)) (universal (coend _)) ○ ∘-resp-≈ʳ (⟺ homomorphism)
; F-resp-≈ = λ eq → unique (coend _) $ universal (coend _) ○ ∘-resp-≈ʳ (⟺ (F-resp-≈ eq))
}
where F₁′ : ∀ {X Y} → X E.⇒ Y → Coend.E (coend X) ⇒ Coend.E (coend Y)
F₁′ {X} {Y} f = factor (coend X) $ record
{ E = Coend.E (coend Y)
; dinatural = dinatural (coend Y) ∘> F₁ f
F₁′ f = factor (coend _) $ record
{ E = Coend.E (coend _)
; dinatural = dinatural (coend _) ∘> F₁ f
}

-- A Natural Transformation between two functors induces an arrow between the
Expand Down Expand Up @@ -122,3 +112,22 @@ module _ {P Q : Bifunctor (Category.op C) C D} (P⇒Q : NaturalTransformation P
open Cowedge
open MR D

module _ {F : Bifunctor (Category.op C) C D} (ω₁ ω₂ : Coend F) where
private
module ω₁ = Coend ω₁
module ω₂ = Coend ω₂

open Category D using (identityˡ; module HomReasoning)
open HomReasoning using (_○_; ⟺)
open M D using (_≅_)
open MR D using (glueTrianglesˡ)

coend-unique : ω₁.E ≅ ω₂.E
coend-unique = record
{ from = ω₁.factor ω₂.cowedge
; to = ω₂.factor ω₁.cowedge
; iso = record
{ isoˡ = ω₁.unique′ (glueTrianglesˡ ω₂.universal ω₁.universal ○ ⟺ identityˡ)
; isoʳ = ω₂.unique′ (glueTrianglesˡ ω₁.universal ω₂.universal ○ ⟺ identityˡ)
}
}
11 changes: 5 additions & 6 deletions src/Categories/Diagram/End.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,19 +6,18 @@ open import Categories.Functor.Bifunctor
module Categories.Diagram.End {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
(F : Bifunctor (Category.op C) C D) where

open Category D
open HomReasoning
open Equiv

private
module D = Category D
open D
open HomReasoning
open Equiv
variable
A B : Obj
f g : A ⇒ B

open import Level

open import Categories.Diagram.Wedge F
open import Categories.NaturalTransformation.Dinatural

record End : Set (levelOfTerm F) where
field
Expand All @@ -33,7 +32,7 @@ record End : Set (levelOfTerm F) where
universal : ∀ {W : Wedge} {A} → wedge.dinatural.α A ∘ factor W ≈ dinatural.α W A
unique : ∀ {W : Wedge} {g : E W ⇒ wedge.E} → (∀ {A} → wedge.dinatural.α A ∘ g ≈ dinatural.α W A) → factor W ≈ g

η-id : factor wedge ≈ D.id
η-id : factor wedge ≈ id
η-id = unique identityʳ

unique′ :(∀ {A} → wedge.dinatural.α A ∘ f ≈ wedge.dinatural.α A ∘ g) → f ≈ g
Expand Down
2 changes: 1 addition & 1 deletion src/Categories/Diagram/End/Parameterized.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ open import Categories.Category.Construction.Functors
open import Categories.Category.Product renaming (Product to _×ᶜ_)
open import Categories.Diagram.End renaming (End to ∫)
open import Categories.Diagram.End.Limit
open import Categories.Diagram.End.Properties
open import Categories.Diagram.End.Properties hiding (EndF)
open import Categories.Diagram.Wedge
open import Categories.Functor hiding (id)
open import Categories.Functor.Bifunctor
Expand Down
45 changes: 37 additions & 8 deletions src/Categories/Diagram/End/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ open import Function using (_$_)

open import Categories.Category using (Category)
open import Categories.Category.Construction.Functors using (Functors)
open import Categories.Category.Product using (Product)
open import Categories.Diagram.End using () renaming (End to ∫)
open import Categories.Diagram.Wedge using (Wedge; module Wedge-Morphism)
open import Categories.Functor using (Functor)
Expand All @@ -30,7 +31,7 @@ import Categories.Morphism.Reasoning as MR
private
variable
o ℓ e o′ ℓ′ e′ : Level
P C D : Category o ℓ e
P C D E : Category o ℓ e

open Category using (o-level; ℓ-level; e-level)

Expand Down Expand Up @@ -60,6 +61,32 @@ module _ (F : Bifunctor (Category.op C) C D) where
open Terminal.Terminal i
open Wedge-Morphism

module _ (F : Functor E (Functors (Product (Category.op C) C) D)) where

private
module E = Category E

open Category D
open HomReasoning
open MR D
open Functor F
open NaturalTransformation using (η)

EndF : (∀ X → ∫ (F₀ X)) → Functor E D
EndF end = record
{ F₀ = λ X → ∫.E (end X)
; F₁ = F₁′
; identity = ∫.unique (end _) $ id-comm ○ ∘-resp-≈ˡ (⟺ identity)
; homomorphism = ∫.unique (end _) $ glue′ (∫.universal (end _)) (∫.universal (end _)) ○ ∘-resp-≈ˡ (⟺ homomorphism)
; F-resp-≈ = λ eq → ∫.unique (end _) $ ∫.universal (end _) ○ ∘-resp-≈ˡ (⟺ (F-resp-≈ eq))
}
where
F₁′ : ∀ {X Y} → X E.⇒ Y → ∫.E (end X) ⇒ ∫.E (end Y)
F₁′ f = ∫.factor (end _) record
{ E = ∫.E (end _)
; dinatural = F₁ f <∘ ∫.dinatural (end _)
}

-- A Natural Transformation between two functors induces an arrow between the
-- (object part of) the respective ends.
module _ {F G : Bifunctor (Category.op C) C D} (F⇒G : NaturalTransformation F G) where
Expand Down Expand Up @@ -101,17 +128,19 @@ module _ {F : Bifunctor (Category.op C) C D} (ω₁ ω₂ : ∫ F) where
module ω₁ = ∫ ω₁
module ω₂ = ∫ ω₂
open Category D
open HomReasoning
open M D
open _≅_
open Iso
open MR D
open HomReasoning

end-unique : ∫.E ω₁ ≅ ∫.E ω₂
end-unique .to = ω₁.factor ω₂.wedge
end-unique .from = ω₂.factor ω₁.wedge
end-unique .iso .isoʳ = ω₂.unique′ $ pullˡ ω₂.universal ○ ω₁.universal ○ ⟺ identityʳ
end-unique .iso .isoˡ = ω₁.unique′ $ pullˡ ω₁.universal ○ ω₂.universal ○ ⟺ identityʳ
end-unique = record
{ from = ω₂.factor ω₁.wedge
; to = ω₁.factor ω₂.wedge
; iso = record
{ isoˡ = ω₁.unique′ (glueTrianglesʳ ω₁.universal ω₂.universal ○ ⟺ identityʳ)
; isoʳ = ω₂.unique′ (glueTrianglesʳ ω₂.universal ω₁.universal ○ ⟺ identityʳ)
}
}

module _ {C : Category o ℓ e } {D : Category o′ ℓ′ e′} where
open MR D
Expand Down