Prove that the yoneda embedding is distributive

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)
+      fmap : Transformation (prshf A) (prshf B)
-      :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.isAssociative
+      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