Merge pull request #462 from agda/naturaltransformations-end

The set of natural transformations between two functors is an end

Author: JacquesCarette

src/Categories/Diagram/End/Instance/NaturalTransformations.agda

@@ -0,0 +1,78 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Categories.Functor using (Functor)
+
+open import Level
+
+module Categories.Diagram.End.Instance.NaturalTransformations
+  {o ℓ e o′ ℓ′ e′}
+  {C : Category o ℓ e}
+  {D : Category o′ (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)}
+  (F G : Functor C D)
+  where
+
+open import Categories.Category.Construction.Functors using (Functors)
+open import Categories.Diagram.End using (End)
+open import Categories.Diagram.Wedge using (Wedge)
+open import Categories.Functor.Bifunctor using (reduce-×)
+open import Categories.Functor.Hom using (Hom[_][-,-]; Hom[_][_,_])
+open import Categories.Morphism.Reasoning D
+open import Categories.NaturalTransformation using (NaturalTransformation)
+
+open import Function.Bundles using (Func; _⟨$⟩_)
+
+private
+  module F = Functor F
+  module G = Functor G
+
+open Category C using (id)
+open Category D hiding (id)
+open HomReasoning
+open NaturalTransformation
+open Wedge
+
+-- For appropriately sized categories, the set of natural
+-- transformations from F to G forms the end ∫ₓ F x ⇒ G x
+-- This is Theorem 1.4.1 of Coend calculus
+
+naturalTransformations : End (reduce-× Hom[ D ][-,-] F.op G)
+naturalTransformations = record
+  { wedge = record
+    { E = Hom[ Functors C D ][ F , G ]
+    ; dinatural = record
+      { α = λ X → record
+        { to = λ nt → η nt X
+        ; cong = λ eq → eq
+        }
+      ; commute = λ {X Y} f {nt} → begin
+        G.₁ f ∘ η nt X ∘ F.₁ id ≈⟨ refl⟩∘⟨ elimʳ F.identity ⟩
+        G.₁ f ∘ η nt X          ≈⟨ sym-commute nt f ⟩
+        η nt Y ∘ F.₁ f          ≈⟨ pushˡ (introˡ G.identity) ⟩
+        G.₁ id ∘ η nt Y ∘ F.₁ f ∎
+      ; op-commute = λ {X Y} f {nt} → begin
+        G.₁ id ∘ η nt Y ∘ F.₁ f ≈⟨ pullˡ (elimˡ G.identity) ⟩
+        η nt Y ∘ F.₁ f          ≈⟨ commute nt f ⟩
+        G.₁ f ∘ η nt X          ≈⟨ refl⟩∘⟨ introʳ F.identity ⟩
+        G.₁ f ∘ η nt X ∘ F.₁ id ∎
+      }
+    }
+  ; factor = λ W → record
+    { to = λ e → record
+      { η = λ X → dinatural.α W X ⟨$⟩ e
+      ; commute = λ {X Y} f → begin
+        (dinatural.α W Y ⟨$⟩ e) ∘ F.₁ f          ≈⟨ pushˡ (introˡ G.identity) ⟩
+        G.₁ id ∘ (dinatural.α W Y ⟨$⟩ e) ∘ F.₁ f ≈⟨ dinatural.op-commute W f ⟩
+        G.₁ f ∘ (dinatural.α W X ⟨$⟩ e) ∘ F.₁ id ≈⟨ refl⟩∘⟨ elimʳ F.identity ⟩
+        G.₁ f ∘ (dinatural.α W X ⟨$⟩ e)          ∎
+      ; sym-commute = λ {X Y} f → begin
+        G.₁ f ∘ (dinatural.α W X ⟨$⟩ e)          ≈⟨ refl⟩∘⟨ introʳ F.identity ⟩
+        G.₁ f ∘ (dinatural.α W X ⟨$⟩ e) ∘ F.₁ id ≈⟨ dinatural.commute W f ⟩
+        G.₁ id ∘ (dinatural.α W Y ⟨$⟩ e) ∘ F.₁ f ≈⟨ pullˡ (elimˡ G.identity) ⟩
+        (dinatural.α W Y ⟨$⟩ e) ∘ F.₁ f          ∎
+      }
+    ; cong = λ eq → Func.cong (dinatural.α W _) eq
+    }
+  ; universal = Equiv.refl
+  ; unique = λ eq → Equiv.sym eq
+  }