From 3fcdf828d849a6c36cb7bb40e38d125a73226231 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 21:29:15 +0100
Subject: [PATCH] Implement exponentials

---
 src/Cat/Category.agda            |  7 ++++++
 src/Cat/Category/Properties.agda | 37 ++++++++++++++++++++++----------
 2 files changed, 33 insertions(+), 11 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 91e25f3..1c8c12f 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -88,6 +88,13 @@ record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : ℂ .Object)
     proj₁ : ℂ .Arrow obj A
     proj₂ : ℂ .Arrow obj B
     {{isProduct}} : IsProduct ℂ proj₁ proj₂
+  arrowProduct : ∀ {X} → (π₁ : Arrow ℂ X A) (π₂ : Arrow ℂ X B)
+    → Arrow ℂ X obj
+  arrowProduct π₁ π₂ = fst (isProduct π₁ π₂)
+
+record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
+  field
+    product : ∀ (A B : ℂ .Object) → Product {ℂ = ℂ} A B
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   Opposite : Category ℓ ℓ'
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index 4ff4376..9d3293e 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -49,17 +49,32 @@ epi-mono-is-not-iso f =
 -}
 
 
-module _ {ℓa ℓa' ℓb ℓb'} where
-  Exponential : Category ℓa ℓa' → Category ℓb ℓb' → Category {!!} {!!}
-  Exponential A B = record
-    { Object = {!!}
-    ; Arrow = {!!}
-    ; 𝟙 = {!!}
-    ; _⊕_ = {!!}
-    ; isCategory = {!!}
-    }
+module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} (B C : ℂ .Category.Object) where
+  open Category
+  open HasProducts hasProducts
+  open Product
+  prod-obj : (A B : ℂ .Object) → ℂ .Object
+  prod-obj A B = Product.obj (product A B)
+  -- The product mentioned in awodey in Def 6.1 is not the regular product of arrows.
+  -- It's a "parallel" product
+  ×A : {A A' B B' : ℂ .Object} → ℂ .Arrow A A' → ℂ .Arrow B B'
+    → ℂ .Arrow (prod-obj A B) (prod-obj A' B')
+  ×A {A = A} {A' = A'} {B = B} {B' = B'} a b = arrowProduct (product A' B')
+    (ℂ ._⊕_ a ((product A B) .proj₁))
+    (ℂ ._⊕_ b ((product A B) .proj₂))
+
+  IsExponential : {Cᴮ : ℂ .Object} → ℂ .Arrow (prod-obj Cᴮ B) C → Set (ℓ ⊔ ℓ')
+  IsExponential eval = ∀ (A : ℂ .Object) (f : ℂ .Arrow (prod-obj A B) C)
+    → ∃![ f~ ] (ℂ ._⊕_ eval (×A f~ (ℂ .𝟙)) ≡ f)
+
+  record Exponential : Set (ℓ ⊔ ℓ') where
+    field
+      -- obj ≡ Cᴮ
+      obj : ℂ .Object
+      eval : ℂ .Arrow ( prod-obj obj B ) C
+      {{isExponential}} : IsExponential eval
 
 _⇑_ = Exponential
 
-yoneda : ∀ {ℓ ℓ'} → {ℂ : Category ℓ ℓ'} → Functor ℂ (Sets ⇑ (Opposite ℂ))
-yoneda = {!!}
+-- yoneda : ∀ {ℓ ℓ'} → {ℂ : Category ℓ ℓ'} → Functor ℂ (Sets ⇑ (Opposite ℂ))
+-- yoneda = {!!}