One step closer to yoneda

src/Cat/Category/Properties.agda

@@ -58,35 +58,35 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
   open Exponential
   private
     Catℓ = Cat ℓ ℓ
+    prshf = presheaf {ℂ = ℂ}
 
-  -- Exp : Set (lsuc (lsuc ℓ))
+    -- Exp : Set (lsuc (lsuc ℓ))
-  -- Exp = Exponential (Cat (lsuc ℓ) ℓ)
+    -- Exp = Exponential (Cat (lsuc ℓ) ℓ)
-  --   Sets (Opposite ℂ)
+    --   Sets (Opposite ℂ)
 
-  _⇑_ : (A B : Catℓ .Object) → Catℓ .Object
+    _⇑_ : (A B : Catℓ .Object) → Catℓ .Object
-  A ⇑ B = (exponent A B) .obj
+    A ⇑ B = (exponent A B) .obj
-    where
+      where
-      open HasExponentials (Cat.hasExponentials ℓ)
+        open HasExponentials (Cat.hasExponentials ℓ)
 
-  -- private
+    module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where
-  --   -- I need `Sets` to be a `Category ℓ ℓ` but it simlpy isn't.
+      :func→: : NaturalTransformation (prshf A) (prshf B)
-  --   Setz : Category ℓ ℓ
+      :func→: = (λ C x → (ℂ ._⊕_ f x)) , λ f₁ → funExt λ x → lem
-  --   Setz = {!Sets!}
+        where
-  --   :func*: : ℂ .Object → (Setz ⇑ Opposite ℂ) .Object
+          lem = (ℂ .isCategory) .IsCategory.assoc
-  --   :func*: A = {!!}
+    module _ {c : ℂ .Object} where
+      eqTrans : (:func→: (ℂ .𝟙 {c})) .proj₁ ≡ (Fun .𝟙 {o = prshf c}) .proj₁
+      eqTrans = funExt λ x → funExt λ x → ℂ .isCategory .IsCategory.ident .proj₂
+      eqNat : (i : I) → Natural (prshf c) (prshf c) (eqTrans i)
+      eqNat i f = {!!}
 
-    -- prsh = presheaf {ℂ = ℂ}
+      :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c})
-    -- k = prsh {!!}
+      :ident: i = eqTrans i , eqNat i
-    -- :func*:' : ℂ .Object → Presheaf ℂ
-    -- :func*:' = prsh
-    -- module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where
-    --   open import Cat.Categories.Fun
-    --   :func→:' : NaturalTransformation (prsh A) (prsh B)
 
   yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}})
   yoneda = record
-    { func* = presheaf {ℂ = ℂ}
+    { func* = prshf
-    ; func→ = {!!}
+    ; func→ = :func→:
-    ; ident = {!!}
+    ; ident = :ident:
     ; distrib = {!!}
     }