module Cat.Diagram.Coend.Sets where
Coends in Sets🔗
We can give an explicit construction of coends in the category of sets by
taking a coequaliser.
Intuitively, the coend should be the “sum of the diagonal” of a functor
which translates directly to the sigma type
Σ[ X ∈ Ob ] ∣ F₀ (X , X) ∣. However, trying to use this
without some sort of quotient is going to be immediately problematic.
For starters, this isn’t even a set! More importantly, we run into an
immediate issue when we try to prove that this is extranatural; we need
to show that F₁ (f , id) Fyx ≡ F₁ (id , f) Fyx for all
f : Hom Y X and ∣ Fyx : F₀ (X , Y) ∣.
However, if we take a coequaliser of
Σ[ X ∈ Ob ] ∣ F₀ (X , X) ∣ both of these problems
immediately disappear. In particular, we want to take the coequaliser of
the following pair of functions:
This allows us to prove the troublesome extranaturality condition
directly with glue. With that motivation out
of the way, let’s continue with the construction!
module mk {o ℓ} {C : Precategory o ℓ} (F : Bifunctor (C ^op) C (Sets (o ⊔ ℓ))) where open Precategory C open Cowedge open Coend open Bifunctor F
We start by defining the two maps we will coequalise along. Quite a bit of bundling is required to make things well typed, but this is exactly the same pair of maps in the diagram above.
dimapl : Σ[ X ∈ C ] Σ[ Y ∈ C ] Σ[ f ∈ Hom Y X ] ⌞ F · X · Y ⌟ → Σ[ X ∈ C ] ⌞ F · X · X ⌟ dimapl (X , Y , f , Fxy) = X , rmap f Fxy dimapr : Σ[ X ∈ C ] Σ[ Y ∈ C ] Σ[ f ∈ Hom Y X ] ⌞ F · X · Y ⌟ → Σ[ X ∈ C ] ⌞ F · X · X ⌟ dimapr (X , Y , f , Fxy) = Y , lmap f Fxy
record Coend₀ : Type (o ⊔ ℓ) where constructor lift field lower : Coeq dimapl dimapr
begin : ∀ x → ⌞ F · x · x ⌟ → Coend₀ begin a x = lift (inc (a , x)) unquoteDecl H-Level-Coend₀ = declare-record-hlevel 2 H-Level-Coend₀ (quote Coend₀) abstract coend-glue : ∀ {x y} (f : Hom y x) (a : ⌞ F · x · y ⌟) → Path Coend₀ (begin x (rmap f a)) (begin y (lmap f a)) coend-glue f a = ap {B = λ _ → Coend₀} lift (Coeq.glue {f = dimapl} {g = dimapr} (_ , _ , f , a)) instance Extensional-coend-map : ∀ {ℓ' ℓr} {T : Type ℓ'} ⦃ _ : Extensional ((x : ⌞ C ⌟) → ⌞ F · x · x ⌟ → T) ℓr ⦄ → ⦃ _ : H-Level T 2 ⦄ → Extensional (Coend₀ → T) ℓr Extensional-coend-map {T = T} = injection→extensional! {B = Coeq dimapl dimapr → T} {f = λ f x → f (lift x)} (λ p → funext (λ { (lift x) → p ·ₚ x })) auto Inductive-coend : ∀ {ℓ ℓm} {P : Coend₀ → Type ℓ} → ⦃ _ : Inductive ((x : Coeq dimapl dimapr) → P (lift x)) ℓm ⦄ → Inductive (∀ x → P x) ℓm Inductive-coend {P = P} ⦃ i ⦄ = record { methods = i .Inductive.methods ; from = λ z x → i .Inductive.from z (x .Coend₀.lower) }
Constructing the universal Cowedge is easy now that we’ve
taken the right coequaliser.
Set-coend : Coend F Set-coend = coend where universal-cowedge : Cowedge F universal-cowedge .nadir = el! Coend₀ universal-cowedge .ψ X Fxx = begin X Fxx universal-cowedge .extranatural {X} {Y} f = ext λ x → coend-glue _ _
To show that the Cowedge is universal, we can
essentially just project out the bundled up object from the coend and
feed that to the family associated to the cowedge W.
factoring : (W : Cowedge F) → Coeq dimapl dimapr → ⌞ W .nadir ⌟ factoring W (inc (o , x)) = W .ψ o x factoring W (glue (X , Y , f , Fxy) i) = W .extranatural f i Fxy factoring W (squash x y p q i j) = W .nadir .is-tr (factoring W x) (factoring W y) (λ i → factoring W (p i)) (λ i → factoring W (q i)) i j coend : Coend F coend .cowedge = universal-cowedge coend .factor W (lift x) = factoring W x coend .commutes = refl coend .unique {W = W} p = ext λ X x → sym p ·ₚ x
This construction is actually functorial! Given any functor we can naturally construct its Coend in This ends up assembling into a functor from the functor category into
open mk hiding (H-Level-Coend₀ ; Extensional-coend-map ; Inductive-coend ; begin ; coend-glue) public module _ {o ℓ} {C : Precategory o ℓ} {F : Bifunctor (C ^op) C (Sets (o ⊔ ℓ))} where open mk F using (H-Level-Coend₀ ; Extensional-coend-map ; Inductive-coend ; begin ; coend-glue) public {-# DISPLAY mk.lift (Coeq.inc (a , b)) = begin a b #-}
module _ {o ℓ} {𝒞 : Precategory o ℓ} where open Precategory 𝒞 open Functor open _=>_ Coends : Functor (Cat[ 𝒞 ^op , Cat[ 𝒞 , Sets (o ⊔ ℓ) ] ]) (Sets (o ⊔ ℓ)) Coends .F₀ F = el! (Coeq (dimapl F) (dimapr F)) Coends .F₁ α = rec! λ where .inc* i x → inc (i , α · _ · _ · x) .glue* → ext λ X Y f Fxy → ap (λ ϕ → Coeq.inc (X , ϕ)) (α .η _ .is-natural _ _ _ ·ₚ _) ∙∙ glue (X , Y , f , α .η X .η Y Fxy) ∙∙ sym (ap (λ ϕ → Coeq.inc (Y , ϕ)) (α .is-natural _ _ _ ·ₚ _ ·ₚ _)) Coends .F-id = ext λ _ _ → refl Coends .F-∘ f g = ext λ _ _ → refl