From 902b953ad0232876c2a7c7de0c474e420047c3c2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 17 Jan 2018 12:10:18 +0100
Subject: [PATCH] Implement representable functors

---
 src/Cat/Categories/Sets.agda | 28 +++++++---------------------
 src/Cat/Category.agda        |  6 +++---
 2 files changed, 10 insertions(+), 24 deletions(-)

diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index b8584bc..4e784b6 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -25,22 +25,8 @@ Sets {ℓ} = record
   ; ident = funExt (λ x → refl) , funExt (λ x → refl)
   }
 
-module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ}} where
-  private
-    C-Obj = Object ℂ
-    _+_   = Arrow ℂ
-
-  RepFunctor : Functor ℂ Sets
-  RepFunctor =
-    record
-      { 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
+representable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor ℂ (Sets {ℓ'})
+representable {ℂ = ℂ} A = record
   { func* = λ B → ℂ.Arrow A B
   ; func→ = λ f g → f ℂ.⊕ g
   ; ident = funExt λ _ → snd ℂ.ident
@@ -49,12 +35,12 @@ Hom0 {ℂ = ℂ} A = record
   where
     open module ℂ = Category ℂ
 
-Hom1 : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor (Opposite ℂ) (Sets {ℓ'})
-Hom1 {ℂ = ℂ} B = record
+coRepresentable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object (Opposite ℂ) → Functor (Opposite ℂ) (Sets {ℓ'})
+coRepresentable {ℂ = ℂ} B = record
   { func* = λ A → ℂ.Arrow A B
-  ; func→ = λ f g → {!!} ℂ.⊕ {!!}
-  ; ident = {!!}
-  ; distrib = {!!}
+  ; func→ = λ f g → g ℂ.⊕ f
+  ; ident = funExt λ x → fst ℂ.ident
+  ; distrib = funExt λ x → ℂ.assoc
   }
   where
     open module ℂ = Category ℂ
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index f508633..a30aee4 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -128,8 +128,8 @@ Opposite ℂ =
   where
     open module ℂ = Category ℂ
 
-Hom : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → (A B : Object ℂ) → Set ℓ'
-Hom {ℂ = ℂ} A B = Arrow ℂ A B
+Hom : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → (A B : Object ℂ) → Set ℓ'
+Hom ℂ A B = Arrow ℂ A B
 
 module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} where
   private
@@ -138,5 +138,5 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} where
     _+_ = _⊕_ ℂ
 
   HomFromArrow : (A : Obj) → {B B' : Obj} → (g : Arr B B')
-    → Hom {ℂ = ℂ} A B → Hom {ℂ = ℂ} A B'
+    → Hom ℂ A B → Hom ℂ A B'
   HomFromArrow _A g = λ f → g + f