Unfinished stuff about HOM-sets and exponentials

src/Cat/Categories/Sets.agda

@@ -1,8 +1,14 @@
-module Category.Sets where
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module Cat.Categories.Sets where
 
 open import Cubical.PathPrelude
 open import Agda.Primitive
-open import Category
+open import Data.Product
+open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
+
+open import Cat.Category
+open import Cat.Functor
 
 -- Sets are built-in to Agda. The set of all small sets is called Set.
 
@@ -27,8 +33,28 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ}} where
   RepFunctor : Functor ℂ Sets
   RepFunctor =
     record
-    { F = λ A → (B : C-Obj) → Hom {ℂ = ℂ} A B
-    ; f = λ { {c' = c'} f g → {!HomFromArrow {ℂ = } c' g!}}
-    ; ident = {!!}
-    ; distrib = {!!}
-    }
+      { func* = λ A → (B : C-Obj) → Hom {ℂ = ℂ} A B
+      ; func→ = λ { {c} {c'} f g → {!HomFromArrow {ℂ = {!!}} c' g!} }
+      ; ident = {!!}
+      ; distrib = {!!}
+      }
+
+Hom0 : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor ℂ (Sets {ℓ'})
+Hom0 {ℂ = ℂ} A = record
+  { func* = λ B → ℂ.Arrow A B
+  ; func→ = λ f g → f ℂ.⊕ g
+  ; ident = funExt λ _ → snd ℂ.ident
+  ; distrib = funExt λ x → sym ℂ.assoc
+  }
+  where
+    open module ℂ = Category ℂ
+
+Hom1 : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor (Opposite ℂ) (Sets {ℓ'})
+Hom1 {ℂ = ℂ} B = record
+  { func* = λ A → ℂ.Arrow A B
+  ; func→ = λ f g → {!!} ℂ.⊕ {!!}
+  ; ident = {!!}
+  ; distrib = {!!}
+  }
+  where
+    open module ℂ = Category ℂ

src/Cat/Category/Properties.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module Cat.Category.Properties where
+
+open import Cat.Category
+open import Cat.Functor
+open import Cat.Categories.Sets
+
+module _ {ℓa ℓa' ℓb ℓb'} where
+  Exponential : Category {ℓa} {ℓa'} → Category {ℓb} {ℓb'} → Category {{!!}} {{!!}}
+  Exponential A B = record
+    { Object = {!!}
+    ; Arrow = {!!}
+    ; 𝟙 = {!!}
+    ; _⊕_ = {!!}
+    ; assoc = {!!}
+    ; ident = {!!}
+    }
+
+_⇑_ = Exponential
+
+yoneda : ∀ {ℓ ℓ'} → {ℂ : Category {ℓ} {ℓ'}} → Functor ℂ (Sets ⇑ (Opposite ℂ))
+yoneda = {!!}

src/Cat/Functor.agda

@@ -8,7 +8,6 @@ open import Cat.Category
 
 record Functor {ℓc ℓc' ℓd ℓd'} (C : Category {ℓc} {ℓc'}) (D : Category {ℓd} {ℓd'})
   : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
-  constructor functor
   private
     open module C = Category C
     open module D = Category D
@@ -59,4 +58,9 @@ module _ {ℓ ℓ' : Level} {A B C : Category {ℓ} {ℓ'}} (F : Functor B C) (G
 -- The identity functor
 identity : {ℓ ℓ' : Level} → {C : Category {ℓ} {ℓ'}} → Functor C C
 -- Identity = record { F* = λ x → x ; F→ = λ x → x ; ident = refl ; distrib = refl }
-identity = functor (λ x → x) (λ x → x) (refl) (refl)
+identity = record
+  { func* = λ x → x
+  ; func→ = λ x → x
+  ; ident = refl
+  ; distrib = refl
+  }