Merge branch 'Saizan-dev-yoneda'

README.md

@@ -6,7 +6,7 @@ consisting of the proposal for the thesis).
 Installation
 ============
 You probably need a very recent version of the Agda compiler. At the time
-of writing the solution has been tested with Agda version 2.6.0-9af3e07.
+of writing the solution has been tested with Agda version 2.6.0-5d84754.
 
 Dependencies
 ------------

src/Cat/Categories/Cat.agda

@@ -34,8 +34,6 @@ module _ (ℓ ℓ' : Level) where
           (λ i → {x y : A .Object} → A .Arrow x y → D .Arrow (eq* i x) (eq* i y))
           (func→ (h ∘f (g ∘f f))) (func→ ((h ∘f g) ∘f f))
         eq→ = refl
-        id-l = (h ∘f (g ∘f f)) .ident -- = func→ (h ∘f (g ∘f f)) (𝟙 A) ≡ 𝟙 D
-        id-r = ((h ∘f g) ∘f f) .ident -- = func→ ((h ∘f g) ∘f f) (𝟙 A) ≡ 𝟙 D
         postulate eqI : PathP
                    (λ i → ∀ {c : A .Object} → eq→ i (A .𝟙 {c}) ≡ D .𝟙 {eq* i c})
                    (ident ((h ∘f (g ∘f f))))

src/Cat/Category/Properties.agda

@@ -52,12 +52,12 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
   open import Cat.Category
   open Category
   open import Cat.Categories.Cat using (Cat)
+  open import Cat.Categories.Fun
+  open import Cat.Categories.Sets
   module Cat = Cat.Categories.Cat
   open Exponential
   private
     Catℓ = Cat ℓ ℓ
-    CatHasExponentials : HasExponentials Catℓ
-    CatHasExponentials = Cat.hasExponentials ℓ
 
   -- Exp : Set (lsuc (lsuc ℓ))
   -- Exp = Exponential (Cat (lsuc ℓ) ℓ)
@@ -66,18 +66,26 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
   _⇑_ : (A B : Catℓ .Object) → Catℓ .Object
   A ⇑ B = (exponent A B) .obj
     where
-      open HasExponentials CatHasExponentials
+      open HasExponentials (Cat.hasExponentials ℓ)
 
-  private
+  -- private
-    -- I need `Sets` to be a `Category ℓ ℓ` but it simlpy isn't.
+  --   -- I need `Sets` to be a `Category ℓ ℓ` but it simlpy isn't.
-    Setz : Category ℓ ℓ
+  --   Setz : Category ℓ ℓ
-    Setz = {!Sets!}
+  --   Setz = {!Sets!}
-    :func*: : ℂ .Object → (Setz ⇑ Opposite ℂ) .Object
+  --   :func*: : ℂ .Object → (Setz ⇑ Opposite ℂ) .Object
-    :func*: A = {!!}
+  --   :func*: A = {!!}
 
-  yoneda : Functor ℂ (Setz ⇑ (Opposite ℂ))
+    -- prsh = presheaf {ℂ = ℂ}
+    -- k = prsh {!!}
+    -- :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* = :func*:
+    { func* = presheaf {ℂ = ℂ}
     ; func→ = {!!}
     ; ident = {!!}
     ; distrib = {!!}