diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 61769b3..fae77fb 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -22,6 +22,7 @@ eqpair eqa eqb i = eqa i , eqb i
 
 open Functor
 open Category
+
 module _ {ℓ ℓ' : Level} {A B : Category ℓ ℓ'} where
   lift-eq-functors : {f g : Functor A B}
     → (eq* : f .func* ≡ g .func*)
@@ -179,21 +180,24 @@ module _ {ℓ ℓ' : Level} where
 module _ {ℓ ℓ' : Level} where
   open Category
   instance
-    CatHasProducts : HasProducts (Cat ℓ ℓ')
-    CatHasProducts = record { product = product }
+    hasProducts : HasProducts (Cat ℓ ℓ')
+    hasProducts = record { product = product }
 
 -- Basically proves that `Cat ℓ ℓ` is cartesian closed.
-module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ)}} where
-  open Data.Product
-  open Category
-
+module _ (ℓ : Level) where
   private
-    Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ)
-    Catℓ = Cat ℓ ℓ
+    open Data.Product
+    open Category
     open import Cat.Categories.Fun
     open Functor
+
+    Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ)
+    Catℓ = Cat ℓ ℓ
     module _ (ℂ 𝔻 : Category ℓ ℓ) where
       private
+        _𝔻⊕_ = 𝔻 ._⊕_
+        _ℂ⊕_ = ℂ ._⊕_
+
         :obj: : Cat ℓ ℓ .Object
         :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻}
 
@@ -216,7 +220,6 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ)
           → 𝔻 .Arrow (F .func* A) (G .func* B)
         :func→: ((θ , θNat) , f) = result
           where
-            _𝔻⊕_ = 𝔻 ._⊕_
             θA : 𝔻 .Arrow (F .func* A) (G .func* A)
             θA = θ A
             θB : 𝔻 .Arrow (F .func* B) (G .func* B)
@@ -247,23 +250,22 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ)
           C = proj₂ c
 
         -- NaturalTransformation F G × ℂ .Arrow A B
-        :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙
-        :ident: = trans (proj₂ 𝔻.ident) (F .ident)
-          where
-            _𝔻⊕_ = 𝔻 ._⊕_
-            open module 𝔻 = IsCategory (𝔻 .isCategory)
-        -- Unfortunately the equational version has some ambigous arguments.
-        -- :ident: : :func→: (identityNat F , ℂ .𝟙 {o = proj₂ c}) ≡ 𝔻 .𝟙
-        -- :ident: = begin
-        --   :func→: ((:obj: ×p ℂ) .Product.obj .𝟙) ≡⟨⟩
-        --   :func→: (identityNat F , ℂ .𝟙) ≡⟨⟩
-        --   (identityTrans F C 𝔻⊕ F .func→ (ℂ .𝟙)) ≡⟨⟩
-        --   (𝔻 .𝟙 𝔻⊕ F .func→ (ℂ .𝟙)) ≡⟨ proj₂ 𝔻.ident ⟩
-        --   F .func→ (ℂ .𝟙) ≡⟨ F .ident ⟩
-        --   𝔻 .𝟙 ∎
+        -- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙
+        -- :ident: = trans (proj₂ 𝔻.ident) (F .ident)
         --   where
         --     _𝔻⊕_ = 𝔻 ._⊕_
         --     open module 𝔻 = IsCategory (𝔻 .isCategory)
+        -- Unfortunately the equational version has some ambigous arguments.
+        :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙 {o = proj₂ c}) ≡ 𝔻 .𝟙
+        :ident: = begin
+          :func→: {c} {c} ((:obj: ×p ℂ) .Product.obj .𝟙 {c}) ≡⟨⟩
+          :func→: {c} {c} (identityNat F , ℂ .𝟙)             ≡⟨⟩
+          (identityTrans F C 𝔻⊕ F .func→ (ℂ .𝟙))             ≡⟨⟩
+          𝔻 .𝟙 𝔻⊕ F .func→ (ℂ .𝟙)                            ≡⟨ proj₂ 𝔻.ident ⟩
+          F .func→ (ℂ .𝟙)                                    ≡⟨ F .ident ⟩
+          𝔻 .𝟙 ∎
+          where
+            open module 𝔻 = IsCategory (𝔻 .isCategory)
       module _ {F×A G×B H×C : Functor ℂ 𝔻 × ℂ .Object} where
         F = F×A .proj₁
         A = F×A .proj₂
@@ -271,68 +273,50 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ)
         B = G×B .proj₂
         H = H×C .proj₁
         C = H×C .proj₂
-        _𝔻⊕_ = 𝔻 ._⊕_
-        _ℂ⊕_ = ℂ ._⊕_
         -- Not entirely clear what this is at this point:
         _P⊕_ = (:obj: ×p ℂ) .Product.obj ._⊕_ {F×A} {G×B} {H×C}
         module _
           -- NaturalTransformation F G × ℂ .Arrow A B
-          {θ×α : NaturalTransformation F G × ℂ .Arrow A B}
-          {η×β : NaturalTransformation G H × ℂ .Arrow B C} where
-          θ : Transformation F G
-          θ = proj₁ (proj₁ θ×α)
-          θNat : Natural F G θ
-          θNat = proj₂ (proj₁ θ×α)
-          f : ℂ .Arrow A B
-          f = proj₂ θ×α
-          η : Transformation G H
-          η = proj₁ (proj₁ η×β)
-          ηNat : Natural G H η
-          ηNat = proj₂ (proj₁ η×β)
-          g : ℂ .Arrow B C
-          g = proj₂ η×β
-          -- :func→: ((θ , θNat) , f) = θB 𝔻⊕ F→f
-          _ : (:func→: {F×A} {G×B} θ×α) ≡ (θ B 𝔻⊕ F .func→ f)
-          _ = refl
-          ηθ : NaturalTransformation F H
-          ηθ = Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat)
-          _ : ηθ ≡ Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat)
-          _ = refl
-          ηθT = proj₁ ηθ
-          ηθN = proj₂ ηθ
-          _ : ηθT ≡ λ T → η T 𝔻⊕ θ T -- Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat)
-          _ = refl
+          {θ×f : NaturalTransformation F G × ℂ .Arrow A B}
+          {η×g : NaturalTransformation G H × ℂ .Arrow B C} where
+          private
+            θ : Transformation F G
+            θ = proj₁ (proj₁ θ×f)
+            θNat : Natural F G θ
+            θNat = proj₂ (proj₁ θ×f)
+            f : ℂ .Arrow A B
+            f = proj₂ θ×f
+            η : Transformation G H
+            η = proj₁ (proj₁ η×g)
+            ηNat : Natural G H η
+            ηNat = proj₂ (proj₁ η×g)
+            g : ℂ .Arrow B C
+            g = proj₂ η×g
+
+            ηθNT : NaturalTransformation F H
+            ηθNT = Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat)
+
+            ηθ = proj₁ ηθNT
+            ηθNat = proj₂ ηθNT
+
           :distrib: :
-              :func→: {F×A} {H×C} (η×β P⊕ θ×α)
-            ≡ (:func→: {G×B} {H×C} η×β) 𝔻⊕ (:func→: {F×A} {G×B} θ×α)
+              (η C 𝔻⊕ θ C) 𝔻⊕ F .func→ (g ℂ⊕ f)
+            ≡ (η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f)
           :distrib: = begin
-            :func→: {F×A} {H×C} (η×β P⊕ θ×α)        ≡⟨⟩
-            :func→: {F×A} {H×C} (ηθ , g ℂ⊕ f)       ≡⟨⟩
-            (ηθT C 𝔻⊕ F .func→ (g ℂ⊕ f))            ≡⟨ ηθN (g ℂ⊕ f) ⟩
-            (H .func→ (g ℂ⊕ f) 𝔻⊕ ηθT A)            ≡⟨ cong (λ φ → φ 𝔻⊕ ηθT A) (H .distrib) ⟩
-            ((H .func→ g 𝔻⊕ H .func→ f) 𝔻⊕ ηθT A)   ≡⟨ sym 𝔻.assoc ⟩
-            (H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ ηθT A))   ≡⟨⟩
-            (H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (η A 𝔻⊕ θ A))) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) 𝔻.assoc ⟩
-            (H .func→ g 𝔻⊕ ((H .func→ f 𝔻⊕ η A) 𝔻⊕ θ A)) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) (cong (λ φ → φ 𝔻⊕ θ A) (sym (ηNat f))) ⟩
-            (H .func→ g 𝔻⊕ ((η B 𝔻⊕ G .func→ f) 𝔻⊕ θ A)) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) (sym 𝔻.assoc) ⟩
-            (H .func→ g 𝔻⊕ (η B 𝔻⊕ (G .func→ f 𝔻⊕ θ A))) ≡⟨ 𝔻.assoc ⟩
-            ((H .func→ g 𝔻⊕ η B) 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) ≡⟨ cong (λ φ → φ 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) (sym (ηNat g)) ⟩
-            ((η C 𝔻⊕ G .func→ g) 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) ≡⟨ cong (λ φ → (η C 𝔻⊕ G .func→ g) 𝔻⊕ φ) (sym (θNat f)) ⟩
-            ((η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f)) ≡⟨⟩
-            ((:func→: {G×B} {H×C} η×β) 𝔻⊕ (:func→: {F×A} {G×B} θ×α)) ∎
+            (ηθ C) 𝔻⊕ F .func→ (g ℂ⊕ f)                ≡⟨ ηθNat (g ℂ⊕ f) ⟩
+            H .func→ (g ℂ⊕ f) 𝔻⊕ (ηθ A)                ≡⟨ cong (λ φ → φ 𝔻⊕ ηθ A) (H .distrib) ⟩
+            (H .func→ g 𝔻⊕ H .func→ f) 𝔻⊕ (ηθ A)       ≡⟨ sym assoc ⟩
+            H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (ηθ A))       ≡⟨⟩
+            H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (ηθ A))       ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) assoc ⟩
+            H .func→ g 𝔻⊕ ((H .func→ f 𝔻⊕ η A) 𝔻⊕ θ A) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) (cong (λ φ → φ 𝔻⊕ θ A) (sym (ηNat f))) ⟩
+            H .func→ g 𝔻⊕ ((η B 𝔻⊕ G .func→ f) 𝔻⊕ θ A) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) (sym assoc) ⟩
+            H .func→ g 𝔻⊕ (η B 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) ≡⟨ assoc ⟩
+            (H .func→ g 𝔻⊕ η B) 𝔻⊕ (G .func→ f 𝔻⊕ θ A) ≡⟨ cong (λ φ → φ 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) (sym (ηNat g)) ⟩
+            (η C 𝔻⊕ G .func→ g) 𝔻⊕ (G .func→ f 𝔻⊕ θ A) ≡⟨ cong (λ φ → (η C 𝔻⊕ G .func→ g) 𝔻⊕ φ) (sym (θNat f)) ⟩
+            (η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f) ∎
             where
-              lemθ : θ B 𝔻⊕ F .func→ f ≡ G .func→ f 𝔻⊕ θ A
-              lemθ = θNat f
-              lemη : η C 𝔻⊕ G .func→ g ≡ H .func→ g 𝔻⊕ η B
-              lemη = ηNat g
-              lemm : ηθT C 𝔻⊕ F .func→ (g ℂ⊕ f) ≡ (H .func→ (g ℂ⊕ f) 𝔻⊕ ηθT A)
-              lemm = ηθN (g ℂ⊕ f)
-              final : η B 𝔻⊕ G .func→ f ≡ H .func→ f 𝔻⊕ η A
-              final = ηNat f
-              open module 𝔻 = IsCategory (𝔻 .isCategory)
-      -- Type of `:eval:` is aka.:
-      --     Functor ((:obj: ×p ℂ) .Product.obj) 𝔻
-      -- :eval: : Cat ℓ ℓ .Arrow ((:obj: ×p ℂ) .Product.obj) 𝔻
+              open IsCategory (𝔻 .isCategory)
+
       :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻
       :eval: = record
         { func* = :func*:
@@ -342,14 +326,8 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ)
         }
 
       module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where
-        instance
-          CatℓHasProducts : HasProducts Catℓ
-          CatℓHasProducts = CatHasProducts {ℓ} {ℓ}
-        t : Catℓ .Arrow ((𝔸 ×p ℂ) .Product.obj) 𝔻 ≡ Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻
-        t = refl
-        tt : Category ℓ ℓ
-        tt = (𝔸 ×p ℂ) .Product.obj
-        open HasProducts CatℓHasProducts
+        open HasProducts (hasProducts {ℓ} {ℓ}) using (parallelProduct)
+
         postulate
           transpose : Functor 𝔸 :obj:
           eq : Catℓ ._⊕_ :eval: (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ≡ F
@@ -369,5 +347,5 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ)
         ; isExponential = :isExponential:
         }
 
-  CatHasExponentials : HasExponentials Catℓ
-  CatHasExponentials = record { exponent = :exponent: }
+  hasExponentials : HasExponentials (Cat ℓ ℓ)
+  hasExponentials = record { exponent = :exponent: }
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index cec4043..98750cf 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -1,5 +1,3 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-
 module Cat.Categories.Sets where
 
 open import Cubical.PathPrelude
@@ -25,17 +23,19 @@ module _ {ℓ : Level} where
 
   private
     module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
-      pair : (X → A × B)
-      pair x = f x , g x
-      lem : Sets ._⊕_ proj₁ pair ≡ f × Sets ._⊕_ snd pair ≡ g
+      _&&&_ : (X → A × B)
+      _&&&_ x = f x , g x
+    module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
+      _S⊕_ = Sets ._⊕_
+      lem : proj₁ S⊕ (f &&& g) ≡ f × snd S⊕ (f &&& g) ≡ g
       proj₁ lem = refl
-      snd   lem = refl
+      proj₂ lem = refl
     instance
       isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} fst snd
-      isProduct f g = pair f g , lem f g
+      isProduct f g = f &&& g , lem f g
 
     product : (A B : Sets .Object) → Product {ℂ = Sets} A B
-    product A B = record { obj = A × B ; proj₁ = fst ; proj₂ = snd ; isProduct = {!!} }
+    product A B = record { obj = A × B ; proj₁ = fst ; proj₂ = snd ; isProduct = isProduct }
 
   instance
     SetsHasProducts : HasProducts Sets
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 1d826da..9fd378a 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -141,8 +141,8 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where
     → Hom ℂ A B → Hom ℂ A B'
   HomFromArrow _A = _⊕_ ℂ
 
-module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{ℂHasProducts : HasProducts ℂ}} where
-  open HasProducts ℂHasProducts
+module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} where
+  open HasProducts hasProducts
   open Product hiding (obj)
   private
     _×p_ : (A B : ℂ .Object) → ℂ .Object
@@ -161,8 +161,8 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{ℂHasProducts : HasProducts ℂ
         {{isExponential}} : IsExponential obj eval
       -- If I make this an instance-argument then the instance resolution
       -- algorithm goes into an infinite loop. Why?
-      productsFromExp : HasProducts ℂ
-      productsFromExp = ℂHasProducts
+      exponentialsHaveProducts : HasProducts ℂ
+      exponentialsHaveProducts = hasProducts
       transpose : (A : ℂ .Object) → ℂ .Arrow (A ×p B) C → ℂ .Arrow A obj
       transpose A f = fst (isExponential A f)
 
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index 78baf35..90bc1b8 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -48,25 +48,37 @@ epi-mono-is-not-iso f =
   in {!!}
 -}
 
-  open import Cat.Categories.Cat
+module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
+  open import Cat.Category
+  open Category
+  open import Cat.Categories.Cat using (Cat)
+  module Cat = Cat.Categories.Cat
   open Exponential
-  open HasExponentials CatHasExponentials
+  private
+    Catℓ = Cat ℓ ℓ
+    CatHasExponentials : HasExponentials Catℓ
+    CatHasExponentials = Cat.hasExponentials ℓ
 
-  Exp : Set {!!}
-  Exp = Exponential (Cat {!!} {!!}) {{ℂHasProducts = {!!}}}
-    Sets (Opposite {!!})
+  -- Exp : Set (lsuc (lsuc ℓ))
+  -- Exp = Exponential (Cat (lsuc ℓ) ℓ)
+  --   Sets (Opposite ℂ)
 
-  -- _⇑_ : (A B : Catℓ .Object) → Catℓ .Object
-  -- A ⇑ B = (exponent A B) .obj
+  _⇑_ : (A B : Catℓ .Object) → Catℓ .Object
+  A ⇑ B = (exponent A B) .obj
+    where
+      open HasExponentials CatHasExponentials
 
-  -- private
-  --   :func*: : ℂ .Object → (Sets ⇑ Opposite ℂ) .Object
-  --   :func*: x = {!!}
+  private
+    -- I need `Sets` to be a `Category ℓ ℓ` but it simlpy isn't.
+    Setz : Category ℓ ℓ
+    Setz = {!Sets!}
+    :func*: : ℂ .Object → (Setz ⇑ Opposite ℂ) .Object
+    :func*: A = {!!}
 
-  -- yoneda : Functor ℂ (Sets ⇑ (Opposite ℂ))
-  -- yoneda = record
-  --   { func* = :func*:
-  --   ; func→ = {!!}
-  --   ; ident = {!!}
-  --   ; distrib = {!!}
-  --   }
+  yoneda : Functor ℂ (Setz ⇑ (Opposite ℂ))
+  yoneda = record
+    { func* = :func*:
+    ; func→ = {!!}
+    ; ident = {!!}
+    ; distrib = {!!}
+    }