From 7fbca1aeebee93ca07b09720db77408f3c20ba52 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:04:04 +0100
Subject: [PATCH] Clean-up yoneda embedding

---
 src/Cat/Category/Yoneda.agda | 55 ++++++++++++++++--------------------
 1 file changed, 24 insertions(+), 31 deletions(-)

diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda
index 365f441..87d37c0 100644
--- a/src/Cat/Category/Yoneda.agda
+++ b/src/Cat/Category/Yoneda.agda
@@ -5,23 +5,18 @@ module Cat.Category.Yoneda where
 open import Agda.Primitive
 open import Data.Product
 open import Cubical
+open import Cubical.NType.Properties
 
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Equality
-open Equality.Data.Product
 
--- TODO: We want to avoid defining the yoneda embedding going through the
--- category of categories (since it doesn't exist).
-open import Cat.Categories.Cat using (RawCat)
+open import Cat.Categories.Fun
+open import Cat.Categories.Sets
+open import Cat.Categories.Cat
 
 module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
   private
-    open import Cat.Categories.Fun
-    open import Cat.Categories.Sets
-    module Cat = Cat.Categories.Cat
-    open import Cat.Category.Exponential
-    open Functor
     𝓢 = Sets ℓ
     open Fun (opposite ℂ) 𝓢
     prshf = presheaf ℂ
@@ -34,33 +29,31 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
     --
     -- In stead we'll use an ad-hoc definition -- which is definitionally
     -- equivalent to that other one.
-    _⇑_ = Cat.CatExponential.prodObj
+    _⇑_ = CatExponential.prodObj
 
     module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where
       :func→: : NaturalTransformation (prshf A) (prshf B)
       :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.isAssociative
 
-    module _ {c : Category.Object ℂ} where
-      eqTrans : (λ _ → Transformation (prshf c) (prshf c))
-        [ (λ _ x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
-      eqTrans = funExt λ x → funExt λ x → ℂ.isIdentity .proj₂
+    rawYoneda : RawFunctor ℂ Fun
+    RawFunctor.func* rawYoneda = prshf
+    RawFunctor.func→ rawYoneda = :func→:
+    open RawFunctor rawYoneda
 
-      open import Cubical.NType.Properties
-      open import Cat.Categories.Fun
-      :ident: : :func→: (ℂ.𝟙 {c}) ≡ Category.𝟙 Fun {A = prshf c}
-      :ident: = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq
-        where
-          eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c)
-          eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
+    isIdentity : IsIdentity
+    isIdentity {c} = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq
+      where
+      eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c)
+      eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
+
+    isDistributive : IsDistributive
+    isDistributive = {!!}
+
+    instance
+      isFunctor : IsFunctor ℂ Fun rawYoneda
+      IsFunctor.isIdentity     isFunctor = isIdentity
+      IsFunctor.isDistributive isFunctor = isDistributive
 
   yoneda : Functor ℂ Fun
-  yoneda = record
-    { raw = record
-      { func* = prshf
-      ; func→ = :func→:
-      }
-    ; isFunctor = record
-      { isIdentity = :ident:
-      ; isDistributive = {!!}
-      }
-    }
+  Functor.raw yoneda = rawYoneda
+  Functor.isFunctor yoneda = isFunctor