diff --git a/CHANGELOG.md b/CHANGELOG.md
index cc79e6c..56020da 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,23 @@
 Changelog
 =========
 
+Version 1.2.0
+-------------
+This version is mainly a huge refactor.
+
+I've renamed
+
+* `distrib` to `isDistributive`
+* `arrowIsSet` to `arrowsAreSets`
+* `ident` to `isIdentity`
+* `assoc` to `isAssociative`
+
+And added "type-synonyms" for all of these. Their names should now match their
+type. So e.g. `isDistributive` has type `IsDistributive`.
+
+I've also changed how names are exported in `Functor` to be in line with
+`Category`.
+
 Version 1.1.0
 -------------
 In this version categories have been refactored - there's now a notion of a raw
diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 1ec9acb..b7e306e 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -16,107 +16,58 @@ open import Cat.Category.Exponential
 open import Cat.Equality
 open Equality.Data.Product
 
-open Functor
-open IsFunctor
-open Category hiding (_∘_)
+open Functor using (func→ ; func*)
+open Category using (Object ; 𝟙)
 
 -- The category of categories
 module _ (ℓ ℓ' : Level) where
   private
     module _ {𝔸 𝔹 ℂ 𝔻 : Category ℓ ℓ'} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻} where
-      private
-        eq* : func* (H ∘f (G ∘f F)) ≡ func* ((H ∘f G) ∘f F)
-        eq* = refl
-        eq→ : PathP
-          (λ i → {A B : Object 𝔸} → 𝔸 [ A , B ] → 𝔻 [ eq* i A , eq* i B ])
-          (func→ (H ∘f (G ∘f F))) (func→ ((H ∘f G) ∘f F))
-        eq→ = refl
-        postulate
-          eqI
-            : (λ i → ∀ {A : Object 𝔸} → eq→ i (𝟙 𝔸 {A}) ≡ 𝟙 𝔻 {eq* i A})
-            [ (H ∘f (G ∘f F)) .isFunctor .ident
-            ≡ ((H ∘f G) ∘f F) .isFunctor .ident
-            ]
-          eqD
-            : (λ i → ∀ {A B C} {f : 𝔸 [ A , B ]} {g : 𝔸 [ B , C ]}
-              → eq→ i (𝔸 [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
-            [ (H ∘f (G ∘f F)) .isFunctor .distrib
-            ≡ ((H ∘f G) ∘f F) .isFunctor .distrib
-            ]
-
       assc : H ∘f (G ∘f F) ≡ (H ∘f G) ∘f F
-      assc = Functor≡ eq* eq→ (IsFunctor≡ eqI eqD)
+      assc = Functor≡ refl refl
 
     module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where
-      module _ where
-        private
-          eq* : (func* F) ∘ (func* (identity {C = ℂ})) ≡ func* F
-          eq* = refl
-          -- lemmm : func→ {C = A} {D = B} (f ∘f identity) ≡ func→ f
-          eq→ : PathP
-            (λ i →
-            {x y : Object ℂ} → Arrow ℂ x y → Arrow 𝔻 (func* F x) (func* F y))
-            (func→ (F ∘f identity)) (func→ F)
-          eq→ = refl
-          postulate
-            eqI-r
-              : (λ i → {c : Object ℂ} → (λ _ → 𝔻 [ func* F c , func* F c ])
-                [ func→ F (𝟙 ℂ) ≡ 𝟙 𝔻 ])
-              [(F ∘f identity) .isFunctor .ident ≡ F .isFunctor .ident ]
-            eqD-r : PathP
-                        (λ i →
-                        {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} →
-                        eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
-                        ((F ∘f identity) .isFunctor .distrib) (F .isFunctor .distrib)
-        ident-r : F ∘f identity ≡ F
-        ident-r = Functor≡ eq* eq→ (IsFunctor≡ eqI-r eqD-r)
-      module _ where
-        private
-          postulate
-            eq* : (identity ∘f F) .func* ≡ F .func*
-            eq→ : PathP
-              (λ i → {x y : Object ℂ} → ℂ [ x , y ] → 𝔻 [ eq* i x , eq* i y ])
-              ((identity ∘f F) .func→) (F .func→)
-            eqI : (λ i → ∀ {A : Object ℂ} → eq→ i (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {eq* i A})
-                  [ ((identity ∘f F) .isFunctor .ident) ≡ (F .isFunctor .ident) ]
-            eqD : PathP (λ i → {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
-                 → eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
-                 ((identity ∘f F) .isFunctor .distrib) (F .isFunctor .distrib)
-                 -- (λ z → eq* i z) (eq→ i)
-        ident-l : identity ∘f F ≡ F
-        ident-l = Functor≡ eq* eq→ λ i → record { ident = eqI i ; distrib = eqD i }
+      ident-r : F ∘f identity ≡ F
+      ident-r = Functor≡ refl refl
 
-    RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
-    RawCat =
-      record
-        { Object = Category ℓ ℓ'
-        ; Arrow = Functor
-        ; 𝟙 = identity
-        ; _∘_ = _∘f_
-        -- What gives here? Why can I not name the variables directly?
-        -- ; isCategory = record
-        --   { assoc = λ {_ _ _ _ F G H} → assc {F = F} {G = G} {H = H}
-        --   ; ident = ident-r , ident-l
-        --   }
-        }
-    open IsCategory
-    instance
-      :isCategory: : IsCategory RawCat
-      assoc :isCategory: {f = F} {G} {H} = assc {F = F} {G = G} {H = H}
-      ident :isCategory: = ident-r , ident-l
-      arrow-is-set :isCategory: = {!!}
-      univalent :isCategory: = {!!}
+      ident-l : identity ∘f F ≡ F
+      ident-l = Functor≡ refl refl
 
-  Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
-  raw Cat = RawCat
+  RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
+  RawCat =
+    record
+      { Object = Category ℓ ℓ'
+      ; Arrow = Functor
+      ; 𝟙 = identity
+      ; _∘_ = _∘f_
+      }
+  private
+    open RawCategory RawCat
+    isAssociative : IsAssociative
+    isAssociative {f = F} {G} {H} = assc {F = F} {G = G} {H = H}
+    -- TODO: Rename `ident'` to `ident` after changing how names are exposed in Functor.
+    ident' : IsIdentity identity
+    ident' = ident-r , ident-l
+    -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors,
+    -- however, form a groupoid! Therefore there is no (1-)category of
+    -- categories. There does, however, exist a 2-category of 1-categories.
 
-module _ {ℓ ℓ' : Level} where
+  -- Because of the note above there is not category of categories.
+  Cat : (unprovable : IsCategory RawCat) → Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
+  Category.raw        (Cat _) = RawCat
+  Category.isCategory (Cat unprovable) = unprovable
+  -- Category.raw Cat _ = RawCat
+  -- Category.isCategory Cat unprovable = unprovable
+
+-- The following to some extend depends on the category of categories being a
+-- category. In some places it may not actually be needed, however.
+module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
   module _ (ℂ 𝔻 : Category ℓ ℓ') where
     private
-      Catt = Cat ℓ ℓ'
+      Catt = Cat ℓ ℓ' unprovable
       :Object: = Object ℂ × Object 𝔻
       :Arrow:  : :Object: → :Object: → Set ℓ'
-      :Arrow: (c , d) (c' , d') = Arrow ℂ c c' × Arrow 𝔻 d d'
+      :Arrow: (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ]
       :𝟙: : {o : :Object:} → :Arrow: o o
       :𝟙: = 𝟙 ℂ , 𝟙 𝔻
       _:⊕:_ :
@@ -131,70 +82,67 @@ module _ {ℓ ℓ' : Level} where
       RawCategory.Arrow :rawProduct: = :Arrow:
       RawCategory.𝟙 :rawProduct: = :𝟙:
       RawCategory._∘_ :rawProduct: = _:⊕:_
+      open RawCategory :rawProduct:
 
-      module C = IsCategory (ℂ .isCategory)
-      module D = IsCategory (𝔻 .isCategory)
-      postulate
-        issSet : {A B : RawCategory.Object :rawProduct:} → isSet (RawCategory.Arrow :rawProduct: A B)
+      module C = Category ℂ
+      module D = Category 𝔻
+      open import Cubical.Sigma
+      issSet : {A B : RawCategory.Object :rawProduct:} → isSet (Arrow A B)
+      issSet = setSig {sA = C.arrowsAreSets} {sB = λ x → D.arrowsAreSets}
+      ident' : IsIdentity :𝟙:
+      ident'
+        = Σ≡ (fst C.isIdentity) (fst D.isIdentity)
+        , Σ≡ (snd C.isIdentity) (snd D.isIdentity)
+      postulate univalent : Univalence.Univalent :rawProduct: ident'
       instance
         :isCategory: : IsCategory :rawProduct:
-        -- :isCategory: = record
-        --   { assoc = Σ≡ C.assoc D.assoc
-        --   ; ident
-        --     = Σ≡ (fst C.ident) (fst D.ident)
-        --     , Σ≡ (snd C.ident) (snd D.ident)
-        --   ; arrow-is-set = issSet
-        --   ; univalent = {!!}
-        --   }
-        IsCategory.assoc :isCategory: = Σ≡ C.assoc D.assoc
-        IsCategory.ident :isCategory:
-          = Σ≡ (fst C.ident) (fst D.ident)
-          , Σ≡ (snd C.ident) (snd D.ident)
-        IsCategory.arrow-is-set :isCategory: = issSet
-        IsCategory.univalent :isCategory: = {!!}
+        IsCategory.isAssociative :isCategory: = Σ≡ C.isAssociative D.isAssociative
+        IsCategory.isIdentity :isCategory: = ident'
+        IsCategory.arrowsAreSets :isCategory: = issSet
+        IsCategory.univalent :isCategory: = univalent
 
       :product: : Category ℓ ℓ'
-      raw :product: = :rawProduct:
+      Category.raw :product: = :rawProduct:
 
       proj₁ : Catt [ :product: , ℂ ]
-      proj₁ = record { func* = fst ; func→ = fst ; isFunctor = record { ident = refl ; distrib = refl } }
+      proj₁ = record
+        { raw = record { func* = fst ; func→ = fst }
+        ; isFunctor = record { isIdentity = refl ; isDistributive = refl }
+        }
 
       proj₂ : Catt [ :product: , 𝔻 ]
-      proj₂ = record { func* = snd ; func→ = snd ; isFunctor = record { ident = refl ; distrib = refl } }
+      proj₂ = record
+        { raw = record { func* = snd ; func→ = snd }
+        ; isFunctor = record { isIdentity = refl ; isDistributive = refl }
+        }
 
       module _ {X : Object Catt} (x₁ : Catt [ X , ℂ ]) (x₂ : Catt [ X , 𝔻 ]) where
-        open Functor
+        x : Functor X :product:
+        x = record
+          { raw = record
+            { func* = λ x → x₁ .func* x , x₂ .func* x
+            ; func→ = λ x → func→ x₁ x , func→ x₂ x
+            }
+          ; isFunctor = record
+            { isIdentity   = Σ≡ x₁.isIdentity x₂.isIdentity
+            ; isDistributive = Σ≡ x₁.isDistributive x₂.isDistributive
+            }
+          }
+          where
+            open module x₁ = Functor x₁
+            open module x₂ = Functor x₂
 
-        postulate x : Functor X :product:
-        -- x = record
-        --   { func* = λ x → x₁ .func* x , x₂ .func* x
-        --   ; func→ = λ x → func→ x₁ x , func→ x₂ x
-        --   ; isFunctor = record
-        --     { ident   = Σ≡ x₁.ident x₂.ident
-        --     ; distrib = Σ≡ x₁.distrib x₂.distrib
-        --     }
-        --   }
-        --   where
-        --     open module x₁ = IsFunctor (x₁ .isFunctor)
-        --     open module x₂ = IsFunctor (x₂ .isFunctor)
+        isUniqL : Catt [ proj₁ ∘ x ] ≡ x₁
+        isUniqL = Functor≡ eq* eq→
+          where
+            eq* : (Catt [ proj₁ ∘ x ]) .func* ≡ x₁ .func*
+            eq* = refl
+            eq→ : (λ i → {A : Object X} {B : Object X} → X [ A , B ] → ℂ [ eq* i A , eq* i B ])
+                    [ (Catt [ proj₁ ∘ x ]) .func→ ≡ x₁ .func→ ]
+            eq→ = refl
 
-        -- Turned into postulate after:
-        -- > commit e8215b2c051062c6301abc9b3f6ec67106259758 (HEAD -> dev, github/dev)
-        -- > Author: Frederik Hanghøj Iversen <fhi.1990@gmail.com>
-        -- > Date:   Mon Feb 5 14:59:53 2018 +0100
-        postulate isUniqL : Catt [ proj₁ ∘ x ] ≡ x₁
-        -- isUniqL = Functor≡ eq* eq→ {!!}
-        --   where
-        --     eq* : (Catt [ proj₁ ∘ x ]) .func* ≡ x₁ .func*
-        --     eq* = {!refl!}
-        --     eq→ : (λ i → {A : Object X} {B : Object X} → X [ A , B ] → ℂ [ eq* i A , eq* i B ])
-        --             [ (Catt [ proj₁ ∘ x ]) .func→ ≡ x₁ .func→ ]
-        --     eq→ = refl
-            -- postulate eqIsF : (Catt [ proj₁ ∘ x ]) .isFunctor ≡ x₁ .isFunctor
-            -- eqIsF = IsFunctor≡ {!refl!} {!!}
-
-        postulate isUniqR : Catt [ proj₂ ∘ x ] ≡ x₂
-        -- isUniqR = Functor≡ refl refl {!!} {!!}
+        isUniqR : Catt [ proj₂ ∘ x ] ≡ x₂
+        isUniqR = Functor≡ refl refl
 
         isUniq : Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂
         isUniq = isUniqL , isUniqR
@@ -203,36 +151,37 @@ module _ {ℓ ℓ' : Level} where
         uniq = x , isUniq
 
     instance
-      isProduct : IsProduct (Cat ℓ ℓ') proj₁ proj₂
+      isProduct : IsProduct Catt proj₁ proj₂
       isProduct = uniq
 
-    product : Product {ℂ = (Cat ℓ ℓ')} ℂ 𝔻
+    product : Product {ℂ = Catt} ℂ 𝔻
     product = record
       { obj = :product:
       ; proj₁ = proj₁
       ; proj₂ = proj₂
       }
 
-module _ {ℓ ℓ' : Level} where
+module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
+  Catt = Cat ℓ ℓ' unprovable
   instance
-    hasProducts : HasProducts (Cat ℓ ℓ')
-    hasProducts = record { product = product }
+    hasProducts : HasProducts Catt
+    hasProducts = record { product = product unprovable }
 
 -- Basically proves that `Cat ℓ ℓ` is cartesian closed.
-module _ (ℓ : Level) where
+module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
   private
     open Data.Product
     open import Cat.Categories.Fun
 
     Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ)
-    Catℓ = Cat ℓ ℓ
+    Catℓ = Cat ℓ ℓ unprovable
     module _ (ℂ 𝔻 : Category ℓ ℓ) where
       private
-        :obj: : Object (Cat ℓ ℓ)
+        :obj: : Object Catℓ
         :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻}
 
         :func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻
-        :func*: (F , A) = F .func* A
+        :func*: (F , A) = func* F A
 
       module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where
         private
@@ -247,30 +196,30 @@ module _ (ℓ : Level) where
           B = proj₂ cod
 
         :func→: : (pobj : NaturalTransformation F G × ℂ [ A , B ])
-          → 𝔻 [ F .func* A , G .func* B ]
+          → 𝔻 [ func* F A , func* G B ]
         :func→: ((θ , θNat) , f) = result
           where
-            θA : 𝔻 [ F .func* A , G .func* A ]
+            θA : 𝔻 [ func* F A , func* G A ]
             θA = θ A
-            θB : 𝔻 [ F .func* B , G .func* B ]
+            θB : 𝔻 [ func* F B , func* G B ]
             θB = θ B
-            F→f : 𝔻 [ F .func* A , F .func* B ]
-            F→f = F .func→ f
-            G→f : 𝔻 [ G .func* A , G .func* B ]
-            G→f = G .func→ f
-            l : 𝔻 [ F .func* A , G .func* B ]
+            F→f : 𝔻 [ func* F A , func* F B ]
+            F→f = func→ F f
+            G→f : 𝔻 [ func* G A , func* G B ]
+            G→f = func→ G f
+            l : 𝔻 [ func* F A , func* G B ]
             l = 𝔻 [ θB ∘ F→f ]
-            r : 𝔻 [ F .func* A , G .func* B ]
+            r : 𝔻 [ func* F A , func* G B ]
             r = 𝔻 [ G→f ∘ θA ]
             -- There are two choices at this point,
             -- but I suppose the whole point is that
             -- by `θNat f` we have `l ≡ r`
             --     lem : 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
             --     lem = θNat f
-            result : 𝔻 [ F .func* A , G .func* B ]
+            result : 𝔻 [ func* F A , func* G B ]
             result = l
 
-      _×p_ = product
+      _×p_ = product unprovable
 
       module _ {c : Functor ℂ 𝔻 × Object ℂ} where
         private
@@ -281,21 +230,21 @@ module _ (ℓ : Level) where
 
         -- NaturalTransformation F G × ℂ .Arrow A B
         -- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙
-        -- :ident: = trans (proj₂ 𝔻.ident) (F .ident)
+        -- :ident: = trans (proj₂ 𝔻.isIdentity) (F .isIdentity)
         --   where
         --     open module 𝔻 = IsCategory (𝔻 .isCategory)
         -- Unfortunately the equational version has some ambigous arguments.
-        :ident: : :func→: {c} {c} (identityNat F , 𝟙 ℂ {o = proj₂ c}) ≡ 𝟙 𝔻
+        :ident: : :func→: {c} {c} (identityNat F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻
         :ident: = begin
           :func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩
           :func→: {c} {c} (identityNat F , 𝟙 ℂ)             ≡⟨⟩
-          𝔻 [ identityTrans F C ∘ F .func→ (𝟙 ℂ)]           ≡⟨⟩
-          𝔻 [ 𝟙 𝔻 ∘ F .func→ (𝟙 ℂ)]                        ≡⟨ proj₂ 𝔻.ident ⟩
-          F .func→ (𝟙 ℂ)                                    ≡⟨ F.ident ⟩
+          𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)]           ≡⟨⟩
+          𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)]                        ≡⟨ proj₂ 𝔻.isIdentity ⟩
+          func→ F (𝟙 ℂ)                                    ≡⟨ F.isIdentity ⟩
           𝟙 𝔻                                               ∎
           where
-            open module 𝔻 = IsCategory (𝔻 .isCategory)
-            open module F = IsFunctor (F .isFunctor)
+            open module 𝔻 = Category 𝔻
+            open module F = Functor F
 
       module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where
         F = F×A .proj₁
@@ -330,48 +279,51 @@ module _ (ℓ : Level) where
             ηθ = proj₁ ηθNT
             ηθNat = proj₂ ηθNT
 
-          :distrib: :
-              𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F .func→ ( ℂ [ g ∘ f ] ) ]
-            ≡ 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ θ B ∘ F .func→ f ] ]
-          :distrib: = begin
-            𝔻 [ (ηθ C) ∘ F .func→ (ℂ [ g ∘ f ]) ]
+          :isDistributive: :
+              𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ]
+            ≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ]
+          :isDistributive: = begin
+            𝔻 [ (ηθ C) ∘ func→ F (ℂ [ 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 ] ]
-              ≡⟨ 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→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ]
+              ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.isDistributive) ⟩
+            𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ]
+              ≡⟨ sym isAssociative ⟩
+            𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) isAssociative ⟩
+            𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ func→ H f ∘ η A ] ∘ θ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩
+            𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ η B ∘ func→ G f ] ∘ θ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (sym isAssociative) ⟩
+            𝔻 [ func→ H g ∘ 𝔻 [ η B ∘ 𝔻 [ func→ G f ∘ θ A ] ] ]
+              ≡⟨ isAssociative ⟩
+            𝔻 [ 𝔻 [ func→ H g ∘ η B ] ∘ 𝔻 [ func→ G f ∘ θ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ func→ G f ∘ θ A ] ]) (sym (ηNat g)) ⟩
+            𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ func→ G f ∘ θ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ φ ]) (sym (θNat f)) ⟩
+            𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ∎
             where
-              open IsCategory (𝔻 .isCategory)
-              open module H = IsFunctor (H .isFunctor)
+              open Category 𝔻
+              module H = Functor H
 
       :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻
       :eval: = record
-        { func* = :func*:
-        ; func→ = λ {dom} {cod} → :func→: {dom} {cod}
+        { raw = record
+          { func* = :func*:
+          ; func→ = λ {dom} {cod} → :func→: {dom} {cod}
+          }
         ; isFunctor = record
-          { ident = λ {o} → :ident: {o}
-          ; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y}
+          { isIdentity = λ {o} → :ident: {o}
+          ; isDistributive = λ {f u n k y} → :isDistributive: {f} {u} {n} {k} {y}
           }
         }
 
       module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where
-        open HasProducts (hasProducts {ℓ} {ℓ}) renaming (_|×|_ to parallelProduct)
+        open HasProducts (hasProducts {ℓ} {ℓ} unprovable) renaming (_|×|_ to parallelProduct)
 
         postulate
           transpose : Functor 𝔸 :obj:
-          eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F
+          eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {A = ℂ})) ] ≡ F
           -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F
           -- eq' : (Catℓ [ :eval: ∘
           --   (record { product = product } HasProducts.|×| transpose)
@@ -384,10 +336,11 @@ module _ (ℓ : Level) where
         -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose =
         -- transpose , eq
 
-      :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
-      :isExponential: = {!catTranspose!}
-        where
-          open HasProducts (hasProducts {ℓ} {ℓ}) using (_|×|_)
+      postulate :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
+      -- :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
+      -- :isExponential: = {!catTranspose!}
+      --   where
+      --     open HasProducts (hasProducts {ℓ} {ℓ} unprovable) using (_|×|_)
       -- :isExponential: = λ 𝔸 F → transpose 𝔸 F , eq' 𝔸 F
 
       -- :exponent: : Exponential (Cat ℓ ℓ) A B
@@ -398,5 +351,5 @@ module _ (ℓ : Level) where
         ; isExponential = :isExponential:
         }
 
-  hasExponentials : HasExponentials (Cat ℓ ℓ)
+  hasExponentials : HasExponentials Catℓ
   hasExponentials = record { exponent = :exponent: }
diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda
index 83f19b0..6150dd2 100644
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@@ -25,12 +25,12 @@ module _ (ℓa ℓb : Level) where
     c ⟨ g ∘ f ⟩ = _∘_ {c = c} g f
 
     module _ {A B C D : Obj'} {f : Arr A B} {g : Arr B C} {h : Arr C D} where
-      assoc : (D ⟨ h ∘ C ⟨ g ∘ f ⟩ ⟩) ≡ D ⟨ D ⟨ h ∘ g ⟩ ∘ f ⟩
-      assoc = Σ≡ refl refl
+      isAssociative : (D ⟨ h ∘ C ⟨ g ∘ f ⟩ ⟩) ≡ D ⟨ D ⟨ h ∘ g ⟩ ∘ f ⟩
+      isAssociative = Σ≡ refl refl
 
     module _ {A B : Obj'} {f : Arr A B} where
-      ident : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f
-      ident = (Σ≡ refl refl) , Σ≡ refl refl
+      isIdentity : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f
+      isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
 
 
     RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
@@ -44,9 +44,9 @@ module _ (ℓa ℓb : Level) where
     instance
       isCategory : IsCategory RawFam
       isCategory = record
-        { assoc = λ {A} {B} {C} {D} {f} {g} {h} → assoc {D = D} {f} {g} {h}
-        ; ident = λ {A} {B} {f} → ident {A} {B} {f = f}
-        ; arrowIsSet = {!!}
+        { isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {D = D} {f} {g} {h}
+        ; isIdentity = λ {A} {B} {f} → isIdentity {A} {B} {f = f}
+        ; arrowsAreSets = {!!}
         ; univalent = {!!}
         }
 
diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda
index 326152a..5441abc 100644
--- a/src/Cat/Categories/Free.agda
+++ b/src/Cat/Categories/Free.agda
@@ -9,14 +9,6 @@ open import Cat.Category
 
 open IsCategory
 
--- data Path {ℓ : Level} {A : Set ℓ} : (a b : A) → Set ℓ where
---   emptyPath : {a : A} → Path a a
---   concatenate : {a b c : A} → Path a b → Path b c → Path a b
-
--- import Data.List
--- P : (a b : Object ℂ) → Set (ℓ ⊔ ℓ')
--- P = {!Data.List.List ?!}
--- Generalized paths:
 data Path {ℓ ℓ' : Level} {A : Set ℓ} (R : A → A → Set ℓ') : (a b : A) → Set (ℓ ⊔ ℓ') where
   empty : {a : A} → Path R a a
   cons : {a b c : A} → R b c → Path R a b → Path R a c
@@ -34,16 +26,16 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   open Category ℂ
 
   private
-    p-assoc : {A B C D : Object} {r : Path Arrow A B} {q : Path Arrow B C} {p : Path Arrow C D}
+    p-isAssociative : {A B C D : Object} {r : Path Arrow A B} {q : Path Arrow B C} {p : Path Arrow C D}
       → p ++ (q ++ r) ≡ (p ++ q) ++ r
-    p-assoc {r = r} {q} {empty} = refl
-    p-assoc {A} {B} {C} {D} {r = r} {q} {cons x p} = begin
+    p-isAssociative {r = r} {q} {empty} = refl
+    p-isAssociative {A} {B} {C} {D} {r = r} {q} {cons x p} = begin
       cons x p ++ (q ++ r)   ≡⟨ cong (cons x) lem ⟩
       cons x ((p ++ q) ++ r) ≡⟨⟩
       (cons x p ++ q) ++ r ∎
       where
         lem : p ++ (q ++ r) ≡ ((p ++ q) ++ r)
-        lem = p-assoc {r = r} {q} {p}
+        lem = p-isAssociative {r = r} {q} {p}
 
     ident-r : ∀ {A} {B} {p : Path Arrow A B} → concatenate p empty ≡ p
     ident-r {p = empty} = refl
@@ -65,8 +57,8 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
     }
   RawIsCategoryFree : IsCategory RawFree
   RawIsCategoryFree = record
-    { assoc = λ { {f = f} {g} {h} → p-assoc {r = f} {g} {h}}
-    ; ident = ident-r , ident-l
-    ; arrowIsSet = {!!}
+    { isAssociative = λ { {f = f} {g} {h} → p-isAssociative {r = f} {g} {h}}
+    ; isIdentity = ident-r , ident-l
+    ; arrowsAreSets = {!!}
     ; univalent = {!!}
     }
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index ba492d0..3e4dcbf 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -38,9 +38,6 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       → (f : ℂ [ A , B ])
       → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
 
-    -- naturalIsProp : ∀ θ → isProp (Natural θ)
-    -- naturalIsProp θ x y = {!funExt!}
-
     NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
     NaturalTransformation = Σ Transformation Natural
 
@@ -63,8 +60,8 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
   identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
   identityNatural F {A = A} {B = B} f = begin
     𝔻 [ identityTrans F B ∘ F→ f ]  ≡⟨⟩
-    𝔻 [ 𝟙 𝔻 ∘  F→ f ]              ≡⟨ proj₂ 𝔻.ident ⟩
-    F→ f                            ≡⟨ sym (proj₁ 𝔻.ident) ⟩
+    𝔻 [ 𝟙 𝔻 ∘  F→ f ]              ≡⟨ proj₂ 𝔻.isIdentity ⟩
+    F→ f                            ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩
     𝔻 [ F→ f ∘ 𝟙 𝔻 ]               ≡⟨⟩
     𝔻 [ F→ f ∘ identityTrans F A ]  ∎
     where
@@ -87,11 +84,11 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η
     proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin
       𝔻 [ (θ ∘nt η) B ∘ F.func→ f ]     ≡⟨⟩
-      𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.func→ f ] ≡⟨ sym assoc ⟩
+      𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.func→ f ] ≡⟨ sym isAssociative ⟩
       𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
-      𝔻 [ θ B ∘ 𝔻 [ G.func→ f ∘ η A ] ] ≡⟨ assoc ⟩
+      𝔻 [ θ B ∘ 𝔻 [ G.func→ f ∘ η A ] ] ≡⟨ isAssociative ⟩
       𝔻 [ 𝔻 [ θ B ∘ G.func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
-      𝔻 [ 𝔻 [ H.func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym assoc ⟩
+      𝔻 [ 𝔻 [ H.func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym isAssociative ⟩
       𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
       𝔻 [ H.func→ f ∘ (θ ∘nt η) A ]     ∎
       where
@@ -100,59 +97,56 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     NatComp = _:⊕:_
 
   private
-    module _ {F G : Functor ℂ 𝔻} where
-      module 𝔻 = Category 𝔻
+    module 𝔻 = Category 𝔻
 
-      transformationIsSet : isSet (Transformation F G)
-      transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C)   (λ l → q l C) i j
-      IsSet'   : {ℓ : Level} (A : Set ℓ) → Set ℓ
-      IsSet' A = {x y : A} → (p q : (λ _ → A) [ x ≡ y ]) → p ≡ q
+  module _ {F G : Functor ℂ 𝔻} where
+    transformationIsSet : isSet (Transformation F G)
+    transformationIsSet _ _ p q i j C = 𝔻.arrowsAreSets _ _ (λ l → p l C)   (λ l → q l C) i j
 
-      naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
-      naturalIsProp θ θNat θNat' = lem
-        where
-          lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
-          lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i
+    naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
+    naturalIsProp θ θNat θNat' = lem
+      where
+        lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
+        lem = λ i f → 𝔻.arrowsAreSets _ _ (θNat f) (θNat' f) i
 
-      naturalTransformationIsSets : isSet (NaturalTransformation F G)
-      naturalTransformationIsSets = sigPresSet transformationIsSet
-        λ θ → ntypeCommulative
-          (s≤s {n = Nat.suc Nat.zero} z≤n)
-          (naturalIsProp θ)
+    naturalTransformationIsSets : isSet (NaturalTransformation F G)
+    naturalTransformationIsSets = sigPresSet transformationIsSet
+      λ θ → ntypeCommulative
+        (s≤s {n = Nat.suc Nat.zero} z≤n)
+        (naturalIsProp θ)
 
-    module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B}
-      {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
-      private
-        θ = proj₁ θ'
-        η = proj₁ η'
-        ζ = proj₁ ζ'
-        θNat = proj₂ θ'
-        ηNat = proj₂ η'
-        ζNat = proj₂ ζ'
-        L : NaturalTransformation A D
-        L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ'))
-        R : NaturalTransformation A D
-        R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
-      _g⊕f_ = _:⊕:_ {A} {B} {C}
-      _h⊕g_ = _:⊕:_ {B} {C} {D}
-      :assoc: : L ≡ R
-      :assoc: = lemSig (naturalIsProp {F = A} {D})
-        L R (funExt (λ x → assoc))
-        where
-          open Category 𝔻
+  module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B}
+    {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
+    private
+      θ = proj₁ θ'
+      η = proj₁ η'
+      ζ = proj₁ ζ'
+      θNat = proj₂ θ'
+      ηNat = proj₂ η'
+      ζNat = proj₂ ζ'
+      L : NaturalTransformation A D
+      L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ'))
+      R : NaturalTransformation A D
+      R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
+    _g⊕f_ = _:⊕:_ {A} {B} {C}
+    _h⊕g_ = _:⊕:_ {B} {C} {D}
+    :isAssociative: : L ≡ R
+    :isAssociative: = lemSig (naturalIsProp {F = A} {D})
+      L R (funExt (λ x → isAssociative))
+      where
+        open Category 𝔻
 
+  private
     module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
-      private
-        allNatural = naturalIsProp {F = A} {B}
-        f' = proj₁ f
-        module 𝔻Data = Category 𝔻
-        eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C
-        eq-r C = begin
-          𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩
-          𝔻 [ f' C ∘ 𝔻Data.𝟙 ]  ≡⟨ proj₁ (𝔻.ident {A} {B}) ⟩
-          f' C ∎
-        eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
-        eq-l C = proj₂ (𝔻.ident {A} {B})
+      allNatural = naturalIsProp {F = A} {B}
+      f' = proj₁ f
+      eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C
+      eq-r C = begin
+        𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩
+        𝔻 [ f' C ∘ 𝔻.𝟙 ]  ≡⟨ proj₁ 𝔻.isIdentity ⟩
+        f' C ∎
+      eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
+      eq-l C = proj₂ 𝔻.isIdentity
       ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
       ident-r = lemSig allNatural _ _ (funExt eq-r)
       ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
@@ -174,9 +168,9 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
   instance
     :isCategory: : IsCategory RawFun
     :isCategory: = record
-      { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D}
-      ; ident = λ {A B} → :ident: {A} {B}
-      ; arrowIsSet = λ {F} {G} → naturalTransformationIsSets {F} {G}
+      { isAssociative = λ {A B C D} → :isAssociative: {A} {B} {C} {D}
+      ; isIdentity = λ {A B} → :ident: {A} {B}
+      ; arrowsAreSets = λ {F} {G} → naturalTransformationIsSets {F} {G}
       ; univalent = {!!}
       }
 
diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index 8a93274..de3d1f2 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -149,10 +149,10 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset
       ≃ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
     equi = fwd Cubical.FromStdLib., isequiv
 
-    -- assocc : Q + (R + S) ≡ (Q + R) + S
-  is-assoc : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)
+    -- isAssociativec : Q + (R + S) ≡ (Q + R) + S
+  is-isAssociative : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)
          ≡ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
-  is-assoc = equivToPath equi
+  is-isAssociative = equivToPath equi
 
 RawRel : RawCategory (lsuc lzero) (lsuc lzero)
 RawRel = record
@@ -164,8 +164,8 @@ RawRel = record
 
 RawIsCategoryRel : IsCategory RawRel
 RawIsCategoryRel = record
-  { assoc = funExt is-assoc
-  ; ident = funExt ident-l , funExt ident-r
-  ; arrowIsSet = {!!}
+  { isAssociative = funExt is-isAssociative
+  ; isIdentity = funExt ident-l , funExt ident-r
+  ; arrowsAreSets = {!!}
   ; univalent = {!!}
   }
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index d6c1329..bc0fd81 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -25,10 +25,10 @@ module _ (ℓ : Level) where
     _∘_ SetsRaw = Function._∘′_
 
     SetsIsCategory : IsCategory SetsRaw
-    assoc SetsIsCategory = refl
-    proj₁ (ident SetsIsCategory) = funExt λ _ → refl
-    proj₂ (ident SetsIsCategory) = funExt λ _ → refl
-    arrowIsSet SetsIsCategory {B = (_ , s)} = setPi λ _ → s
+    isAssociative SetsIsCategory = refl
+    proj₁ (isIdentity SetsIsCategory) = funExt λ _ → refl
+    proj₂ (isIdentity SetsIsCategory) = funExt λ _ → refl
+    arrowsAreSets SetsIsCategory {B = (_ , s)} = setPi λ _ → s
     univalent SetsIsCategory = {!!}
 
   𝓢𝓮𝓽 Sets : Category (lsuc ℓ) ℓ
@@ -94,12 +94,12 @@ module _ {ℓa ℓb : Level} where
   representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
   representable {ℂ = ℂ} A = record
     { raw = record
-      { func* = λ B → ℂ [ A , B ] , arrowIsSet
+      { func* = λ B → ℂ [ A , B ] , arrowsAreSets
       ; func→ = ℂ [_∘_]
       }
     ; isFunctor = record
-      { ident = funExt λ _ → proj₂ ident
-      ; distrib = funExt λ x → sym assoc
+      { isIdentity = funExt λ _ → proj₂ isIdentity
+      ; isDistributive = funExt λ x → sym isAssociative
       }
     }
     where
@@ -109,12 +109,12 @@ module _ {ℓa ℓb : Level} where
   presheaf : {ℂ : Category ℓa ℓb} → Category.Object (Opposite ℂ) → Presheaf ℂ
   presheaf {ℂ = ℂ} B = record
     { raw = record
-      { func* = λ A → ℂ [ A , B ] , arrowIsSet
+      { func* = λ A → ℂ [ A , B ] , arrowsAreSets
       ; func→ = λ f g → ℂ [ g ∘ f ]
     }
     ; isFunctor = record
-      { ident = funExt λ x → proj₁ ident
-      ; distrib = funExt λ x → assoc
+      { isIdentity = funExt λ x → proj₁ isIdentity
+      ; isDistributive = funExt λ x → isAssociative
       }
     }
     where
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 686ae76..cec311d 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -49,6 +49,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   IsIdentity id = {A B : Object} {f : Arrow A B}
     → f ∘ id ≡ f × id ∘ f ≡ f
 
+  ArrowsAreSets : Set (ℓa ⊔ ℓb)
+  ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B)
+
   IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb
   IsInverseOf = λ f g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
 
@@ -80,9 +83,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
 -- Univalence is indexed by a raw category as well as an identity proof.
 module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   open RawCategory ℂ
-  module _ (ident : IsIdentity 𝟙) where
+  module _ (isIdentity : IsIdentity 𝟙) where
     idIso : (A : Object) → A ≅ A
-    idIso A = 𝟙 , (𝟙 , ident)
+    idIso A = 𝟙 , (𝟙 , isIdentity)
 
     -- Lemma 9.1.4 in [HoTT]
     id-to-iso : (A B : Object) → A ≡ B → A ≅ B
@@ -98,10 +101,10 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
   open RawCategory ℂ
   open Univalence ℂ public
   field
-    assoc : IsAssociative
-    ident : IsIdentity 𝟙
-    arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
-    univalent : Univalent ident
+    isAssociative : IsAssociative
+    isIdentity    : IsIdentity 𝟙
+    arrowsAreSets : ArrowsAreSets
+    univalent     : Univalent isIdentity
 
 -- `IsCategory` is a mere proposition.
 module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
@@ -112,12 +115,12 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
     open import Cubical.NType.Properties
 
     propIsAssociative : isProp IsAssociative
-    propIsAssociative x y i = arrowIsSet _ _ x y i
+    propIsAssociative x y i = arrowsAreSets _ _ x y i
 
     propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f)
     propIsIdentity a b i
-      = arrowIsSet _ _ (fst a) (fst b) i
-      , arrowIsSet _ _ (snd a) (snd b) i
+      = arrowsAreSets _ _ (fst a) (fst b) i
+      , arrowsAreSets _ _ (snd a) (snd b) i
 
     propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
     propArrowIsSet a b i = isSetIsProp a b i
@@ -126,9 +129,9 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
     propIsInverseOf x y = λ i →
       let
         h : fst x ≡ fst y
-        h = arrowIsSet _ _ (fst x) (fst y)
+        h = arrowsAreSets _ _ (fst x) (fst y)
         hh : snd x ≡ snd y
-        hh = arrowIsSet _ _ (snd x) (snd y)
+        hh = arrowsAreSets _ _ (snd x) (snd y)
       in h i , hh i
 
     module _ {A B : Object} {f : Arrow A B} where
@@ -139,14 +142,14 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
             open Cubical.NType.Properties
             geq : g ≡ g'
             geq = begin
-              g            ≡⟨ sym (fst ident) ⟩
+              g            ≡⟨ sym (fst isIdentity) ⟩
               g ∘ 𝟙        ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
-              g ∘ (f ∘ g') ≡⟨ assoc ⟩
+              g ∘ (f ∘ g') ≡⟨ isAssociative ⟩
               (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩
-              𝟙 ∘ g'       ≡⟨ snd ident ⟩
+              𝟙 ∘ g'       ≡⟨ snd isIdentity ⟩
               g'           ∎
 
-    propUnivalent : isProp (Univalent ident)
+    propUnivalent : isProp (Univalent isIdentity)
     propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
 
   private
@@ -159,23 +162,28 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
       -- projections of `IsCategory` - I've arbitrarily chosed to use this
       -- result from `x : IsCategory C`. I don't know which (if any) possibly
       -- adverse effects this may have.
-      ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ]
-      ident = propIsIdentity x X.ident Y.ident
+      isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ]
+      isIdentity = propIsIdentity x X.isIdentity Y.isIdentity
       done : x ≡ y
-      U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] → (b : Univalent a) → Set _
-      U eqwal bbb = (λ i → Univalent (eqwal i)) [ X.univalent ≡ bbb ]
+      U : ∀ {a : IsIdentity 𝟙}
+        → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ]
+        → (b : Univalent a)
+        → Set _
+      U eqwal bbb =
+        (λ i → Univalent (eqwal i))
+        [ X.univalent ≡ bbb ]
       P : (y : IsIdentity 𝟙)
-        → (λ _ → IsIdentity 𝟙) [ X.ident ≡ y ] → Set _
+        → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ y ] → Set _
       P y eq = ∀ (b' : Univalent y) → U eq b'
-      helper : ∀ (b' : Univalent X.ident)
-        → (λ _ → Univalent X.ident) [ X.univalent ≡ b' ]
+      helper : ∀ (b' : Univalent X.isIdentity)
+        → (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ]
       helper univ = propUnivalent x X.univalent univ
-      foo = pathJ P helper Y.ident ident
-      eqUni : U ident Y.univalent
+      foo = pathJ P helper Y.isIdentity isIdentity
+      eqUni : U isIdentity Y.univalent
       eqUni = foo Y.univalent
-      IC.assoc      (done i) = propIsAssociative x X.assoc Y.assoc i
-      IC.ident      (done i) = ident i
-      IC.arrowIsSet (done i) = propArrowIsSet x X.arrowIsSet Y.arrowIsSet i
+      IC.isAssociative      (done i) = propIsAssociative x X.isAssociative Y.isAssociative i
+      IC.isIdentity      (done i) = isIdentity i
+      IC.arrowsAreSets (done i) = propArrowIsSet x X.arrowsAreSets Y.arrowsAreSets i
       IC.univalent  (done i) = eqUni i
 
   propIsCategory : isProp (IsCategory C)
@@ -208,9 +216,9 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     RawCategory._∘_ OpRaw = Function.flip _∘_
 
     OpIsCategory : IsCategory OpRaw
-    IsCategory.assoc OpIsCategory = sym assoc
-    IsCategory.ident OpIsCategory = swap ident
-    IsCategory.arrowIsSet OpIsCategory = arrowIsSet
+    IsCategory.isAssociative OpIsCategory = sym isAssociative
+    IsCategory.isIdentity OpIsCategory = swap isIdentity
+    IsCategory.arrowsAreSets OpIsCategory = arrowsAreSets
     IsCategory.univalent OpIsCategory = {!!}
 
   Opposite : Category ℓa ℓb
@@ -234,9 +242,9 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
     open IsCategory
     module IsCat = IsCategory (ℂ .isCategory)
     rawIsCat : (i : I) → IsCategory (rawOp i)
-    assoc (rawIsCat i) = IsCat.assoc
-    ident (rawIsCat i) = IsCat.ident
-    arrowIsSet (rawIsCat i) = IsCat.arrowIsSet
+    isAssociative (rawIsCat i) = IsCat.isAssociative
+    isIdentity (rawIsCat i) = IsCat.isIdentity
+    arrowsAreSets (rawIsCat i) = IsCat.arrowsAreSets
     univalent (rawIsCat i) = IsCat.univalent
 
   Opposite-is-involution : Opposite (Opposite ℂ) ≡ ℂ
diff --git a/src/Cat/Category/Exponential.agda b/src/Cat/Category/Exponential.agda
index 137e501..1e443ce 100644
--- a/src/Cat/Category/Exponential.agda
+++ b/src/Cat/Category/Exponential.agda
@@ -35,5 +35,6 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}}
       transpose A f = proj₁ (isExponential A f)
 
 record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where
+  open Exponential public
   field
     exponent : (A B : Object ℂ) → Exponential ℂ A B
diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index 484cfdc..0269df9 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -7,7 +7,7 @@ open import Function
 
 open import Cat.Category
 
-open Category hiding (_∘_ ; raw)
+open Category hiding (_∘_ ; raw ; IsIdentity)
 
 module _ {ℓc ℓc' ℓd ℓd'}
     (ℂ : Category ℓc ℓc')
@@ -23,42 +23,40 @@ module _ {ℓc ℓc' ℓd ℓd'}
       func* : Object ℂ → Object 𝔻
       func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
 
+    IsIdentity : Set _
+    IsIdentity = {A : Object ℂ} → func→ (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {func* A}
+
+    IsDistributive : Set _
+    IsDistributive = {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
+      → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ]
+
   record IsFunctor (F : RawFunctor) : 𝓤 where
-    open RawFunctor F
+    open RawFunctor F public
     field
-      ident   : {c : Object ℂ} → func→ (𝟙 ℂ {c}) ≡ 𝟙 𝔻 {func* c}
-      distrib : {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
-        → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ]
+      isIdentity : IsIdentity
+      isDistributive : IsDistributive
 
   record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
     field
       raw : RawFunctor
       {{isFunctor}} : IsFunctor raw
 
-    private
-      module R = RawFunctor raw
+    open IsFunctor isFunctor public
 
-    func* : Object ℂ → Object 𝔻
-    func* = R.func*
-
-    func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
-    func→ = R.func→
-
-open IsFunctor
 open Functor
 
 module _
     {ℓa ℓb : Level}
     {ℂ 𝔻 : Category ℓa ℓb}
-    {F : RawFunctor ℂ 𝔻}
+    (F : RawFunctor ℂ 𝔻)
     where
   private
     module 𝔻 = IsCategory (isCategory 𝔻)
 
   propIsFunctor : isProp (IsFunctor _ _ F)
   propIsFunctor isF0 isF1 i = record
-    { ident = 𝔻.arrowIsSet _ _ isF0.ident isF1.ident i
-    ; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i
+    { isIdentity = 𝔻.arrowsAreSets _ _ isF0.isIdentity isF1.isIdentity i
+    ; isDistributive = 𝔻.arrowsAreSets _ _ isF0.isDistributive isF1.isDistributive i
     }
     where
       module isF0 = IsFunctor isF0
@@ -77,7 +75,7 @@ module _
 
   IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
   IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
-    (\ F → propIsFunctor {F = F}) (\ i → F i)
+    (\ F → propIsFunctor F) (\ i → F i)
     where
       open import Cubical.NType.Properties using (lemPropF)
 
@@ -108,8 +106,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
       dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ]
       dist = begin
         (F→ ∘ G→) (A [ α1 ∘ α0 ])         ≡⟨ refl ⟩
-        F→ (G→ (A [ α1 ∘ α0 ]))           ≡⟨ cong F→ (G .isFunctor .distrib)⟩
-        F→ (B [ G→ α1 ∘ G→ α0 ])          ≡⟨ F .isFunctor .distrib ⟩
+        F→ (G→ (A [ α1 ∘ α0 ]))           ≡⟨ cong F→ (isDistributive G) ⟩
+        F→ (B [ G→ α1 ∘ G→ α0 ])          ≡⟨ isDistributive F ⟩
         C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎
 
     _∘fr_ : RawFunctor A C
@@ -118,12 +116,12 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
     instance
       isFunctor' : IsFunctor A C _∘fr_
       isFunctor' = record
-        { ident = begin
+        { isIdentity = begin
           (F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩
-          F→ (G→ (𝟙 A))   ≡⟨ cong F→ (G .isFunctor .ident)⟩
-          F→ (𝟙 B)        ≡⟨ F .isFunctor .ident ⟩
+          F→ (G→ (𝟙 A))   ≡⟨ cong F→ (isIdentity G)⟩
+          F→ (𝟙 B)        ≡⟨ isIdentity F ⟩
           𝟙 C             ∎
-        ; distrib = dist
+        ; isDistributive = dist
         }
 
   _∘f_ : Functor A C
@@ -137,7 +135,7 @@ identity = record
     ; func→ = λ x → x
     }
   ; isFunctor = record
-    { ident = refl
-    ; distrib = refl
+    { isIdentity = refl
+    ; isDistributive = refl
     }
   }
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index b001344..190592e 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -17,106 +17,77 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object 
 
   iso-is-epi : Isomorphism f → Epimorphism {X = X} f
   iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
-    g₀              ≡⟨ sym (proj₁ ident) ⟩
+    g₀              ≡⟨ sym (proj₁ isIdentity) ⟩
     g₀ ∘ 𝟙          ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
-    g₀ ∘ (f ∘ f-)   ≡⟨ assoc ⟩
+    g₀ ∘ (f ∘ f-)   ≡⟨ isAssociative ⟩
     (g₀ ∘ f) ∘ f-   ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩
-    (g₁ ∘ f) ∘ f-   ≡⟨ sym assoc ⟩
+    (g₁ ∘ f) ∘ f-   ≡⟨ sym isAssociative ⟩
     g₁ ∘ (f ∘ f-)   ≡⟨ cong (_∘_ g₁) right-inv ⟩
-    g₁ ∘ 𝟙          ≡⟨ proj₁ ident ⟩
+    g₁ ∘ 𝟙          ≡⟨ proj₁ isIdentity ⟩
     g₁              ∎
 
   iso-is-mono : Isomorphism f → Monomorphism {X = X} f
   iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq =
     begin
-    g₀            ≡⟨ sym (proj₂ ident) ⟩
+    g₀            ≡⟨ sym (proj₂ isIdentity) ⟩
     𝟙 ∘ g₀        ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩
-    (f- ∘ f) ∘ g₀ ≡⟨ sym assoc ⟩
+    (f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩
     f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩
-    f- ∘ (f ∘ g₁) ≡⟨ assoc ⟩
+    f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩
     (f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩
-    𝟙 ∘ g₁        ≡⟨ proj₂ ident ⟩
+    𝟙 ∘ g₁        ≡⟨ proj₂ isIdentity ⟩
     g₁            ∎
 
   iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
   iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso
 
-{-
-epi-mono-is-not-iso : ∀ {ℓ ℓ'} → ¬ ((ℂ : Category {ℓ} {ℓ'}) {A B X : Object ℂ} (f : Arrow ℂ A B ) → Epimorphism {ℂ = ℂ} {X = X} f → Monomorphism {ℂ = ℂ} {X = X} f → Isomorphism {ℂ = ℂ} f)
-epi-mono-is-not-iso f =
-  let k = f {!!} {!!} {!!} {!!}
-  in {!!}
--}
+-- TODO: We want to avoid defining the yoneda embedding going through the
+-- category of categories (since it doesn't exist).
+open import Cat.Categories.Cat using (RawCat)
 
-open import Cat.Category
-open Category
-open Functor
+module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat ℓ ℓ)) where
+  open import Cat.Categories.Fun
+  open import Cat.Categories.Sets
+  module Cat = Cat.Categories.Cat
+  open import Cat.Category.Exponential
+  open Functor
+  𝓢 = Sets ℓ
+  private
+    Catℓ : Category _ _
+    Catℓ = record { raw = RawCat ℓ ℓ ; isCategory = unprovable}
+    prshf = presheaf {ℂ = ℂ}
+    module ℂ = Category ℂ
 
--- module _ {ℓ : Level} {ℂ : Category ℓ ℓ}
---   {isSObj : isSet (ℂ .Object)}
---   {isz2 : ∀ {ℓ} → {A B : Set ℓ} → isSet (Sets [ A , B ])} where
---   -- open import Cat.Categories.Cat using (Cat)
---   open import Cat.Categories.Fun
---   open import Cat.Categories.Sets
---   -- module Cat = Cat.Categories.Cat
---   open import Cat.Category.Exponential
---   private
---     Catℓ = Cat ℓ ℓ
---     prshf = presheaf {ℂ = ℂ}
---     module ℂ = IsCategory (ℂ .isCategory)
+    _⇑_ : (A B : Category.Object Catℓ) → Category.Object Catℓ
+    A ⇑ B = (exponent A B) .obj
+      where
+        open HasExponentials (Cat.hasExponentials ℓ unprovable)
 
---     -- Exp : Set (lsuc (lsuc ℓ))
---     -- Exp = Exponential (Cat (lsuc ℓ) ℓ)
---     --   Sets (Opposite ℂ)
+    module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where
+      :func→: : NaturalTransformation (prshf A) (prshf B)
+      :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.isAssociative
 
---     _⇑_ : (A B : Catℓ .Object) → Catℓ .Object
---     A ⇑ B = (exponent A B) .obj
---       where
---         open HasExponentials (Cat.hasExponentials ℓ)
+    module _ {c : Category.Object ℂ} where
+      eqTrans : (λ _ → Transformation (prshf c) (prshf c))
+        [ (λ _ x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
+      eqTrans = funExt λ x → funExt λ x → ℂ.isIdentity .proj₂
 
---     module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where
---       :func→: : NaturalTransformation (prshf A) (prshf B)
---       :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.assoc
+      open import Cubical.NType.Properties
+      open import Cat.Categories.Fun
+      :ident: : :func→: (ℂ.𝟙 {c}) ≡ Category.𝟙 Fun {A = prshf c}
+      :ident: = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq
+        where
+          eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c)
+          eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
 
---     module _ {c : ℂ .Object} where
---       eqTrans : (λ _ → Transformation (prshf c) (prshf c))
---         [ (λ _ x → ℂ [ ℂ .𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
---       eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂
-
---       eqNat : (λ i → Natural (prshf c) (prshf c) (eqTrans i))
---         [(λ _ → funExt (λ _ → ℂ.assoc)) ≡ identityNatural (prshf c)]
---       eqNat = λ i {A} {B} f →
---         let
---          open IsCategory (Sets .isCategory)
---          lemm : (Sets [ eqTrans i B ∘ prshf c .func→ f ]) ≡
---            (Sets [ prshf c .func→ f ∘ eqTrans i A ])
---          lemm = {!!}
---          lem : (λ _ → Sets [ Functor.func* (prshf c) A , prshf c .func* B ])
---                 [ Sets [ eqTrans i B ∘ prshf c .func→ f ]
---                 ≡ Sets [ prshf c .func→ f ∘ eqTrans i A ] ]
---          lem
---           = isz2 _ _ lemm _ i
---             -- (Sets [ eqTrans i B ∘ prshf c .func→ f ])
---             -- (Sets [ prshf c .func→ f ∘ eqTrans i A ])
---             -- lemm
---             -- _ i
---         in
---           lem
---       -- eqNat = λ {A} {B} i ℂ[B,A] i' ℂ[A,c] →
---       --   let
---       --     k : ℂ [ {!!} , {!!} ]
---       --     k = ℂ[A,c]
---       --   in {!ℂ [ ? ∘ ? ]!}
-
---       :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c})
---       :ident: = Σ≡ eqTrans eqNat
-
---   yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}})
---   yoneda = record
---     { func* = prshf
---     ; func→ = :func→:
---     ; isFunctor = record
---       { ident = :ident:
---       ; distrib = {!!}
---       }
---     }
+  yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = 𝓢})
+  yoneda = record
+    { raw = record
+      { func* = prshf
+      ; func→ = :func→:
+      }
+    ; isFunctor = record
+      { isIdentity = :ident:
+      ; isDistributive = {!!}
+      }
+    }
diff --git a/src/Cat/Equality.agda b/src/Cat/Equality.agda
index c3c333d..d6b3dc0 100644
--- a/src/Cat/Equality.agda
+++ b/src/Cat/Equality.agda
@@ -20,28 +20,3 @@ module Equality where
         Σ≡ : a ≡ b
         proj₁ (Σ≡ i) = proj₁≡ i
         proj₂ (Σ≡ i) = proj₂≡ i
-
-        -- Remark 2.7.1: This theorem:
-        --
-        --   (x , u) ≡ (x , v) → u ≡ v
-        --
-        -- does *not* hold! We can only conclude that there *exists* `p : x ≡ x`
-        -- such that
-        --
-        --   p* u ≡ v
-        -- thm : isSet A → (∀ {a} → isSet (B a)) → isSet (Σ A B)
-        -- thm sA sB (x , y) (x' , y') p q = res
-        --   where
-        --     x≡x'0 : x ≡ x'
-        --     x≡x'0 = λ i → proj₁ (p i)
-        --     x≡x'1 : x ≡ x'
-        --     x≡x'1 = λ i → proj₁ (q i)
-        --     someP : x ≡ x'
-        --     someP = {!!}
-        --     tricky : {!y!} ≡ y'
-        --     tricky = {!!}
-        --     -- res' : (λ _ → Σ A B) [ (x , y) ≡ (x' , y') ]
-        --     res' : ({!!} , {!!}) ≡ ({!!} , {!!})
-        --     res' = {!!}
-        --     res : p ≡ q
-        --     res i = {!res'!}