From ce4dd83969f4ed67baca5c1ce3a576e72409f83b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 5 Mar 2018 14:42:12 +0100
Subject: [PATCH] Prove that the yoneda embedding is distributive

---
 src/Cat/Category/Yoneda.agda | 29 +++++++++++++++++++++++++----
 1 file changed, 25 insertions(+), 4 deletions(-)

diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda
index 87d37c0..88b0bbd 100644
--- a/src/Cat/Category/Yoneda.agda
+++ b/src/Cat/Category/Yoneda.agda
@@ -32,12 +32,18 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
     _⇑_ = CatExponential.prodObj
 
     module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where
-      :func→: : NaturalTransformation (prshf A) (prshf B)
-      :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.isAssociative
+      fmap : Transformation (prshf A) (prshf B)
+      fmap C x = ℂ [ f ∘ x ]
+
+      fmapNatural : Natural (prshf A) (prshf B) fmap
+      fmapNatural g = funExt λ _ → ℂ.isAssociative
+
+      fmapNT : NaturalTransformation (prshf A) (prshf B)
+      fmapNT = fmap , fmapNatural
 
     rawYoneda : RawFunctor ℂ Fun
     RawFunctor.func* rawYoneda = prshf
-    RawFunctor.func→ rawYoneda = :func→:
+    RawFunctor.func→ rawYoneda = fmapNT
     open RawFunctor rawYoneda
 
     isIdentity : IsIdentity
@@ -47,7 +53,22 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
       eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
 
     isDistributive : IsDistributive
-    isDistributive = {!!}
+    isDistributive {A} {B} {C} {f = f} {g}
+      = lemSig (propIsNatural (prshf A) (prshf C)) _ _ eq
+      where
+      T[_∘_]' = T[_∘_] {F = prshf A} {prshf B} {prshf C}
+      eqq : (X : ℂ.Object) → (x : ℂ [ X , A ])
+        → fmap (ℂ [ g ∘ f ]) X x ≡ T[ fmap g ∘ fmap f ]' X x
+      eqq X x = begin
+        fmap (ℂ [ g ∘ f ]) X x ≡⟨⟩
+        ℂ [ ℂ [ g ∘ f ] ∘ x ] ≡⟨ sym ℂ.isAssociative ⟩
+        ℂ [ g ∘ ℂ [ f ∘ x ] ] ≡⟨⟩
+        ℂ [ g ∘ fmap f X x ]  ≡⟨⟩
+        T[ fmap g ∘ fmap f ]' X x ∎
+      eq : fmap (ℂ [ g ∘ f ]) ≡ T[ fmap g ∘ fmap f ]'
+      eq = begin
+        fmap (ℂ [ g ∘ f ])    ≡⟨ funExt (λ X → funExt λ α → eqq X α) ⟩
+        T[ fmap g ∘ fmap f ]' ∎
 
     instance
       isFunctor : IsFunctor ℂ Fun rawYoneda