diff --git a/BACKLOG.md b/BACKLOG.md
index bfbb32b..ed1b205 100644
--- a/BACKLOG.md
+++ b/BACKLOG.md
@@ -1,9 +1,18 @@
 Backlog
 =======
 
-Prove univalence for various categories
-
 Prove postulates in `Cat.Wishlist`
+`ntypeCommulative` might be there as well.
+
+Prove that the opposite category is a category.
+
+Prove univalence for the category of
+  * sets
+  * functors and natural transformations
+
+Prove:
+  * `isProp (Product ...)`
+  * `isProp (HasProducts ...)`
 
 * Functor ✓
 * Applicative Functor ✗
@@ -11,4 +20,11 @@ Prove postulates in `Cat.Wishlist`
     * Monoidal functor ✗
   * Tensorial strength ✗
 * Category ✓
-  * Monoidal category ✗
\ No newline at end of file
+  * Monoidal category ✗
+* Monad
+  * Monoidal monad ✓
+  * Kleisli monad ✓
+  * Problem 2.3 in voe
+    * 1st contruction ~ monoidal ✓
+    * 2nd contruction ~ klesli ✓
+      * 1st ≃ 2nd ✗
diff --git a/CHANGELOG.md b/CHANGELOG.md
index a7a3d14..625d640 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,9 +1,27 @@
 Changelog
 =========
 
+Version 1.4.0
+-------------
+Adds documentation to a number of modules.
+
+Adds an "equality principle" for categories and monads.
+
+Prove that `IsMonad` is a mere proposition.
+
+Provides the yoneda embedding without relying on the existence of a category of
+categories. This is acheived by providing some of the data needed to make a ccc
+out of the category of categories without actually having such a category.
+
+Renames functors object map and arrow map to `omap` and `fmap`.
+
+Prove that kleisli- and monoidal- monads are equivalent!
+
+[WIP] Started working on the proofs for univalence for the category of sets and
+the category of functors.
+
 Version 1.3.0
 -------------
-
 Removed unused modules and streamlined things more: All specific categories are
 in the namespace `Cat.Categories`.
 
diff --git a/README.md b/README.md
index 34467b0..8088a60 100644
--- a/README.md
+++ b/README.md
@@ -14,10 +14,12 @@ Dependencies
 ------------
 To succesfully compile the following is needed:
 
-* Agda version >= [`707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43`](https://github.com/agda/agda/commit/707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43)
-* [Agda Standard Library](https://github.com/agda/agda-stdlib)
+* The Agda release candidate 2.5.4[^1]
+* The experimental branch of [Agda Standard Library](https://github.com/agda/agda-stdlib)
 * [Cubical](https://github.com/Saizan/cubical-demo/)
 
+[^1]: At least version >= [`707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43`](https://github.com/agda/agda/commit/707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43)
+
 It's important to have the right version of these - but which one is the right
 is in constant flux. It's most likely the newest one.
 
diff --git a/libs/agda-stdlib b/libs/agda-stdlib
index b9c8e02..fbd8ba7 160000
--- a/libs/agda-stdlib
+++ b/libs/agda-stdlib
@@ -1 +1 @@
-Subproject commit b9c8e02597751a1b15045cbc5108c221999bd540
+Subproject commit fbd8ba7ea84c4b643fd08797b4031b18a59f561d
diff --git a/libs/cubical b/libs/cubical
index 0d3f02e..5b35333 160000
--- a/libs/cubical
+++ b/libs/cubical
@@ -1 +1 @@
-Subproject commit 0d3f02e68297e940227137beac45fc1bce6e2bea
+Subproject commit 5b35333dbbd8fa523e478c1cfe60657321ca38fe
diff --git a/src/Cat.agda b/src/Cat.agda
index 20c5d69..86e6879 100644
--- a/src/Cat.agda
+++ b/src/Cat.agda
@@ -1,19 +1,20 @@
 module Cat where
 
-import Cat.Category
+open import Cat.Category
 
-import Cat.Category.Functor
-import Cat.Category.Product
-import Cat.Category.Exponential
-import Cat.Category.CartesianClosed
-import Cat.Category.NaturalTransformation
-import Cat.Category.Yoneda
-import Cat.Category.Monad
+open import Cat.Category.Functor
+open import Cat.Category.Product
+open import Cat.Category.Exponential
+open import Cat.Category.CartesianClosed
+open import Cat.Category.NaturalTransformation
+open import Cat.Category.Yoneda
+open import Cat.Category.Monad
+open import Cat.Category.Monad.Voevodsky
 
-import Cat.Categories.Sets
-import Cat.Categories.Cat
-import Cat.Categories.Rel
-import Cat.Categories.Free
-import Cat.Categories.Fun
-import Cat.Categories.Cube
-import Cat.Categories.CwF
+open import Cat.Categories.Sets
+open import Cat.Categories.Cat
+open import Cat.Categories.Rel
+open import Cat.Categories.Free
+open import Cat.Categories.Fun
+open import Cat.Categories.Cube
+open import Cat.Categories.CwF
diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 5a0d2dd..8c7bcbb 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -4,20 +4,20 @@
 module Cat.Categories.Cat where
 
 open import Agda.Primitive
-open import Cubical
-open import Function
 open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
 
+open import Cubical
+open import Cubical.Sigma
+
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
-open import Cat.Category.Exponential
+open import Cat.Category.Exponential hiding (_×_ ; product)
 open import Cat.Category.NaturalTransformation
 
 open import Cat.Equality
 open Equality.Data.Product
 
-open Functor using (func→ ; func*)
 open Category using (Object ; 𝟙)
 
 -- The category of categories
@@ -25,14 +25,14 @@ module _ (ℓ ℓ' : Level) where
   private
     module _ {𝔸 𝔹 ℂ 𝔻 : Category ℓ ℓ'} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻} where
       assc : F[ H ∘ F[ G ∘ F ] ] ≡ F[ F[ H ∘ G ] ∘ F ]
-      assc = Functor≡ refl refl
+      assc = Functor≡ refl
 
     module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where
       ident-r : F[ F ∘ identity ] ≡ F
-      ident-r = Functor≡ refl refl
+      ident-r = Functor≡ refl
 
       ident-l : F[ identity ∘ F ] ≡ F
-      ident-l = Functor≡ refl refl
+      ident-l = Functor≡ refl
 
   RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
   RawCat =
@@ -46,313 +46,325 @@ module _ (ℓ ℓ' : Level) where
     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.
+    ident : IsIdentity identity
+    ident = ident-r , ident-l
 
-  -- Because of the note above there is not category of categories.
+  -- 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.
+  --
+  -- Because of this there is no 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.
+-- | In the following we will pretend there is a category of categories when
+-- e.g. talking about it being cartesian closed. It still makes sense to
+-- construct these things even though that category does not exist.
+--
+-- If the notion of a category is later generalized to work on different
+-- homotopy levels, then the proof that the category of categories is cartesian
+-- closed will follow immediately from these constructions.
+
+-- | the category of categories have products.
+module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
+  private
+    module ℂ = Category ℂ
+    module 𝔻 = Category 𝔻
+
+    Obj = Object ℂ × Object 𝔻
+    Arr  : Obj → Obj → Set ℓ'
+    Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ]
+    𝟙' : {o : Obj} → Arr o o
+    𝟙' = 𝟙 ℂ , 𝟙 𝔻
+    _∘_ :
+      {a b c : Obj} →
+      Arr b c →
+      Arr a b →
+      Arr a c
+    _∘_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]}
+
+    rawProduct : RawCategory ℓ ℓ'
+    RawCategory.Object rawProduct = Obj
+    RawCategory.Arrow  rawProduct = Arr
+    RawCategory.𝟙      rawProduct = 𝟙'
+    RawCategory._∘_    rawProduct = _∘_
+    open RawCategory   rawProduct
+
+    arrowsAreSets : ArrowsAreSets
+    arrowsAreSets = setSig {sA = ℂ.arrowsAreSets} {sB = λ x → 𝔻.arrowsAreSets}
+    isIdentity : IsIdentity 𝟙'
+    isIdentity
+      = Σ≡ (fst ℂ.isIdentity) (fst 𝔻.isIdentity)
+      , Σ≡ (snd ℂ.isIdentity) (snd 𝔻.isIdentity)
+    postulate univalent : Univalence.Univalent rawProduct isIdentity
+    instance
+      isCategory : IsCategory rawProduct
+      IsCategory.isAssociative isCategory = Σ≡ ℂ.isAssociative 𝔻.isAssociative
+      IsCategory.isIdentity    isCategory = isIdentity
+      IsCategory.arrowsAreSets isCategory = arrowsAreSets
+      IsCategory.univalent     isCategory = univalent
+
+  object : Category ℓ ℓ'
+  Category.raw object = rawProduct
+
+  proj₁ : Functor object ℂ
+  proj₁ = record
+    { raw = record
+      { omap = fst ; fmap = fst }
+    ; isFunctor = record
+      { isIdentity = refl ; isDistributive = refl }
+    }
+
+  proj₂ : Functor object 𝔻
+  proj₂ = record
+    { raw = record
+      { omap = snd ; fmap = snd }
+    ; isFunctor = record
+      { isIdentity = refl ; isDistributive = refl }
+    }
+
+  module _ {X : Category ℓ ℓ'} (x₁ : Functor X ℂ) (x₂ : Functor X 𝔻) where
+    private
+      x : Functor X object
+      x = record
+        { raw = record
+          { omap = λ x → x₁.omap x , x₂.omap x
+          ; fmap = λ x → x₁.fmap x , x₂.fmap x
+          }
+        ; isFunctor = record
+          { isIdentity     = Σ≡ x₁.isIdentity x₂.isIdentity
+          ; isDistributive = Σ≡ x₁.isDistributive x₂.isDistributive
+          }
+        }
+        where
+          open module x₁ = Functor x₁
+          open module x₂ = Functor x₂
+
+      isUniqL : F[ proj₁ ∘ x ] ≡ x₁
+      isUniqL = Functor≡ refl
+
+      isUniqR : F[ proj₂ ∘ x ] ≡ x₂
+      isUniqR = Functor≡ refl
+
+      isUniq : F[ proj₁ ∘ x ] ≡ x₁ × F[ proj₂ ∘ x ] ≡ x₂
+      isUniq = isUniqL , isUniqR
+
+    isProduct : ∃![ x ] (F[ proj₁ ∘ x ] ≡ x₁ × F[ proj₂ ∘ x ] ≡ x₂)
+    isProduct = x , isUniq
+
 module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
+  private
+    Catℓ = Cat ℓ ℓ' unprovable
+
   module _ (ℂ 𝔻 : Category ℓ ℓ') where
     private
-      Catt = Cat ℓ ℓ' unprovable
-      :Object: = Object ℂ × Object 𝔻
-      :Arrow:  : :Object: → :Object: → Set ℓ'
-      :Arrow: (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ]
-      :𝟙: : {o : :Object:} → :Arrow: o o
-      :𝟙: = 𝟙 ℂ , 𝟙 𝔻
-      _:⊕:_ :
-        {a b c : :Object:} →
-        :Arrow: b c →
-        :Arrow: a b →
-        :Arrow: a c
-      _:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]}
+      module P = CatProduct ℂ 𝔻
 
-      :rawProduct: : RawCategory ℓ ℓ'
-      RawCategory.Object :rawProduct: = :Object:
-      RawCategory.Arrow :rawProduct: = :Arrow:
-      RawCategory.𝟙 :rawProduct: = :𝟙:
-      RawCategory._∘_ :rawProduct: = _:⊕:_
-      open RawCategory :rawProduct:
+      rawProduct : RawProduct Catℓ ℂ 𝔻
+      RawProduct.object rawProduct = P.object
+      RawProduct.proj₁  rawProduct = P.proj₁
+      RawProduct.proj₂  rawProduct = P.proj₂
 
-      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.isAssociative :isCategory: = Σ≡ C.isAssociative D.isAssociative
-        IsCategory.isIdentity :isCategory: = ident'
-        IsCategory.arrowsAreSets :isCategory: = issSet
-        IsCategory.univalent :isCategory: = univalent
+      isProduct : IsProduct Catℓ _ _ rawProduct
+      IsProduct.isProduct isProduct = P.isProduct
 
-      :product: : Category ℓ ℓ'
-      Category.raw :product: = :rawProduct:
+    product : Product Catℓ ℂ 𝔻
+    Product.raw       product = rawProduct
+    Product.isProduct product = isProduct
 
-      proj₁ : Catt [ :product: , ℂ ]
-      proj₁ = record
-        { raw = record { func* = fst ; func→ = fst }
-        ; isFunctor = record { isIdentity = refl ; isDistributive = refl }
-        }
-
-      proj₂ : Catt [ :product: , 𝔻 ]
-      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
-        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₂
-
-        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
-
-        isUniqR : Catt [ proj₂ ∘ x ] ≡ x₂
-        isUniqR = Functor≡ refl refl
-
-        isUniq : Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂
-        isUniq = isUniqL , isUniqR
-
-        uniq : ∃![ x ] (Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂)
-        uniq = x , isUniq
-
-    instance
-      isProduct : IsProduct Catt proj₁ proj₂
-      isProduct = uniq
-
-    product : Product {ℂ = Catt} ℂ 𝔻
-    product = record
-      { obj = :product:
-      ; proj₁ = proj₁
-      ; proj₂ = proj₂
-      }
-
-module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
-  Catt = Cat ℓ ℓ' unprovable
   instance
-    hasProducts : HasProducts Catt
-    hasProducts = record { product = product unprovable }
+    hasProducts : HasProducts Catℓ
+    hasProducts = record { product = product }
 
--- Basically proves that `Cat ℓ ℓ` is cartesian closed.
-module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
+-- | The category of categories have expoentntials - and because it has products
+-- it is therefory also cartesian closed.
+module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
   private
     open Data.Product
     open import Cat.Categories.Fun
+    module ℂ = Category ℂ
+    module 𝔻 = Category 𝔻
+    Categoryℓ = Category ℓ ℓ
+    open Fun ℂ 𝔻 renaming (identity to idN)
 
+    omap : Functor ℂ 𝔻 × Object ℂ → Object 𝔻
+    omap (F , A) = Functor.omap F A
+
+  -- The exponential object
+  object : Categoryℓ
+  object = Fun
+
+  module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where
+    private
+      F : Functor ℂ 𝔻
+      F = proj₁ dom
+      A : Object ℂ
+      A = proj₂ dom
+
+      G : Functor ℂ 𝔻
+      G = proj₁ cod
+      B : Object ℂ
+      B = proj₂ cod
+
+      module F = Functor F
+      module G = Functor G
+
+    fmap : (pobj : NaturalTransformation F G × ℂ [ A , B ])
+      → 𝔻 [ F.omap A , G.omap B ]
+    fmap ((θ , θNat) , f) = result
+      where
+        θA : 𝔻 [ F.omap A , G.omap A ]
+        θA = θ A
+        θB : 𝔻 [ F.omap B , G.omap B ]
+        θB = θ B
+        F→f : 𝔻 [ F.omap A , F.omap B ]
+        F→f = F.fmap f
+        G→f : 𝔻 [ G.omap A , G.omap B ]
+        G→f = G.fmap f
+        l : 𝔻 [ F.omap A , G.omap B ]
+        l = 𝔻 [ θB ∘ F.fmap f ]
+        r : 𝔻 [ F.omap A , G.omap B ]
+        r = 𝔻 [ G.fmap f ∘ θA ]
+        result : 𝔻 [ F.omap A , G.omap B ]
+        result = l
+
+  open CatProduct renaming (object to _⊗_) using ()
+
+  module _ {c : Functor ℂ 𝔻 × Object ℂ} where
+    private
+      F : Functor ℂ 𝔻
+      F = proj₁ c
+      C : Object ℂ
+      C = proj₂ c
+
+    ident : fmap {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻
+    ident = begin
+      fmap {c} {c} (𝟙 (object ⊗ ℂ) {c})    ≡⟨⟩
+      fmap {c} {c} (idN F , 𝟙 ℂ)             ≡⟨⟩
+      𝔻 [ identityTrans F C ∘ F.fmap (𝟙 ℂ)]    ≡⟨⟩
+      𝔻 [ 𝟙 𝔻 ∘ F.fmap (𝟙 ℂ)]                  ≡⟨ proj₂ 𝔻.isIdentity ⟩
+      F.fmap (𝟙 ℂ)                             ≡⟨ F.isIdentity ⟩
+      𝟙 𝔻                                       ∎
+      where
+        module F = Functor F
+
+  module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where
+    private
+      F = F×A .proj₁
+      A = F×A .proj₂
+      G = G×B .proj₁
+      B = G×B .proj₂
+      H = H×C .proj₁
+      C = H×C .proj₂
+      module F = Functor F
+      module G = Functor G
+      module H = Functor H
+
+    module _
+      -- NaturalTransformation F G × ℂ .Arrow A B
+      {θ×f : NaturalTransformation F G × ℂ [ A , B ]}
+      {η×g : NaturalTransformation G H × ℂ [ B , C ]} where
+      private
+        θ : Transformation F G
+        θ = proj₁ (proj₁ θ×f)
+        θNat : Natural F G θ
+        θNat = proj₂ (proj₁ θ×f)
+        f : ℂ [ A , B ]
+        f = proj₂ θ×f
+        η : Transformation G H
+        η = proj₁ (proj₁ η×g)
+        ηNat : Natural G H η
+        ηNat = proj₂ (proj₁ η×g)
+        g : ℂ [ B , C ]
+        g = proj₂ η×g
+
+        ηθNT : NaturalTransformation F H
+        ηθNT = Category._∘_ Fun {F} {G} {H} (η , ηNat) (θ , θNat)
+
+        ηθ = proj₁ ηθNT
+        ηθNat = proj₂ ηθNT
+
+      isDistributive :
+          𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F.fmap ( ℂ [ g ∘ f ] ) ]
+        ≡ 𝔻 [ 𝔻 [ η C ∘ G.fmap g ] ∘ 𝔻 [ θ B ∘ F.fmap f ] ]
+      isDistributive = begin
+        𝔻 [ (ηθ C) ∘ F.fmap (ℂ [ g ∘ f ]) ]
+          ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩
+        𝔻 [ H.fmap (ℂ [ g ∘ f ]) ∘ (ηθ A) ]
+          ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.isDistributive) ⟩
+        𝔻 [ 𝔻 [ H.fmap g ∘ H.fmap f ] ∘ (ηθ A) ]
+          ≡⟨ sym 𝔻.isAssociative ⟩
+        𝔻 [ H.fmap g ∘ 𝔻 [ H.fmap f ∘ ηθ A ] ]
+          ≡⟨ cong (λ φ → 𝔻 [ H.fmap g ∘ φ ]) 𝔻.isAssociative ⟩
+        𝔻 [ H.fmap g ∘ 𝔻 [ 𝔻 [ H.fmap f ∘ η A ] ∘ θ A ] ]
+          ≡⟨ cong (λ φ → 𝔻 [ H.fmap g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩
+        𝔻 [ H.fmap g ∘ 𝔻 [ 𝔻 [ η B ∘ G.fmap f ] ∘ θ A ] ]
+          ≡⟨ cong (λ φ → 𝔻 [ H.fmap g ∘ φ ]) (sym 𝔻.isAssociative) ⟩
+        𝔻 [ H.fmap g ∘ 𝔻 [ η B ∘ 𝔻 [ G.fmap f ∘ θ A ] ] ]
+          ≡⟨ 𝔻.isAssociative ⟩
+        𝔻 [ 𝔻 [ H.fmap g ∘ η B ] ∘ 𝔻 [ G.fmap f ∘ θ A ] ]
+          ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ G.fmap f ∘ θ A ] ]) (sym (ηNat g)) ⟩
+        𝔻 [ 𝔻 [ η C ∘ G.fmap g ] ∘ 𝔻 [ G.fmap f ∘ θ A ] ]
+          ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ G.fmap g ] ∘ φ ]) (sym (θNat f)) ⟩
+        𝔻 [ 𝔻 [ η C ∘ G.fmap g ] ∘ 𝔻 [ θ B ∘ F.fmap f ] ] ∎
+
+  eval : Functor (CatProduct.object object ℂ) 𝔻
+  eval = record
+    { raw = record
+      { omap = omap
+      ; fmap = λ {dom} {cod} → fmap {dom} {cod}
+      }
+    ; isFunctor = record
+      { isIdentity = λ {o} → ident {o}
+      ; isDistributive = λ {f u n k y} → isDistributive {f} {u} {n} {k} {y}
+      }
+    }
+
+  module _ (𝔸 : Category ℓ ℓ) (F : Functor (𝔸 ⊗ ℂ) 𝔻) where
+    postulate
+      parallelProduct
+        : Functor 𝔸 object → Functor ℂ ℂ
+        → Functor (𝔸 ⊗ ℂ) (object ⊗ ℂ)
+      transpose : Functor 𝔸 object
+      eq : F[ eval ∘ (parallelProduct transpose (identity {C = ℂ})) ] ≡ F
+      -- eq : F[ :eval: ∘ {!!} ] ≡ F
+      -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F
+      -- eq' : (Catℓ [ :eval: ∘
+      --   (record { product = product } HasProducts.|×| transpose)
+      --   (𝟙 Catℓ)
+      --   ])
+      --   ≡ F
+
+    -- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758`
+    -- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [
+    -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose =
+    -- transpose , eq
+
+-- We don't care about filling out the holes below since they are anyways hidden
+-- behind an unprovable statement.
+module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
+  private
     Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ)
     Catℓ = Cat ℓ ℓ unprovable
+
     module _ (ℂ 𝔻 : Category ℓ ℓ) where
-      open Fun ℂ 𝔻 renaming (identity to idN)
-      private
-        :obj: : Object Catℓ
-        :obj: = Fun
+      module CatExp = CatExponential ℂ 𝔻
+      _⊗_ = CatProduct.object
 
-        :func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻
-        :func*: (F , A) = func* F A
+      -- Filling the hole causes Agda to loop indefinitely.
+      eval : Functor (CatExp.object ⊗ ℂ) 𝔻
+      eval = {!CatExp.eval!}
 
-      module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where
-        private
-          F : Functor ℂ 𝔻
-          F = proj₁ dom
-          A : Object ℂ
-          A = proj₂ dom
+      isExponential : IsExponential Catℓ ℂ 𝔻 CatExp.object eval
+      isExponential = {!CatExp.isExponential!}
 
-          G : Functor ℂ 𝔻
-          G = proj₁ cod
-          B : Object ℂ
-          B = proj₂ cod
-
-        :func→: : (pobj : NaturalTransformation F G × ℂ [ A , B ])
-          → 𝔻 [ func* F A , func* G B ]
-        :func→: ((θ , θNat) , f) = result
-          where
-            θA : 𝔻 [ func* F A , func* G A ]
-            θA = θ A
-            θB : 𝔻 [ func* F B , func* G B ]
-            θB = θ 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 : 𝔻 [ 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 : 𝔻 [ func* F A , func* G B ]
-            result = l
-
-      _×p_ = product unprovable
-
-      module _ {c : Functor ℂ 𝔻 × Object ℂ} where
-        private
-          F : Functor ℂ 𝔻
-          F = proj₁ c
-          C : Object ℂ
-          C = proj₂ c
-
-        -- NaturalTransformation F G × ℂ .Arrow A B
-        -- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙
-        -- :ident: = trans (proj₂ 𝔻.isIdentity) (F .isIdentity)
-        --   where
-        --     open module 𝔻 = IsCategory (𝔻 .isCategory)
-        -- Unfortunately the equational version has some ambigous arguments.
-
-        :ident: : :func→: {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻
-        :ident: = begin
-          :func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩
-          :func→: {c} {c} (idN F , 𝟙 ℂ)             ≡⟨⟩
-          𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)]           ≡⟨⟩
-          𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)]                        ≡⟨ proj₂ 𝔻.isIdentity ⟩
-          func→ F (𝟙 ℂ)                                    ≡⟨ F.isIdentity ⟩
-          𝟙 𝔻                                               ∎
-          where
-            open module 𝔻 = Category 𝔻
-            open module F = Functor F
-
-      module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where
-        F = F×A .proj₁
-        A = F×A .proj₂
-        G = G×B .proj₁
-        B = G×B .proj₂
-        H = H×C .proj₁
-        C = H×C .proj₂
-        -- Not entirely clear what this is at this point:
-        _P⊕_ = Category._∘_ (Product.obj (:obj: ×p ℂ)) {F×A} {G×B} {H×C}
-        module _
-          -- NaturalTransformation F G × ℂ .Arrow A B
-          {θ×f : NaturalTransformation F G × ℂ [ A , B ]}
-          {η×g : NaturalTransformation G H × ℂ [ B , C ]} where
-          private
-            θ : Transformation F G
-            θ = proj₁ (proj₁ θ×f)
-            θNat : Natural F G θ
-            θNat = proj₂ (proj₁ θ×f)
-            f : ℂ [ A , B ]
-            f = proj₂ θ×f
-            η : Transformation G H
-            η = proj₁ (proj₁ η×g)
-            ηNat : Natural G H η
-            ηNat = proj₂ (proj₁ η×g)
-            g : ℂ [ B , C ]
-            g = proj₂ η×g
-
-            ηθNT : NaturalTransformation F H
-            ηθNT = Category._∘_ Fun {F} {G} {H} (η , ηNat) (θ , θNat)
-
-            ηθ = proj₁ ηθNT
-            ηθNat = proj₂ ηθNT
-
-          :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 ]) ⟩
-            𝔻 [ 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 Category 𝔻
-              module H = Functor H
-
-      :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻
-      :eval: = record
-        { raw = record
-          { func* = :func*:
-          ; func→ = λ {dom} {cod} → :func→: {dom} {cod}
-          }
-        ; isFunctor = record
-          { 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 {ℓ} {ℓ} unprovable) renaming (_|×|_ to parallelProduct)
-
-        postulate
-          transpose : Functor 𝔸 :obj:
-          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)
-          --   (𝟙 Catℓ)
-          --   ])
-          --   ≡ F
-
-        -- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758`
-        -- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [
-        -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose =
-        -- transpose , eq
-
-      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
-      :exponent: : Exponential Catℓ ℂ 𝔻
-      :exponent: = record
-        { obj = :obj:
-        ; eval = :eval:
-        ; isExponential = :isExponential:
+      exponent : Exponential Catℓ ℂ 𝔻
+      exponent = record
+        { obj           = CatExp.object
+        ; eval          = eval
+        ; isExponential = isExponential
         }
 
   hasExponentials : HasExponentials Catℓ
-  hasExponentials = record { exponent = :exponent: }
+  hasExponentials = record { exponent = exponent }
diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda
index fdee75e..00f10e3 100644
--- a/src/Cat/Categories/Cube.agda
+++ b/src/Cat/Categories/Cube.agda
@@ -26,24 +26,24 @@ open Category hiding (_∘_)
 open Functor
 
 module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
-  -- Ns is the "namespace"
-  ℓo = (suc zero ⊔ ℓ)
+  private
+    -- Ns is the "namespace"
+    ℓo = (suc zero ⊔ ℓ)
 
-  FiniteDecidableSubset : Set ℓ
-  FiniteDecidableSubset = Ns → Dec ⊤
+    FiniteDecidableSubset : Set ℓ
+    FiniteDecidableSubset = Ns → Dec ⊤
 
-  isTrue : Bool → Set
-  isTrue false = ⊥
-  isTrue true = ⊤
+    isTrue : Bool → Set
+    isTrue false = ⊥
+    isTrue true = ⊤
 
-  elmsof : FiniteDecidableSubset → Set ℓ
-  elmsof P = Σ Ns (λ σ → True (P σ)) -- (σ : Ns) → isTrue (P σ)
+    elmsof : FiniteDecidableSubset → Set ℓ
+    elmsof P = Σ Ns (λ σ → True (P σ)) -- (σ : Ns) → isTrue (P σ)
 
-  𝟚 : Set
-  𝟚 = Bool
+    𝟚 : Set
+    𝟚 = Bool
 
-  module _ (I J : FiniteDecidableSubset) where
-    private
+    module _ (I J : FiniteDecidableSubset) where
       Hom' : Set ℓ
       Hom' = elmsof I → elmsof J ⊎ 𝟚
       isInl : {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} → A ⊎ B → Set
@@ -63,18 +63,18 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
           ; (inj₂ _) → Lift ⊤
           }
 
-    Hom = Σ Hom' rules
+      Hom = Σ Hom' rules
 
-  module Raw = RawCategory
-  -- The category of names and substitutions
-  Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
-  Raw.Object Rawℂ = FiniteDecidableSubset
-  Raw.Arrow Rawℂ = Hom
-  Raw.𝟙 Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} }
-  Raw._∘_ Rawℂ = {!!}
+    module Raw = RawCategory
+    -- The category of names and substitutions
+    Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
+    Raw.Object Rawℂ = FiniteDecidableSubset
+    Raw.Arrow Rawℂ = Hom
+    Raw.𝟙 Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} }
+    Raw._∘_ Rawℂ = {!!}
 
-  postulate IsCategoryℂ : IsCategory Rawℂ
+    postulate IsCategoryℂ : IsCategory Rawℂ
 
-  ℂ : Category ℓ ℓ
-  raw ℂ = Rawℂ
-  isCategory ℂ = IsCategoryℂ
+    ℂ : Category ℓ ℓ
+    raw ℂ = Rawℂ
+    isCategory ℂ = IsCategoryℂ
diff --git a/src/Cat/Categories/CwF.agda b/src/Cat/Categories/CwF.agda
index 4b9ce32..ea369ef 100644
--- a/src/Cat/Categories/CwF.agda
+++ b/src/Cat/Categories/CwF.agda
@@ -28,20 +28,20 @@ module _ {ℓa ℓb : Level} where
     private
       module T = Functor T
     Type : (Γ : Object ℂ) → Set ℓa
-    Type Γ = proj₁ (proj₁ (T.func* Γ))
+    Type Γ = proj₁ (proj₁ (T.omap Γ))
 
     module _ {Γ : Object ℂ} {A : Type Γ} where
 
       -- module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
-      --   k : Σ (proj₁ (func* T B) → proj₁ (func* T A))
+      --   k : Σ (proj₁ (omap T B) → proj₁ (omap T A))
       --     (λ f →
-      --     {x : proj₁ (func* T B)} →
-      --     proj₂ (func* T B) x → proj₂ (func* T A) (f x))
-      --   k = T.func→ γ
-      --   k₁ : proj₁ (func* T B) → proj₁ (func* T A)
+      --     {x : proj₁ (omap T B)} →
+      --     proj₂ (omap T B) x → proj₂ (omap T A) (f x))
+      --   k = T.fmap γ
+      --   k₁ : proj₁ (omap T B) → proj₁ (omap T A)
       --   k₁ = proj₁ k
-      --   k₂ : ({x : proj₁ (func* T B)} →
-      --     proj₂ (func* T B) x → proj₂ (func* T A) (k₁ x))
+      --   k₂ : ({x : proj₁ (omap T B)} →
+      --     proj₂ (omap T B) x → proj₂ (omap T A) (k₁ x))
       --   k₂ = proj₂ k
 
       record ContextComprehension : Set (ℓa ⊔ ℓb) where
@@ -51,7 +51,7 @@ module _ {ℓa ℓb : Level} where
           -- proj2 : ????
 
         -- if γ : ℂ [ A , B ]
-        -- then T .func→ γ (written T[γ]) interpret substitutions in types and terms respectively.
+        -- then T .fmap γ (written T[γ]) interpret substitutions in types and terms respectively.
         -- field
         --   ump : {Δ : ℂ .Object} → (γ : ℂ [ Δ , Γ ])
         --     → (a : {!!}) → {!!}
diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda
index 9a0c891..7e80478 100644
--- a/src/Cat/Categories/Free.agda
+++ b/src/Cat/Categories/Free.agda
@@ -20,10 +20,10 @@ singleton : ∀ {ℓ} {𝓤 : Set ℓ} {ℓr} {R : 𝓤 → 𝓤 → Set ℓr} {
 singleton f = cons f empty
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-  module ℂ = Category ℂ
-  open Category ℂ
-
   private
+    module ℂ = Category ℂ
+    open Category ℂ
+
     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-isAssociative {r = r} {q} {empty} = refl
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 2af9e55..019e8b6 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -4,50 +4,24 @@ module Cat.Categories.Fun where
 open import Agda.Primitive
 open import Data.Product
 
-open import Data.Nat using (_≤_ ; z≤n ; s≤s)
-module Nat = Data.Nat
-open import Data.Product
 
 open import Cubical
-open import Cubical.Sigma
+open import Cubical.GradLemma
 open import Cubical.NType.Properties
 
 open import Cat.Category
 open import Cat.Category.Functor hiding (identity)
 open import Cat.Category.NaturalTransformation
-open import Cat.Wishlist
-
-open import Cat.Equality
-import Cat.Category.NaturalTransformation
-open Equality.Data.Product
 
 module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
-  open Category using (Object ; 𝟙)
   module NT = NaturalTransformation ℂ 𝔻
   open NT public
-
   private
+    module ℂ = Category ℂ
     module 𝔻 = Category 𝔻
-
-  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 → 𝔻.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 θ)
-
-  module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B}
-    {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
-    private
+  private
+    module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B}
+      {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
       θ = proj₁ θ'
       η = proj₁ η'
       ζ = proj₁ ζ'
@@ -58,13 +32,11 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
       L = (NT[_∘_] {A} {C} {D} ζ' (NT[_∘_] {A} {B} {C} η' θ'))
       R : NaturalTransformation A D
       R = (NT[_∘_] {A} {B} {D} (NT[_∘_] {B} {C} {D} ζ' η') θ')
-    _g⊕f_ = NT[_∘_] {A} {B} {C}
-    _h⊕g_ = NT[_∘_] {B} {C} {D}
-    :isAssociative: : L ≡ R
-    :isAssociative: = lemSig (naturalIsProp {F = A} {D})
-      L R (funExt (λ x → isAssociative))
-      where
-        open Category 𝔻
+      _g⊕f_ = NT[_∘_] {A} {B} {C}
+      _h⊕g_ = NT[_∘_] {B} {C} {D}
+      isAssociative : L ≡ R
+      isAssociative = lemSig (naturalIsProp {F = A} {D})
+        L R (funExt (λ x → 𝔻.isAssociative))
 
   private
     module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
@@ -94,27 +66,120 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
     ; _∘_ = λ {F G H} → NT[_∘_] {F} {G} {H}
     }
 
+  open RawCategory RawFun
+  open Univalence  RawFun
+  module _ {A B : Functor ℂ 𝔻} where
+    module A = Functor A
+    module B = Functor B
+    module _ (p : A ≡ B) where
+      omapP : A.omap ≡ B.omap
+      omapP i = Functor.omap (p i)
+
+      coerceAB : ∀ {X} → 𝔻 [ A.omap X , A.omap X ] ≡ 𝔻 [ A.omap X , B.omap X ]
+      coerceAB {X} = cong (λ φ → 𝔻 [ A.omap X , φ X ]) omapP
+
+      -- The transformation will be the identity on 𝔻. Such an arrow has the
+      -- type `A.omap A → A.omap A`. Which we can coerce to have the type
+      -- `A.omap → B.omap` since `A` and `B` are equal.
+      coe𝟙 : Transformation A B
+      coe𝟙 X = coe coerceAB 𝔻.𝟙
+
+      module _ {a b : ℂ.Object} (f : ℂ [ a , b ]) where
+        nat' : 𝔻 [ coe𝟙 b ∘ A.fmap f ] ≡ 𝔻 [ B.fmap f ∘ coe𝟙 a ]
+        nat' = begin
+          (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡⟨ {!!} ⟩
+          (𝔻 [ B.fmap f ∘ coe𝟙 a ]) ∎
+
+      transs : (i : I) → Transformation A (p i)
+      transs = {!!}
+
+      natt : (i : I) → Natural A (p i) {!!}
+      natt = {!!}
+
+      t : Natural A B coe𝟙
+      t = coe c (identityNatural A)
+        where
+        c : Natural A A (identityTrans A) ≡ Natural A B coe𝟙
+        c = begin
+          Natural A A (identityTrans A) ≡⟨ (λ x → {!natt ?!}) ⟩
+          Natural A B coe𝟙 ∎
+        -- cong (λ φ → {!Natural A A (identityTrans A)!}) {!!}
+
+      k : Natural A A (identityTrans A) → Natural A B coe𝟙
+      k n {a} {b} f = res
+        where
+        res : (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡ (𝔻 [ B.fmap f ∘ coe𝟙 a ])
+        res = {!!}
+
+      nat : Natural A B coe𝟙
+      nat = nat'
+
+      fromEq : NaturalTransformation A B
+      fromEq = coe𝟙 , nat
+
+  module _ {A B : Functor ℂ 𝔻} where
+    obverse : A ≡ B → A ≅ B
+    obverse p = res
+      where
+      ob  : Arrow A B
+      ob = fromEq p
+      re : Arrow B A
+      re = fromEq (sym p)
+      vr : _∘_ {A = A} {B} {A} re ob ≡ 𝟙 {A}
+      vr = {!!}
+      rv : _∘_ {A = B} {A} {B} ob re ≡ 𝟙 {B}
+      rv = {!!}
+      isInverse : IsInverseOf {A} {B} ob re
+      isInverse = vr , rv
+      iso : Isomorphism {A} {B} ob
+      iso = re , isInverse
+      res : A ≅ B
+      res = ob , iso
+
+    reverse : A ≅ B → A ≡ B
+    reverse iso = {!!}
+
+    ve-re : (y : A ≅ B) → obverse (reverse y) ≡ y
+    ve-re = {!!}
+
+    re-ve : (x : A ≡ B) → reverse (obverse x) ≡ x
+    re-ve = {!!}
+
+    done : isEquiv (A ≡ B) (A ≅ B) (id-to-iso (λ { {A} {B} → isIdentity {A} {B}}) A B)
+    done = {!gradLemma obverse reverse ve-re re-ve!}
+
+  univalent : Univalent (λ{ {A} {B} → isIdentity {A} {B}})
+  univalent = done
+
   instance
-    :isCategory: : IsCategory RawFun
-    :isCategory: = record
-      { isAssociative = λ {A B C D} → :isAssociative: {A} {B} {C} {D}
+    isCategory : IsCategory RawFun
+    isCategory = record
+      { isAssociative = λ {A B C D} → isAssociative {A} {B} {C} {D}
       ; isIdentity = λ {A B} → isIdentity {A} {B}
-      ; arrowsAreSets = λ {F} {G} → naturalTransformationIsSets {F} {G}
-      ; univalent = {!!}
+      ; arrowsAreSets = λ {F} {G} → naturalTransformationIsSet {F} {G}
+      ; univalent = univalent
       }
 
   Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
   Category.raw Fun = RawFun
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-  open import Cat.Categories.Sets
-  open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
+  private
+    open import Cat.Categories.Sets
+    open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
 
-  -- Restrict the functors to Presheafs.
-  RawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
-  RawPresh = record
-    { Object = Presheaf ℂ
-    ; Arrow = NaturalTransformation
-    ; 𝟙 = λ {F} → identity F
-    ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
-    }
+    -- Restrict the functors to Presheafs.
+    rawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
+    rawPresh = record
+      { Object = Presheaf ℂ
+      ; Arrow = NaturalTransformation
+      ; 𝟙 = λ {F} → identity F
+      ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
+      }
+    instance
+      isCategory : IsCategory rawPresh
+      isCategory = Fun.isCategory _ _
+
+  Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
+  Category.raw        Presh = rawPresh
+  Category.isCategory Presh = isCategory
diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index de3d1f2..1dbed3d 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -56,7 +56,6 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where
       backwards (a' , (a=a' , a'b∈S)) = subst (sym a=a') a'b∈S
 
       fwd-bwd : (x : (a , b) ∈ S) → (backwards ∘ forwards) x ≡ x
-      -- isbijective x = pathJ (λ y x₁ → (backwards ∘ forwards) x ≡ x) {!!} {!!} {!!}
       fwd-bwd x = pathJprop (λ y _ → y) x
 
       bwd-fwd : (x : Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 0ed99a3..a329a0f 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -1,35 +1,172 @@
+-- | The category of homotopy sets
 {-# OPTIONS --allow-unsolved-metas --cubical #-}
 module Cat.Categories.Sets where
 
-open import Cubical
 open import Agda.Primitive
 open import Data.Product
-import Function
+open import Function using (_∘_)
+
+open import Cubical hiding (_≃_ ; inverse)
+open import Cubical.Equivalence
+  renaming
+    ( _≅_ to _A≅_ )
+  using
+    (_≃_ ; con ; AreInverses)
+open import Cubical.Univalence
+open import Cubical.GradLemma
 
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
+open import Cat.Wishlist
 
 module _ (ℓ : Level) where
   private
-    open RawCategory
-    open IsCategory
     open import Cubical.Univalence
     open import Cubical.NType.Properties
     open import Cubical.Universe
 
     SetsRaw : RawCategory (lsuc ℓ) ℓ
-    Object SetsRaw = hSet
-    Arrow SetsRaw (T , _) (U , _) = T → U
-    𝟙 SetsRaw = Function.id
-    _∘_ SetsRaw = Function._∘′_
+    RawCategory.Object SetsRaw = hSet
+    RawCategory.Arrow  SetsRaw (T , _) (U , _) = T → U
+    RawCategory.𝟙      SetsRaw = Function.id
+    RawCategory._∘_    SetsRaw = Function._∘′_
+
+    open RawCategory SetsRaw hiding (_∘_)
+    open Univalence  SetsRaw
+
+    isIdentity : IsIdentity Function.id
+    proj₁ isIdentity = funExt λ _ → refl
+    proj₂ isIdentity = funExt λ _ → refl
+
+    arrowsAreSets : ArrowsAreSets
+    arrowsAreSets {B = (_ , s)} = setPi λ _ → s
+
+    module _ {hA hB : Object} where
+      private
+        A = proj₁ hA
+        isSetA : isSet A
+        isSetA = proj₂ hA
+        B = proj₁ hB
+        isSetB : isSet B
+        isSetB = proj₂ hB
+
+        toIsomorphism : A ≃ B → hA ≅ hB
+        toIsomorphism e = obverse , inverse , verso-recto , recto-verso
+          where
+          open _≃_ e
+
+        fromIsomorphism : hA ≅ hB → A ≃ B
+        fromIsomorphism iso = con obverse (gradLemma obverse inverse recto-verso verso-recto)
+          where
+          obverse : A → B
+          obverse = proj₁ iso
+          inverse : B → A
+          inverse = proj₁ (proj₂ iso)
+          -- FIXME IsInverseOf should change name to AreInverses and the
+          -- ordering should be swapped.
+          areInverses : IsInverseOf {A = hA} {hB} obverse inverse
+          areInverses = proj₂ (proj₂ iso)
+          verso-recto : ∀ a → (inverse ∘ obverse) a ≡ a
+          verso-recto a i = proj₁ areInverses i a
+          recto-verso : ∀ b → (obverse Function.∘ inverse) b ≡ b
+          recto-verso b i = proj₂ areInverses i b
+
+      private
+        univIso : (A ≡ B) A≅ (A ≃ B)
+        univIso = _≃_.toIsomorphism univalence
+        obverse' : A ≡ B → A ≃ B
+        obverse' = proj₁ univIso
+        inverse' : A ≃ B → A ≡ B
+        inverse' = proj₁ (proj₂ univIso)
+        -- Drop proof of being a set from both sides of an equality.
+        dropP : hA ≡ hB → A ≡ B
+        dropP eq i = proj₁ (eq i)
+        -- Add proof of being a set to both sides of a set-theoretic equivalence
+        -- returning a category-theoretic equivalence.
+        addE : A A≅ B → hA ≅ hB
+        addE eqv = proj₁ eqv , (proj₁ (proj₂ eqv)) , asPair
+          where
+          areeqv = proj₂ (proj₂ eqv)
+          asPair =
+            let module Inv = AreInverses areeqv
+            in Inv.verso-recto , Inv.recto-verso
+
+        obverse : hA ≡ hB → hA ≅ hB
+        obverse = addE ∘ _≃_.toIsomorphism ∘ obverse' ∘ dropP
+
+        -- Drop proof of being a set form both sides of a category-theoretic
+        -- equivalence returning a set-theoretic equivalence.
+        dropE : hA ≅ hB → A A≅ B
+        dropE eqv = obv , inv , asAreInverses
+          where
+          obv = proj₁ eqv
+          inv = proj₁ (proj₂ eqv)
+          areEq = proj₂ (proj₂ eqv)
+          asAreInverses : AreInverses A B obv inv
+          asAreInverses = record { verso-recto = proj₁ areEq ; recto-verso = proj₂ areEq }
+
+        -- Dunno if this is a thing.
+        isoToEquiv : A A≅ B → A ≃ B
+        isoToEquiv = {!!}
+        -- Add proof of being a set to both sides of an equality.
+        addP : A ≡ B → hA ≡ hB
+        addP p = lemSig (λ X → propPi λ x → propPi (λ y → propIsProp)) hA hB p
+        inverse : hA ≅ hB → hA ≡ hB
+        inverse = addP ∘ inverse' ∘ isoToEquiv ∘ dropE
+
+        -- open AreInverses (proj₂ (proj₂ univIso)) renaming
+        --   ( verso-recto to verso-recto'
+        --   ; recto-verso to recto-verso'
+        --   )
+        -- I can just open them but I wanna be able to see the type annotations.
+        verso-recto' : inverse' ∘ obverse' ≡ Function.id
+        verso-recto' = AreInverses.verso-recto (proj₂ (proj₂ univIso))
+        recto-verso' : obverse' ∘ inverse' ≡ Function.id
+        recto-verso' = AreInverses.recto-verso (proj₂ (proj₂ univIso))
+        verso-recto : (iso : hA ≅ hB) → obverse (inverse iso) ≡ iso
+        verso-recto iso = begin
+          obverse (inverse iso) ≡⟨⟩
+          ( addE ∘ _≃_.toIsomorphism
+          ∘ obverse' ∘ dropP ∘ addP
+          ∘ inverse' ∘ isoToEquiv
+          ∘ dropE) iso
+            ≡⟨⟩
+          ( addE ∘ _≃_.toIsomorphism
+          ∘ obverse'
+          ∘ inverse' ∘ isoToEquiv
+          ∘ dropE) iso
+            ≡⟨ {!!} ⟩ -- obverse' inverse' are inverses
+          ( addE ∘ _≃_.toIsomorphism ∘ isoToEquiv ∘ dropE) iso
+            ≡⟨ {!!} ⟩ -- should be easy to prove
+                      -- _≃_.toIsomorphism ∘ isoToEquiv ≡ id
+          (addE ∘ dropE) iso
+            ≡⟨⟩
+          iso ∎
+
+        -- Similar to above.
+        recto-verso : (eq : hA ≡ hB) → inverse (obverse eq) ≡ eq
+        recto-verso eq = begin
+          inverse (obverse eq) ≡⟨ {!!} ⟩
+          eq ∎
+
+        -- Use the fact that being an h-level is a mere proposition.
+        -- This is almost provable using `Wishlist.isSetIsProp` - although
+        -- this creates homogenous paths.
+        isSetEq : (p : A ≡ B) → (λ i → isSet (p i)) [ isSetA ≡ isSetB ]
+        isSetEq = {!!}
+
+        res : hA ≡ hB
+        proj₁ (res i) = {!!}
+        proj₂ (res i) = isSetEq {!!} i
+      univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)
+      univalent = {!gradLemma obverse inverse verso-recto recto-verso!}
 
     SetsIsCategory : IsCategory SetsRaw
-    isAssociative SetsIsCategory = refl
-    proj₁ (isIdentity SetsIsCategory) = funExt λ _ → refl
-    proj₂ (isIdentity SetsIsCategory) = funExt λ _ → refl
-    arrowsAreSets SetsIsCategory {B = (_ , s)} = setPi λ _ → s
-    univalent SetsIsCategory = {!!}
+    IsCategory.isAssociative SetsIsCategory = refl
+    IsCategory.isIdentity    SetsIsCategory {A} {B} = isIdentity    {A} {B}
+    IsCategory.arrowsAreSets SetsIsCategory {A} {B} = arrowsAreSets {A} {B}
+    IsCategory.univalent     SetsIsCategory = univalent
 
   𝓢𝓮𝓽 Sets : Category (lsuc ℓ) ℓ
   Category.raw 𝓢𝓮𝓽 = SetsRaw
@@ -64,58 +201,57 @@ module _ {ℓ : Level} where
             lem : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g
             proj₁ lem = refl
             proj₂ lem = refl
-        instance
-          isProduct : IsProduct 𝓢 {0A} {0B} {0A×0B} proj₁ proj₂
-          isProduct {X = X} f g = (f &&& g) , lem {0X = X} f g
 
-      product : Product {ℂ = 𝓢} 0A 0B
-      product = record
-        { obj = 0A×0B
-        ; proj₁ = Data.Product.proj₁
-        ; proj₂ = Data.Product.proj₂
-        ; isProduct = λ { {X} → isProduct {X = X}}
-        }
+        rawProduct : RawProduct 𝓢 0A 0B
+        RawProduct.object rawProduct = 0A×0B
+        RawProduct.proj₁  rawProduct = Data.Product.proj₁
+        RawProduct.proj₂  rawProduct = Data.Product.proj₂
+
+        isProduct : IsProduct 𝓢 _ _ rawProduct
+        IsProduct.isProduct isProduct {X = X} f g
+          = (f &&& g) , lem {0X = X} f g
+
+      product : Product 𝓢 0A 0B
+      Product.raw       product = rawProduct
+      Product.isProduct product = isProduct
 
   instance
     SetsHasProducts : HasProducts 𝓢
     SetsHasProducts = record { product = product }
 
-module _ {ℓa ℓb : Level} where
-  module _ (ℂ : Category ℓa ℓb) where
-    -- Covariant Presheaf
-    Representable : Set (ℓa ⊔ lsuc ℓb)
-    Representable = Functor ℂ (𝓢𝓮𝓽 ℓb)
+module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  -- Covariant Presheaf
+  Representable : Set (ℓa ⊔ lsuc ℓb)
+  Representable = Functor ℂ (𝓢𝓮𝓽 ℓb)
 
-    -- Contravariant Presheaf
-    Presheaf : Set (ℓa ⊔ lsuc ℓb)
-    Presheaf = Functor (opposite ℂ) (𝓢𝓮𝓽 ℓb)
+  -- Contravariant Presheaf
+  Presheaf : Set (ℓa ⊔ lsuc ℓb)
+  Presheaf = Functor (opposite ℂ) (𝓢𝓮𝓽 ℓb)
+
+  open Category ℂ
 
   -- The "co-yoneda" embedding.
-  representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
-  representable {ℂ = ℂ} A = record
+  representable : Category.Object ℂ → Representable
+  representable A = record
     { raw = record
-      { func* = λ B → ℂ [ A , B ] , arrowsAreSets
-      ; func→ = ℂ [_∘_]
+      { omap = λ B → ℂ [ A , B ] , arrowsAreSets
+      ; fmap = ℂ [_∘_]
       }
     ; isFunctor = record
       { isIdentity = funExt λ _ → proj₂ isIdentity
       ; isDistributive = funExt λ x → sym isAssociative
       }
     }
-    where
-      open Category ℂ
 
   -- Alternate name: `yoneda`
-  presheaf : {ℂ : Category ℓa ℓb} → Category.Object (opposite ℂ) → Presheaf ℂ
-  presheaf {ℂ = ℂ} B = record
+  presheaf : Category.Object (opposite ℂ) → Presheaf
+  presheaf B = record
     { raw = record
-      { func* = λ A → ℂ [ A , B ] , arrowsAreSets
-      ; func→ = λ f g → ℂ [ g ∘ f ]
+      { omap = λ A → ℂ [ A , B ] , arrowsAreSets
+      ; fmap = λ f g → ℂ [ g ∘ f ]
     }
     ; isFunctor = record
       { isIdentity = funExt λ x → proj₁ isIdentity
       ; isDistributive = funExt λ x → isAssociative
       }
     }
-    where
-      open Category ℂ
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index d70fc65..5b2f025 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -24,9 +24,6 @@
 -- ------
 --
 -- Propositionality for all laws about the category.
---
--- TODO: An equality principle for categories that focuses on the pure data-part.
---
 {-# OPTIONS --allow-unsolved-metas --cubical #-}
 
 module Cat.Category where
@@ -41,7 +38,7 @@ open import Data.Product renaming
 open import Data.Empty
 import Function
 open import Cubical
-open import Cubical.NType.Properties using ( propIsEquiv )
+open import Cubical.NType.Properties using ( propIsEquiv ; lemPropF )
 
 open import Cat.Wishlist
 
@@ -76,7 +73,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     𝟙      : {A : Object} → Arrow A A
     _∘_    : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
 
-  infixl 10 _∘_
+  infixl 10 _∘_ _>>>_
 
   -- | Operations on data
 
@@ -86,9 +83,12 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   codomain : { a b : Object } → Arrow a b → Object
   codomain {b = b} _ = b
 
+  _>>>_ : {A B C : Object} → (Arrow A B) → (Arrow B C) → Arrow A C
+  f >>> g = g ∘ f
+
   -- | Laws about the data
 
-  -- TODO: It seems counter-intuitive that the normal-form is on the
+  -- FIXME It seems counter-intuitive that the normal-form is on the
   -- right-hand-side.
   IsAssociative : Set (ℓa ⊔ ℓb)
   IsAssociative = ∀ {A B C D} {f : Arrow A B} {g : Arrow B C} {h : Arrow C D}
@@ -129,7 +129,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   Terminal : Set (ℓa ⊔ ℓb)
   Terminal = Σ Object IsTerminal
 
--- Univalence is indexed by a raw category as well as an identity proof.
+-- | Univalence is indexed by a raw category as well as an identity proof.
+--
+-- FIXME Put this in `RawCategory` and index it on the witness to `isIdentity`.
 module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   open RawCategory ℂ
   module _ (isIdentity : IsIdentity 𝟙) where
@@ -150,9 +152,11 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
 --     iso-is-epi  : Isomorphism f → Epimorphism {X = X} f
 --     iso-is-mono : Isomorphism f → Monomorphism {X = X} f
 --
+-- Sans `univalent` this would be what is referred to as a pre-category in
+-- [HoTT].
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
   open RawCategory ℂ public
-  open Univalence ℂ public
+  open Univalence  ℂ public
   field
     isAssociative : IsAssociative
     isIdentity    : IsIdentity 𝟙
@@ -191,9 +195,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
 --
 -- Proves that all projections of `IsCategory` are mere propositions as well as
 -- `IsCategory` itself being a mere proposition.
-module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
-  open RawCategory C
-  module _ (ℂ : IsCategory C) where
+module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
+  open RawCategory ℂ
+  module _ (ℂ : IsCategory ℂ) where
     open IsCategory ℂ using (isAssociative ; arrowsAreSets ; isIdentity ; Univalent)
     open import Cubical.NType
     open import Cubical.NType.Properties
@@ -237,52 +241,71 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
     propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
 
   private
-    module _ (x y : IsCategory C) where
+    module _ (x y : IsCategory ℂ) where
       module IC = IsCategory
       module X = IsCategory x
       module Y = IsCategory y
-      open Univalence C
+      open Univalence ℂ
       -- In a few places I use the result of propositionality of the various
       -- 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.
       isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ]
       isIdentity = propIsIdentity x X.isIdentity Y.isIdentity
-      done : x ≡ y
       U : ∀ {a : IsIdentity 𝟙}
         → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ]
         → (b : Univalent a)
         → Set _
-      U eqwal bbb =
+      U eqwal univ =
         (λ i → Univalent (eqwal i))
-        [ X.univalent ≡ bbb ]
+        [ X.univalent ≡ univ ]
       P : (y : IsIdentity 𝟙)
         → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ y ] → Set _
-      P y eq = ∀ (b' : Univalent y) → U eq b'
-      helper : ∀ (b' : Univalent X.isIdentity)
+      P y eq = ∀ (univ : Univalent y) → U eq univ
+      p : ∀ (b' : Univalent X.isIdentity)
         → (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ]
-      helper univ = propUnivalent x X.univalent univ
-      foo = pathJ P helper Y.isIdentity isIdentity
+      p univ = propUnivalent x X.univalent univ
+      helper : P Y.isIdentity isIdentity
+      helper = pathJ P p Y.isIdentity isIdentity
       eqUni : U isIdentity Y.univalent
-      eqUni = foo Y.univalent
-      IC.isAssociative      (done i) = propIsAssociative x X.isAssociative Y.isAssociative i
-      IC.isIdentity      (done i) = isIdentity i
+      eqUni = helper Y.univalent
+      done : x ≡ y
+      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
+      IC.univalent     (done i) = eqUni i
 
-  propIsCategory : isProp (IsCategory C)
+  propIsCategory : isProp (IsCategory ℂ)
   propIsCategory = done
 
 -- | Univalent categories
 --
--- Just bundles up the data with witnesses inhabting the propositions.
+-- Just bundles up the data with witnesses inhabiting the propositions.
 record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   field
-    raw : RawCategory ℓa ℓb
+    raw            : RawCategory ℓa ℓb
     {{isCategory}} : IsCategory raw
 
   open IsCategory isCategory public
 
+-- The fact that being a category is a mere proposition gives rise to this
+-- equality principle for categories.
+module _ {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} where
+  private
+    module ℂ = Category ℂ
+    module 𝔻 = Category 𝔻
+
+  module _ (rawEq : ℂ.raw ≡ 𝔻.raw) where
+    private
+      isCategoryEq : (λ i → IsCategory (rawEq i)) [ ℂ.isCategory ≡ 𝔻.isCategory ]
+      isCategoryEq = lemPropF Propositionality.propIsCategory rawEq
+
+    Category≡ : ℂ ≡ 𝔻
+    Category≡ i = record
+      { raw        = rawEq i
+      ; isCategory = isCategoryEq i
+      }
+
 -- | Syntax for arrows- and composition in a given category.
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   open Category ℂ
@@ -298,23 +321,42 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 -- flipped.
 module Opposite {ℓa ℓb : Level} where
   module _ (ℂ : Category ℓa ℓb) where
-    open Category ℂ
     private
+      module ℂ = Category ℂ
       opRaw : RawCategory ℓa ℓb
-      RawCategory.Object opRaw = Object
-      RawCategory.Arrow  opRaw = Function.flip Arrow
-      RawCategory.𝟙      opRaw = 𝟙
-      RawCategory._∘_    opRaw = Function.flip _∘_
+      RawCategory.Object opRaw = ℂ.Object
+      RawCategory.Arrow  opRaw = Function.flip ℂ.Arrow
+      RawCategory.𝟙      opRaw = ℂ.𝟙
+      RawCategory._∘_    opRaw = Function.flip ℂ._∘_
 
-      opIsCategory : IsCategory opRaw
-      IsCategory.isAssociative opIsCategory = sym isAssociative
-      IsCategory.isIdentity    opIsCategory = swap isIdentity
-      IsCategory.arrowsAreSets opIsCategory = arrowsAreSets
-      IsCategory.univalent     opIsCategory = {!!}
+      open RawCategory opRaw
+      open Univalence  opRaw
+
+      isIdentity : IsIdentity 𝟙
+      isIdentity = swap ℂ.isIdentity
+
+      module _ {A B : ℂ.Object} where
+        univalent : isEquiv (A ≡ B) (A ≅ B)
+          (id-to-iso (swap ℂ.isIdentity) A B)
+        fst (univalent iso) = flipFiber (fst (ℂ.univalent (flipIso iso)))
+          where
+            flipIso : A ≅ B → B ℂ.≅ A
+            flipIso (f , f~ , iso) = f , f~ , swap iso
+            flipFiber
+              : fiber (ℂ.id-to-iso ℂ.isIdentity B A) (flipIso iso)
+              → fiber (  id-to-iso   isIdentity A B)          iso
+            flipFiber (eq , eqIso) = sym eq , {!!}
+        snd (univalent iso) = {!!}
+
+      isCategory : IsCategory opRaw
+      IsCategory.isAssociative isCategory = sym ℂ.isAssociative
+      IsCategory.isIdentity    isCategory = isIdentity
+      IsCategory.arrowsAreSets isCategory = ℂ.arrowsAreSets
+      IsCategory.univalent     isCategory = univalent
 
     opposite : Category ℓa ℓb
-    raw opposite = opRaw
-    Category.isCategory opposite = opIsCategory
+    Category.raw        opposite = opRaw
+    Category.isCategory opposite = isCategory
 
   -- As demonstrated here a side-effect of having no-eta-equality on constructors
   -- means that we need to pick things apart to show that things are indeed
@@ -331,9 +373,7 @@ module Opposite {ℓa ℓb : Level} where
       RawCategory.𝟙        (rawInv _) = 𝟙
       RawCategory._∘_      (rawInv _) = _∘_
 
-    -- TODO: Define and use Monad≡
     oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ
-    Category.raw        (oppositeIsInvolution i) = rawInv i
-    Category.isCategory (oppositeIsInvolution x) = {!!}
+    oppositeIsInvolution = Category≡ rawInv
 
 open Opposite public
diff --git a/src/Cat/Category/Exponential.agda b/src/Cat/Category/Exponential.agda
index 1e443ce..87769f6 100644
--- a/src/Cat/Category/Exponential.agda
+++ b/src/Cat/Category/Exponential.agda
@@ -1,40 +1,44 @@
 module Cat.Category.Exponential where
 
 open import Agda.Primitive
-open import Data.Product
+open import Data.Product hiding (_×_)
 open import Cubical
 
 open import Cat.Category
 open import Cat.Category.Product
 
-open Category
-
 module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} where
-  open HasProducts hasProducts
-  open Product hiding (obj)
-  private
-    _×p_ : (A B : Object ℂ) → Object ℂ
-    _×p_ A B = Product.obj (product A B)
+  open Category ℂ
+  open HasProducts hasProducts public
 
-  module _ (B C : Object ℂ) where
-    IsExponential : (Cᴮ : Object ℂ) → ℂ [ Cᴮ ×p B , C ] → Set (ℓ ⊔ ℓ')
-    IsExponential Cᴮ eval = ∀ (A : Object ℂ) (f : ℂ [ A ×p B , C ])
+  module _ (B C : Object) where
+    record IsExponential'
+      (Cᴮ : Object)
+      (eval : ℂ [ Cᴮ × B , C ]) : Set (ℓ ⊔ ℓ') where
+      field
+        uniq
+          : ∀ (A : Object) (f : ℂ [ A × B , C ])
+          → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f)
+
+    IsExponential : (Cᴮ : Object) → ℂ [ Cᴮ × B , C ] → Set (ℓ ⊔ ℓ')
+    IsExponential Cᴮ eval = ∀ (A : Object) (f : ℂ [ A × B , C ])
       → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f)
 
     record Exponential : Set (ℓ ⊔ ℓ') where
       field
         -- obj ≡ Cᴮ
-        obj : Object ℂ
-        eval : ℂ [ obj ×p B , C ]
+        obj : Object
+        eval : ℂ [ obj × B , C ]
         {{isExponential}} : IsExponential obj eval
-      -- If I make this an instance-argument then the instance resolution
-      -- algorithm goes into an infinite loop. Why?
-      exponentialsHaveProducts : HasProducts ℂ
-      exponentialsHaveProducts = hasProducts
-      transpose : (A : Object ℂ) → ℂ [ A ×p B , C ] → ℂ [ A , obj ]
+
+      transpose : (A : Object) → ℂ [ A × B , C ] → ℂ [ A , obj ]
       transpose A f = proj₁ (isExponential A f)
 
 record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where
+  open Category ℂ
   open Exponential public
   field
-    exponent : (A B : Object ℂ) → Exponential ℂ A B
+    exponent : (A B : Object) → Exponential ℂ A B
+
+  _⇑_ : (A B : Object) → Object
+  A ⇑ B = (exponent A B) .obj
diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index d648728..fc23c2e 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -18,21 +18,50 @@ module _ {ℓc ℓc' ℓd ℓd'}
     ℓ = ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd'
     𝓤 = Set ℓ
 
+  Omap = Object ℂ → Object 𝔻
+  Fmap : Omap → Set _
+  Fmap omap = ∀ {A B}
+    → ℂ [ A , B ] → 𝔻 [ omap A , omap B ]
   record RawFunctor : 𝓤 where
     field
-      func* : Object ℂ → Object 𝔻
-      func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
+      omap : Object ℂ → Object 𝔻
+      fmap : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ omap A , omap B ]
 
     IsIdentity : Set _
-    IsIdentity = {A : Object ℂ} → func→ (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {func* A}
+    IsIdentity = {A : Object ℂ} → fmap (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {omap A}
 
     IsDistributive : Set _
     IsDistributive = {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
-      → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ]
+      → fmap (ℂ [ g ∘ f ]) ≡ 𝔻 [ fmap g ∘ fmap f ]
+
+  -- | Equality principle for raw functors
+  --
+  -- The type of `fmap` depend on the value of `omap`. We can wrap this up
+  -- into an equality principle for this type like is done for e.g. `Σ` using
+  -- `pathJ`.
+  module _ {x y : RawFunctor} where
+    open RawFunctor
+    private
+      P : (omap' : Omap) → (eq : omap x ≡ omap') → Set _
+      P y eq = (fmap' : Fmap y) → (λ i → Fmap (eq i))
+        [ fmap x ≡ fmap' ]
+    module _
+        (eq : (λ i → Omap) [ omap x ≡ omap y ])
+        (kk : P (omap x) refl)
+        where
+      private
+        p : P (omap y) eq
+        p = pathJ P kk (omap y) eq
+        eq→ : (λ i → Fmap (eq i)) [ fmap x ≡ fmap y ]
+        eq→ = p (fmap y)
+      RawFunctor≡ : x ≡ y
+      omap (RawFunctor≡ i) = eq  i
+      fmap (RawFunctor≡ i) = eq→ i
 
   record IsFunctor (F : RawFunctor) : 𝓤 where
     open RawFunctor F public
     field
+      -- FIXME Really ought to be preserves identity or something like this.
       isIdentity : IsIdentity
       isDistributive : IsDistributive
 
@@ -45,6 +74,9 @@ module _ {ℓc ℓc' ℓd ℓd'}
 
 open Functor
 
+EndoFunctor : ∀ {ℓa ℓb} (ℂ : Category ℓa ℓb) → Set _
+EndoFunctor ℂ = Functor ℂ ℂ
+
 module _
     {ℓa ℓb : Level}
     {ℂ 𝔻 : Category ℓa ℓb}
@@ -81,26 +113,21 @@ module _
 
 module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
   Functor≡ : {F G : Functor ℂ 𝔻}
-    → (eq* : func* F ≡ func* G)
-    → (eq→ : (λ i → ∀ {x y} → ℂ [ x , y ] → 𝔻 [ eq* i x , eq* i y ])
-        [ func→ F ≡ func→ G ])
+    → raw F ≡ raw G
     → F ≡ G
-  Functor≡ {F} {G} eq* eq→ i = record
-    { raw = eqR i
-    ; isFunctor = eqIsF i
-    }
+  raw       (Functor≡ eq i) = eq i
+  isFunctor (Functor≡ {F} {G} eq i)
+    = res i
     where
-      eqR : raw F ≡ raw G
-      eqR i = record { func* = eq* i ; func→ = eq→ i }
-      eqIsF : (λ i →  IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ]
-      eqIsF = IsFunctorIsProp' (isFunctor F) (isFunctor G)
+    res : (λ i →  IsFunctor ℂ 𝔻 (eq i)) [ isFunctor F ≡ isFunctor G ]
+    res = IsFunctorIsProp' (isFunctor F) (isFunctor G)
 
 module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
   private
-    F* = func* F
-    F→ = func→ F
-    G* = func* G
-    G→ = func→ G
+    F* = omap F
+    F→ = fmap F
+    G* = omap G
+    G→ = fmap G
     module _ {a0 a1 a2 : Object A} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where
 
       dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ]
@@ -111,8 +138,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
         C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎
 
     _∘fr_ : RawFunctor A C
-    RawFunctor.func* _∘fr_ = F* ∘ G*
-    RawFunctor.func→ _∘fr_ = F→ ∘ G→
+    RawFunctor.omap _∘fr_ = F* ∘ G*
+    RawFunctor.fmap _∘fr_ = F→ ∘ G→
     instance
       isFunctor' : IsFunctor A C _∘fr_
       isFunctor' = record
@@ -131,8 +158,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
 identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C
 identity = record
   { raw = record
-    { func* = λ x → x
-    ; func→ = λ x → x
+    { omap = λ x → x
+    ; fmap = λ x → x
     }
   ; isFunctor = record
     { isIdentity = refl
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 92805e0..2f42f32 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -1,3 +1,22 @@
+{---
+Monads
+
+This module presents two formulations of monads:
+
+  * The standard monoidal presentation
+  * Kleisli's presentation
+
+The first one defines a monad in terms of an endofunctor and two natural
+transformations. The second defines it in terms of a function on objects and a
+pair of arrows.
+
+These two formulations are proven to be equivalent:
+
+    Monoidal.Monad ≃ Kleisli.Monad
+
+The monoidal representation is exposed by default from this module.
+ ---}
+
 {-# OPTIONS --cubical --allow-unsolved-metas #-}
 module Cat.Category.Monad where
 
@@ -6,326 +25,185 @@ open import Agda.Primitive
 open import Data.Product
 
 open import Cubical
+open import Cubical.NType.Properties using (lemPropF ; lemSig ;  lemSigP)
+open import Cubical.GradLemma        using (gradLemma)
 
 open import Cat.Category
 open import Cat.Category.Functor as F
 open import Cat.Category.NaturalTransformation
+open import Cat.Category.Monad.Monoidal as Monoidal public
+open import Cat.Category.Monad.Kleisli  as Kleisli
 open import Cat.Categories.Fun
 
--- "A monad in the monoidal form" [voe]
-module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-  private
-    ℓ = ℓa ⊔ ℓb
-
-  open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
-  open NaturalTransformation ℂ ℂ
-  record RawMonad : Set ℓ where
-    field
-      -- R ~ m
-      R : Functor ℂ ℂ
-      -- η ~ pure
-      ηNat : NaturalTransformation F.identity R
-      -- μ ~ join
-      μNat : NaturalTransformation F[ R ∘ R ] R
-
-    η : Transformation F.identity R
-    η = proj₁ ηNat
-    μ : Transformation F[ R ∘ R ] R
-    μ = proj₁ μNat
-
-    private
-      module R  = Functor R
-      module RR = Functor F[ R ∘ R ]
-      module _ {X : Object} where
-        IsAssociative' : Set _
-        IsAssociative' = μ X ∘ R.func→ (μ X) ≡ μ X ∘ μ (R.func* X)
-        IsInverse' : Set _
-        IsInverse'
-          = μ X ∘ η (R.func* X) ≡ 𝟙
-          × μ X ∘ R.func→ (η X) ≡ 𝟙
-
-    -- We don't want the objects to be indexes of the type, but rather just
-    -- universally quantify over *all* objects of the category.
-    IsAssociative = {X : Object} → IsAssociative' {X}
-    IsInverse = {X : Object} → IsInverse' {X}
-
-  record IsMonad (raw : RawMonad) : Set ℓ where
-    open RawMonad raw public
-    field
-      isAssociative : IsAssociative
-      isInverse : IsInverse
-
-  record Monad : Set ℓ where
-    field
-      raw : RawMonad
-      isMonad : IsMonad raw
-    open IsMonad isMonad public
-
-  postulate propIsMonad : ∀ {raw} → isProp (IsMonad raw)
-  Monad≡ : {m n : Monad} → Monad.raw m ≡ Monad.raw n → m ≡ n
-  Monad.raw     (Monad≡ eq i) = eq i
-  Monad.isMonad (Monad≡ {m} {n} eq i) = res i
-    where
-      -- TODO: PathJ nightmare + `propIsMonad`.
-      res : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
-      res = {!!}
-
--- "A monad in the Kleisli form" [voe]
-module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-  private
-    ℓ = ℓa ⊔ ℓb
-
-  open Category ℂ using (Arrow ; 𝟙 ; Object ; _∘_)
-  record RawMonad : Set ℓ where
-    field
-      RR : Object → Object
-      -- Note name-change from [voe]
-      ζ : {X : Object} → ℂ [ X , RR X ]
-      rr : {X Y : Object} → ℂ [ X , RR Y ] → ℂ [ RR X , RR Y ]
-    -- Note the correspondance with Haskell:
-    --
-    --     RR ~ m
-    --     ζ  ~ pure
-    --     rr ~ flip (>>=)
-    --
-    -- Where those things have these types:
-    --
-    --     m : 𝓤 → 𝓤
-    --     pure : x → m x
-    --     flip (>>=) :: (a → m b) → m a → m b
-    --
-    pure : {X : Object} → ℂ [ X , RR X ]
-    pure = ζ
-    fmap : ∀ {A B} → ℂ [ A , B ] → ℂ [ RR A , RR B ]
-    fmap f = rr (ζ ∘ f)
-    -- Why is (>>=) not implementable?
-    --
-    -- (>>=) : m a -> (a -> m b) -> m b
-    -- (>=>) : (a -> m b) -> (b -> m c) -> a -> m c
-    _>=>_ : {A B C : Object} → ℂ [ A , RR B ] → ℂ [ B , RR C ] → ℂ [ A , RR C ]
-    f >=> g = rr g ∘ f
-
-    -- fmap id ≡ id
-    IsIdentity     = {X : Object}
-      → rr ζ ≡ 𝟙 {RR X}
-    IsNatural      = {X Y : Object}   (f : ℂ [ X , RR Y ])
-      → rr f ∘ ζ ≡ f
-    IsDistributive = {X Y Z : Object} (g : ℂ [ Y , RR Z ]) (f : ℂ [ X , RR Y ])
-      → rr g ∘ rr f ≡ rr (rr g ∘ f)
-    Fusion = {X Y Z : Object} {g : ℂ [ Y , Z ]} {f : ℂ [ X , Y ]}
-      → fmap (g ∘ f) ≡ fmap g ∘ fmap f
-
-  record IsMonad (raw : RawMonad) : Set ℓ where
-    open RawMonad raw public
-    field
-      isIdentity     : IsIdentity
-      isNatural      : IsNatural
-      isDistributive : IsDistributive
-    fusion : Fusion
-    fusion {g = g} {f} = begin
-      fmap (g ∘ f)              ≡⟨⟩
-      rr (ζ ∘ (g ∘ f))          ≡⟨ {!!} ⟩
-      rr (rr (ζ ∘ g) ∘ (ζ ∘ f)) ≡⟨ sym lem ⟩
-      rr (ζ ∘ g) ∘ rr (ζ ∘ f)   ≡⟨⟩
-      fmap g ∘ fmap f           ∎
-      where
-        lem : rr (ζ ∘ g) ∘ rr (ζ ∘ f) ≡ rr (rr (ζ ∘ g) ∘ (ζ ∘ f))
-        lem = isDistributive (ζ ∘ g) (ζ ∘ f)
-
-  record Monad : Set ℓ where
-    field
-      raw : RawMonad
-      isMonad : IsMonad raw
-    open IsMonad isMonad public
-
-  postulate propIsMonad : ∀ {raw} → isProp (IsMonad raw)
-  Monad≡ : {m n : Monad} → Monad.raw m ≡ Monad.raw n → m ≡ n
-  Monad.raw     (Monad≡ eq i) = eq i
-  Monad.isMonad (Monad≡ {m} {n} eq i) = res i
-    where
-      -- TODO: PathJ nightmare + `propIsMonad`.
-      res : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
-      res = {!!}
-
--- Problem 2.3
+-- | The monoidal- and kleisli presentation of monads are equivalent.
 module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
   private
-    open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
-    open Functor using (func* ; func→)
+    module ℂ = Category ℂ
+    open ℂ using (Object ; Arrow ; 𝟙 ; _∘_ ; _>>>_)
     module M = Monoidal ℂ
-    module K = Kleisli ℂ
+    module K = Kleisli  ℂ
 
-    -- Note similarity with locally defined things in Kleisly.RawMonad!!
     module _ (m : M.RawMonad) where
-      private
-        open M.RawMonad m
-        module Kraw = K.RawMonad
-
-        RR : Object → Object
-        RR = func* R
-
-        ζ : {X : Object} → ℂ [ X , RR X ]
-        ζ {X} = η X
-
-        rr : {X Y : Object} → ℂ [ X , RR Y ] → ℂ [ RR X , RR Y ]
-        rr {X} {Y} f = μ Y ∘ func→ R f
+      open M.RawMonad m
 
       forthRaw : K.RawMonad
-      Kraw.RR forthRaw = RR
-      Kraw.ζ  forthRaw = ζ
-      Kraw.rr forthRaw = rr
+      K.RawMonad.omap forthRaw = Romap
+      K.RawMonad.pure forthRaw = pureT _
+      K.RawMonad.bind forthRaw = bind
 
     module _ {raw : M.RawMonad} (m : M.IsMonad raw) where
       private
-        open M.IsMonad m
-        open K.RawMonad (forthRaw raw)
-        module Kis = K.IsMonad
-
-        isIdentity : IsIdentity
-        isIdentity {X} = begin
-          rr ζ                      ≡⟨⟩
-          rr (η X)                  ≡⟨⟩
-          μ X ∘ func→ R (η X)       ≡⟨ proj₂ isInverse ⟩
-          𝟙 ∎
-
-        module R = Functor R
-        isNatural : IsNatural
-        isNatural {X} {Y} f = begin
-          rr f ∘ ζ                  ≡⟨⟩
-          rr f ∘ η X                ≡⟨⟩
-          μ Y ∘ R.func→ f ∘ η X     ≡⟨ sym ℂ.isAssociative ⟩
-          μ Y ∘ (R.func→ f ∘ η X)   ≡⟨ cong (λ φ → μ Y ∘ φ) (sym (ηN f)) ⟩
-          μ Y ∘ (η (R.func* Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩
-          μ Y ∘ η (R.func* Y) ∘ f   ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩
-          𝟙 ∘ f                     ≡⟨ proj₂ ℂ.isIdentity ⟩
-          f ∎
-          where
-            open NaturalTransformation
-            module ℂ = Category ℂ
-            ηN : Natural ℂ ℂ F.identity R η
-            ηN = proj₂ ηNat
-
-        isDistributive : IsDistributive
-        isDistributive {X} {Y} {Z} g f = begin
-          rr g ∘ rr f                         ≡⟨⟩
-          μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ≡⟨ sym lem2 ⟩
-          μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f) ≡⟨⟩
-          μ Z ∘ R.func→ (rr g ∘ f) ∎
-          where
-            -- Proved it in reverse here... otherwise it could be neatly inlined.
-            lem2
-              : μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f)
-              ≡ μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f)
-            lem2 = begin
-              μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f)                     ≡⟨ cong (λ φ → μ Z ∘ φ) distrib ⟩
-              μ Z ∘ (R.func→ (μ Z) ∘ R.func→ (R.func→ g) ∘ R.func→ f) ≡⟨⟩
-              μ Z ∘ (R.func→ (μ Z) ∘ RR.func→ g ∘ R.func→ f)          ≡⟨ {!!} ⟩ -- ●-solver?
-              (μ Z ∘ R.func→ (μ Z)) ∘ (RR.func→ g ∘ R.func→ f)        ≡⟨ cong (λ φ → φ ∘ (RR.func→ g ∘ R.func→ f)) lemmm ⟩
-              (μ Z ∘ μ (R.func* Z)) ∘ (RR.func→ g ∘ R.func→ f)        ≡⟨ {!!} ⟩ -- ●-solver?
-              μ Z ∘ μ (R.func* Z) ∘ RR.func→ g ∘ R.func→ f            ≡⟨ {!!} ⟩ -- ●-solver + lem4
-              μ Z ∘ R.func→ g ∘ μ Y ∘ R.func→ f                       ≡⟨ sym (Category.isAssociative ℂ) ⟩
-              μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ∎
-              where
-                module RR = Functor F[ R ∘ R ]
-                distrib : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
-                  → R.func→ (a ∘ b ∘ c)
-                  ≡ R.func→ a ∘ R.func→ b ∘ R.func→ c
-                distrib = {!!}
-                comm : ∀ {A B C D E}
-                  → {a : Arrow D E} {b : Arrow C D} {c : Arrow B C} {d : Arrow A B}
-                  → a ∘ (b ∘ c ∘ d) ≡ a ∘ b ∘ c ∘ d
-                comm = {!!}
-                μN = proj₂ μNat
-                lemmm : μ Z ∘ R.func→ (μ Z) ≡ μ Z ∘ μ (R.func* Z)
-                lemmm = isAssociative
-                lem4 : μ (R.func* Z) ∘ RR.func→ g ≡ R.func→ g ∘ μ Y
-                lem4 = μN g
-
+        module MI = M.IsMonad m
       forthIsMonad : K.IsMonad (forthRaw raw)
-      Kis.isIdentity forthIsMonad = isIdentity
-      Kis.isNatural forthIsMonad = isNatural
-      Kis.isDistributive forthIsMonad = isDistributive
+      K.IsMonad.isIdentity     forthIsMonad = proj₂ MI.isInverse
+      K.IsMonad.isNatural      forthIsMonad = MI.isNatural
+      K.IsMonad.isDistributive forthIsMonad = MI.isDistributive
 
     forth : M.Monad → K.Monad
-    Kleisli.Monad.raw     (forth m) = forthRaw     (M.Monad.raw m)
+    Kleisli.Monad.raw     (forth m) = forthRaw     (M.Monad.raw     m)
     Kleisli.Monad.isMonad (forth m) = forthIsMonad (M.Monad.isMonad m)
 
     module _ (m : K.Monad) where
-      private
-        module ℂ = Category ℂ
-        open K.Monad m
-        module Mraw = M.RawMonad
-        open NaturalTransformation ℂ ℂ
-
-        rawR : RawFunctor ℂ ℂ
-        RawFunctor.func* rawR = RR
-        RawFunctor.func→ rawR f = rr (ζ ∘ f)
-
-        isFunctorR : IsFunctor ℂ ℂ rawR
-        IsFunctor.isIdentity     isFunctorR = begin
-          rr (ζ ∘ 𝟙) ≡⟨ cong rr (proj₁ ℂ.isIdentity) ⟩
-          rr ζ       ≡⟨ isIdentity ⟩
-          𝟙 ∎
-        IsFunctor.isDistributive isFunctorR {f = f} {g} = begin
-          rr (ζ ∘ (g ∘ f))        ≡⟨⟩
-          fmap (g ∘ f)            ≡⟨ fusion ⟩
-          fmap g ∘ fmap f         ≡⟨⟩
-          rr (ζ ∘ g) ∘ rr (ζ ∘ f) ∎
-
-        R : Functor ℂ ℂ
-        Functor.raw       R = rawR
-        Functor.isFunctor R = isFunctorR
-
-        R2 : Functor ℂ ℂ
-        R2 = F[ R ∘ R ]
-
-        ηNat : NaturalTransformation F.identity R
-        ηNat = {!!}
-
-        μNat : NaturalTransformation R2 R
-        μNat = {!!}
+      open K.Monad m
 
       backRaw : M.RawMonad
-      Mraw.R    backRaw = R
-      Mraw.ηNat backRaw = ηNat
-      Mraw.μNat backRaw = μNat
+      M.RawMonad.R      backRaw = R
+      M.RawMonad.pureNT backRaw = pureNT
+      M.RawMonad.joinNT backRaw = joinNT
 
-    module _ (m : K.Monad) where
-      open K.Monad m
-      open M.RawMonad (backRaw m)
-      module Mis = M.IsMonad
+      private
+        open M.RawMonad backRaw
+        module R = Functor (M.RawMonad.R backRaw)
 
-      backIsMonad : M.IsMonad (backRaw m)
-      backIsMonad = {!!}
+      backIsMonad : M.IsMonad backRaw
+      M.IsMonad.isAssociative backIsMonad {X} = begin
+        joinT X  ∘ R.fmap (joinT X)  ≡⟨⟩
+        join ∘ fmap (joinT X)         ≡⟨⟩
+        join ∘ fmap join              ≡⟨ isNaturalForeign ⟩
+        join ∘ join                   ≡⟨⟩
+        joinT X  ∘ joinT (R.omap X)  ∎
+      M.IsMonad.isInverse backIsMonad {X} = inv-l , inv-r
+        where
+        inv-l = begin
+          joinT X ∘ pureT (R.omap X) ≡⟨⟩
+          join ∘ pure                 ≡⟨ proj₁ isInverse ⟩
+          𝟙                           ∎
+        inv-r = begin
+          joinT X ∘ R.fmap (pureT X) ≡⟨⟩
+          join ∘ fmap pure            ≡⟨ proj₂ isInverse ⟩
+          𝟙                           ∎
 
     back : K.Monad → M.Monad
     Monoidal.Monad.raw     (back m) = backRaw     m
     Monoidal.Monad.isMonad (back m) = backIsMonad m
 
-    -- I believe all the proofs here should be `refl`.
     module _ (m : K.Monad) where
-      open K.RawMonad (K.Monad.raw m)
+      private
+        open K.Monad m
+        bindEq : ∀ {X Y}
+          → K.RawMonad.bind (forthRaw (backRaw m)) {X} {Y}
+          ≡ K.RawMonad.bind (K.Monad.raw m)
+        bindEq {X} {Y} = begin
+          K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩
+          (λ f → join ∘ fmap f)                  ≡⟨⟩
+          (λ f → bind (f >>> pure) >>> bind 𝟙)   ≡⟨ funExt lem ⟩
+          (λ f → bind f)                         ≡⟨⟩
+          bind                                   ∎
+          where
+          lem : (f : Arrow X (omap Y))
+            → bind (f >>> pure) >>> bind 𝟙
+            ≡ bind f
+          lem f = begin
+            bind (f >>> pure) >>> bind 𝟙
+              ≡⟨ isDistributive _ _ ⟩
+            bind ((f >>> pure) >>> bind 𝟙)
+              ≡⟨ cong bind ℂ.isAssociative ⟩
+            bind (f >>> (pure >>> bind 𝟙))
+              ≡⟨ cong (λ φ → bind (f >>> φ)) (isNatural _) ⟩
+            bind (f >>> 𝟙)
+              ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩
+            bind f ∎
+
       forthRawEq : forthRaw (backRaw m) ≡ K.Monad.raw m
-      K.RawMonad.RR (forthRawEq _) = RR
-      K.RawMonad.ζ  (forthRawEq _) = ζ
-      -- stuck
-      K.RawMonad.rr (forthRawEq i) = {!!}
+      K.RawMonad.omap  (forthRawEq _) = omap
+      K.RawMonad.pure  (forthRawEq _) = pure
+      K.RawMonad.bind  (forthRawEq i) = bindEq i
 
     fortheq : (m : K.Monad) → forth (back m) ≡ m
     fortheq m = K.Monad≡ (forthRawEq m)
 
     module _ (m : M.Monad) where
-      open M.RawMonad (M.Monad.raw m)
+      private
+        open M.Monad m
+        module KM = K.Monad (forth m)
+        module R = Functor R
+        omapEq : KM.omap ≡ Romap
+        omapEq = refl
+
+        bindEq : ∀ {X Y} {f : Arrow X (Romap Y)} → KM.bind f ≡ bind f
+        bindEq {X} {Y} {f} = begin
+          KM.bind f         ≡⟨⟩
+          joinT Y ∘ Rfmap f ≡⟨⟩
+          bind f            ∎
+
+        joinEq : ∀ {X} → KM.join ≡ joinT X
+        joinEq {X} = begin
+          KM.join                ≡⟨⟩
+          KM.bind 𝟙              ≡⟨⟩
+          bind 𝟙                 ≡⟨⟩
+          joinT X ∘ Rfmap 𝟙      ≡⟨ cong (λ φ → _ ∘ φ) R.isIdentity ⟩
+          joinT X ∘ 𝟙            ≡⟨ proj₁ ℂ.isIdentity ⟩
+          joinT X                ∎
+
+        fmapEq : ∀ {A B} → KM.fmap {A} {B} ≡ Rfmap
+        fmapEq {A} {B} = funExt (λ f → begin
+          KM.fmap f                                ≡⟨⟩
+          KM.bind (f >>> KM.pure)                  ≡⟨⟩
+             bind (f >>> pureT _)                  ≡⟨⟩
+             Rfmap (f >>> pureT B) >>> joinT B     ≡⟨⟩
+          Rfmap (f >>> pureT B) >>> joinT B        ≡⟨ cong (λ φ → φ >>> joinT B) R.isDistributive ⟩
+          Rfmap f >>> Rfmap (pureT B) >>> joinT B  ≡⟨ ℂ.isAssociative ⟩
+          joinT B ∘ Rfmap (pureT B) ∘ Rfmap f      ≡⟨ cong (λ φ → φ ∘ Rfmap f) (proj₂ isInverse) ⟩
+          𝟙 ∘ Rfmap f                              ≡⟨ proj₂ ℂ.isIdentity ⟩
+          Rfmap f                                  ∎
+          )
+
+        rawEq : Functor.raw KM.R ≡ Functor.raw R
+        RawFunctor.omap (rawEq i) = omapEq i
+        RawFunctor.fmap (rawEq i) = fmapEq i
+
+      Req : M.RawMonad.R (backRaw (forth m)) ≡ R
+      Req = Functor≡ rawEq
+
+      open NaturalTransformation ℂ ℂ
+
+      pureTEq : M.RawMonad.pureT (backRaw (forth m)) ≡ pureT
+      pureTEq = funExt (λ X → refl)
+
+      pureNTEq : (λ i → NaturalTransformation F.identity (Req i))
+        [ M.RawMonad.pureNT (backRaw (forth m)) ≡ pureNT ]
+      pureNTEq = lemSigP (λ i → propIsNatural F.identity (Req i)) _ _ pureTEq
+
+      joinTEq : M.RawMonad.joinT (backRaw (forth m)) ≡ joinT
+      joinTEq = funExt (λ X → begin
+        M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩
+        KM.join ≡⟨⟩
+        joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩
+        joinT X ∘ 𝟙 ≡⟨ proj₁ ℂ.isIdentity ⟩
+        joinT X ∎)
+
+      joinNTEq : (λ i → NaturalTransformation F[ Req i ∘ Req i ] (Req i))
+        [ M.RawMonad.joinNT (backRaw (forth m)) ≡ joinNT ]
+      joinNTEq = lemSigP (λ i → propIsNatural F[ Req i ∘ Req i ] (Req i)) _ _ joinTEq
+
       backRawEq : backRaw (forth m) ≡ M.Monad.raw m
-      -- stuck
-      M.RawMonad.R    (backRawEq i) = {!!}
-      M.RawMonad.ηNat (backRawEq i) = {!!}
-      M.RawMonad.μNat (backRawEq i) = {!!}
+      M.RawMonad.R      (backRawEq i) = Req i
+      M.RawMonad.pureNT (backRawEq i) = pureNTEq i
+      M.RawMonad.joinNT (backRawEq i) = joinNTEq i
 
     backeq : (m : M.Monad) → back (forth m) ≡ m
     backeq m = M.Monad≡ (backRawEq m)
 
-    open import Cubical.GradLemma
     eqv : isEquiv M.Monad K.Monad forth
     eqv = gradLemma forth back fortheq backeq
 
diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda
new file mode 100644
index 0000000..8f96b82
--- /dev/null
+++ b/src/Cat/Category/Monad/Kleisli.agda
@@ -0,0 +1,253 @@
+{---
+The Kleisli formulation of monads
+ ---}
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
+open import Agda.Primitive
+
+open import Data.Product
+
+open import Cubical
+open import Cubical.NType.Properties using (lemPropF ; lemSig ;  lemSigP)
+open import Cubical.GradLemma        using (gradLemma)
+
+open import Cat.Category
+open import Cat.Category.Functor as F
+open import Cat.Category.NaturalTransformation
+open import Cat.Categories.Fun
+
+-- "A monad in the Kleisli form" [voe]
+module Cat.Category.Monad.Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+private
+  ℓ = ℓa ⊔ ℓb
+  module ℂ = Category ℂ
+  open ℂ using (Arrow ; 𝟙 ; Object ; _∘_ ; _>>>_)
+
+-- | Data for a monad.
+--
+-- Note that (>>=) is not expressible in a general category because objects
+-- are not generally types.
+record RawMonad : Set ℓ where
+  field
+    omap : Object → Object
+    pure : {X : Object}   → ℂ [ X , omap X ]
+    bind : {X Y : Object} → ℂ [ X , omap Y ] → ℂ [ omap X , omap Y ]
+
+  -- | functor map
+  --
+  -- This should perhaps be defined in a "Klesli-version" of functors as well?
+  fmap : ∀ {A B} → ℂ [ A , B ] → ℂ [ omap A , omap B ]
+  fmap f = bind (pure ∘ f)
+
+  -- | Composition of monads aka. the kleisli-arrow.
+  _>=>_ : {A B C : Object} → ℂ [ A , omap B ] → ℂ [ B , omap C ] → ℂ [ A , omap C ]
+  f >=> g = f >>> (bind g)
+
+  -- | Flattening nested monads.
+  join : {A : Object} → ℂ [ omap (omap A) , omap A ]
+  join = bind 𝟙
+
+  ------------------
+  -- * Monad laws --
+  ------------------
+
+  -- There may be better names than what I've chosen here.
+
+  IsIdentity     = {X : Object}
+    → bind pure ≡ 𝟙 {omap X}
+  IsNatural      = {X Y : Object}   (f : ℂ [ X , omap Y ])
+    → pure >>> (bind f) ≡ f
+  IsDistributive = {X Y Z : Object} (g : ℂ [ Y , omap Z ]) (f : ℂ [ X , omap Y ])
+    → (bind f) >>> (bind g) ≡ bind (f >=> g)
+
+  -- | Functor map fusion.
+  --
+  -- This is really a functor law. Should we have a kleisli-representation of
+  -- functors as well and make them a super-class?
+  Fusion = {X Y Z : Object} {g : ℂ [ Y , Z ]} {f : ℂ [ X , Y ]}
+    → fmap (g ∘ f) ≡ fmap g ∘ fmap f
+
+  -- In the ("foreign") formulation of a monad `IsNatural`'s analogue here would be:
+  IsNaturalForeign : Set _
+  IsNaturalForeign = {X : Object} → join {X} ∘ fmap join ≡ join ∘ join
+
+  IsInverse : Set _
+  IsInverse = {X : Object} → join {X} ∘ pure ≡ 𝟙 × join {X} ∘ fmap pure ≡ 𝟙
+
+record IsMonad (raw : RawMonad) : Set ℓ where
+  open RawMonad raw public
+  field
+    isIdentity     : IsIdentity
+    isNatural      : IsNatural
+    isDistributive : IsDistributive
+
+  -- | Map fusion is admissable.
+  fusion : Fusion
+  fusion {g = g} {f} = begin
+    fmap (g ∘ f)               ≡⟨⟩
+    bind ((f >>> g) >>> pure)  ≡⟨ cong bind ℂ.isAssociative ⟩
+    bind (f >>> (g >>> pure))  ≡⟨ cong (λ φ → bind (f >>> φ)) (sym (isNatural _)) ⟩
+    bind (f >>> (pure >>> (bind (g >>> pure)))) ≡⟨⟩
+    bind (f >>> (pure >>> fmap g)) ≡⟨⟩
+    bind ((fmap g ∘ pure) ∘ f) ≡⟨ cong bind (sym ℂ.isAssociative) ⟩
+    bind (fmap g ∘ (pure ∘ f)) ≡⟨ sym distrib ⟩
+    bind (pure ∘ g) ∘ bind (pure ∘ f) ≡⟨⟩
+    fmap g ∘ fmap f            ∎
+    where
+      distrib : fmap g ∘ fmap f ≡ bind (fmap g ∘ (pure ∘ f))
+      distrib = isDistributive (pure ∘ g) (pure ∘ f)
+
+  -- | This formulation gives rise to the following endo-functor.
+  private
+    rawR : RawFunctor ℂ ℂ
+    RawFunctor.omap rawR = omap
+    RawFunctor.fmap rawR = fmap
+
+    isFunctorR : IsFunctor ℂ ℂ rawR
+    IsFunctor.isIdentity isFunctorR = begin
+      bind (pure ∘ 𝟙) ≡⟨ cong bind (proj₁ ℂ.isIdentity) ⟩
+      bind pure       ≡⟨ isIdentity ⟩
+      𝟙               ∎
+
+    IsFunctor.isDistributive isFunctorR {f = f} {g} = begin
+      bind (pure ∘ (g ∘ f))             ≡⟨⟩
+      fmap (g ∘ f)                      ≡⟨ fusion ⟩
+      fmap g ∘ fmap f                   ≡⟨⟩
+      bind (pure ∘ g) ∘ bind (pure ∘ f) ∎
+
+  -- FIXME Naming!
+  R : EndoFunctor ℂ
+  Functor.raw       R = rawR
+  Functor.isFunctor R = isFunctorR
+
+  private
+    open NaturalTransformation ℂ ℂ
+
+    R⁰ : EndoFunctor ℂ
+    R⁰ = F.identity
+    R² : EndoFunctor ℂ
+    R² = F[ R ∘ R ]
+    module R  = Functor R
+    module R⁰ = Functor R⁰
+    module R² = Functor R²
+    pureT : Transformation R⁰ R
+    pureT A = pure
+    pureN : Natural R⁰ R pureT
+    pureN {A} {B} f = begin
+      pureT B             ∘ R⁰.fmap f ≡⟨⟩
+      pure            ∘ f          ≡⟨ sym (isNatural _) ⟩
+      bind (pure ∘ f) ∘ pure       ≡⟨⟩
+      fmap f          ∘ pure       ≡⟨⟩
+      R.fmap f       ∘ pureT A        ∎
+    joinT : Transformation R² R
+    joinT C = join
+    joinN : Natural R² R joinT
+    joinN f = begin
+      join       ∘ R².fmap f  ≡⟨⟩
+      bind 𝟙     ∘ R².fmap f  ≡⟨⟩
+      R².fmap f >>> bind 𝟙    ≡⟨⟩
+      fmap (fmap f) >>> bind 𝟙 ≡⟨⟩
+      fmap (bind (f >>> pure)) >>> bind 𝟙          ≡⟨⟩
+      bind (bind (f >>> pure) >>> pure) >>> bind 𝟙
+        ≡⟨ isDistributive _ _ ⟩
+      bind ((bind (f >>> pure) >>> pure) >=> 𝟙)
+        ≡⟨⟩
+      bind ((bind (f >>> pure) >>> pure) >>> bind 𝟙)
+        ≡⟨ cong bind ℂ.isAssociative ⟩
+      bind (bind (f >>> pure) >>> (pure >>> bind 𝟙))
+        ≡⟨ cong (λ φ → bind (bind (f >>> pure) >>> φ)) (isNatural _) ⟩
+      bind (bind (f >>> pure) >>> 𝟙)
+        ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩
+      bind (bind (f >>> pure))
+        ≡⟨ cong bind (sym (proj₁ ℂ.isIdentity)) ⟩
+      bind (𝟙 >>> bind (f >>> pure)) ≡⟨⟩
+      bind (𝟙 >=> (f >>> pure))
+        ≡⟨ sym (isDistributive _ _) ⟩
+      bind 𝟙     >>> bind (f >>> pure)    ≡⟨⟩
+      bind 𝟙     >>> fmap f    ≡⟨⟩
+      bind 𝟙     >>> R.fmap f ≡⟨⟩
+      R.fmap f  ∘ bind 𝟙      ≡⟨⟩
+      R.fmap f  ∘ join        ∎
+
+  pureNT : NaturalTransformation R⁰ R
+  proj₁ pureNT = pureT
+  proj₂ pureNT = pureN
+
+  joinNT : NaturalTransformation R² R
+  proj₁ joinNT = joinT
+  proj₂ joinNT = joinN
+
+  isNaturalForeign : IsNaturalForeign
+  isNaturalForeign = begin
+    fmap join >>> join ≡⟨⟩
+    bind (join >>> pure) >>> bind 𝟙
+      ≡⟨ isDistributive _ _ ⟩
+    bind ((join >>> pure) >>> bind 𝟙)
+      ≡⟨ cong bind ℂ.isAssociative ⟩
+    bind (join >>> (pure >>> bind 𝟙))
+      ≡⟨ cong (λ φ → bind (join >>> φ)) (isNatural _) ⟩
+    bind (join >>> 𝟙)
+      ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩
+    bind join           ≡⟨⟩
+    bind (bind 𝟙)
+      ≡⟨ cong bind (sym (proj₁ ℂ.isIdentity)) ⟩
+    bind (𝟙 >>> bind 𝟙) ≡⟨⟩
+    bind (𝟙 >=> 𝟙)      ≡⟨ sym (isDistributive _ _) ⟩
+    bind 𝟙 >>> bind 𝟙   ≡⟨⟩
+    join >>> join       ∎
+
+  isInverse : IsInverse
+  isInverse = inv-l , inv-r
+    where
+    inv-l = begin
+      pure >>> join   ≡⟨⟩
+      pure >>> bind 𝟙 ≡⟨ isNatural _ ⟩
+      𝟙 ∎
+    inv-r = begin
+      fmap pure >>> join ≡⟨⟩
+      bind (pure >>> pure) >>> bind 𝟙
+        ≡⟨ isDistributive _ _ ⟩
+      bind ((pure >>> pure) >=> 𝟙) ≡⟨⟩
+      bind ((pure >>> pure) >>> bind 𝟙)
+        ≡⟨ cong bind ℂ.isAssociative ⟩
+      bind (pure >>> (pure >>> bind 𝟙))
+        ≡⟨ cong (λ φ → bind (pure >>> φ)) (isNatural _) ⟩
+      bind (pure >>> 𝟙)
+        ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩
+      bind pure ≡⟨ isIdentity ⟩
+      𝟙 ∎
+
+record Monad : Set ℓ where
+  field
+    raw : RawMonad
+    isMonad : IsMonad raw
+  open IsMonad isMonad public
+
+private
+  module _ (raw : RawMonad) where
+    open RawMonad raw
+    propIsIdentity : isProp IsIdentity
+    propIsIdentity x y i = ℂ.arrowsAreSets _ _ x y i
+    propIsNatural      : isProp IsNatural
+    propIsNatural x y i = λ f
+      → ℂ.arrowsAreSets _ _ (x f) (y f) i
+    propIsDistributive : isProp IsDistributive
+    propIsDistributive x y i = λ g f
+      → ℂ.arrowsAreSets _ _ (x g f) (y g f) i
+
+  open IsMonad
+  propIsMonad : (raw : _) → isProp (IsMonad raw)
+  IsMonad.isIdentity     (propIsMonad raw x y i)
+    = propIsIdentity raw (isIdentity x) (isIdentity y) i
+  IsMonad.isNatural      (propIsMonad raw x y i)
+    = propIsNatural raw (isNatural x) (isNatural y) i
+  IsMonad.isDistributive (propIsMonad raw x y i)
+    = propIsDistributive raw (isDistributive x) (isDistributive y) i
+
+module _ {m n : Monad} (eq : Monad.raw m ≡ Monad.raw n) where
+  private
+    eqIsMonad : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
+    eqIsMonad = lemPropF propIsMonad eq
+
+  Monad≡ : m ≡ n
+  Monad.raw     (Monad≡ i) = eq i
+  Monad.isMonad (Monad≡ i) = eqIsMonad i
diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda
new file mode 100644
index 0000000..b969187
--- /dev/null
+++ b/src/Cat/Category/Monad/Monoidal.agda
@@ -0,0 +1,154 @@
+{---
+Monoidal formulation of monads
+ ---}
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
+open import Agda.Primitive
+
+open import Data.Product
+
+open import Cubical
+open import Cubical.NType.Properties using (lemPropF ; lemSig ;  lemSigP)
+open import Cubical.GradLemma        using (gradLemma)
+
+open import Cat.Category
+open import Cat.Category.Functor as F
+open import Cat.Category.NaturalTransformation
+open import Cat.Categories.Fun
+
+module Cat.Category.Monad.Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+
+-- "A monad in the monoidal form" [voe]
+private
+  ℓ = ℓa ⊔ ℓb
+
+open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
+open NaturalTransformation ℂ ℂ
+record RawMonad : Set ℓ where
+  field
+    R      : EndoFunctor ℂ
+    pureNT : NaturalTransformation F.identity R
+    joinNT : NaturalTransformation F[ R ∘ R ] R
+
+  -- Note that `pureT` and `joinT` differs from their definition in the
+  -- kleisli formulation only by having an explicit parameter.
+  pureT : Transformation F.identity R
+  pureT = proj₁ pureNT
+  pureN : Natural F.identity R pureT
+  pureN = proj₂ pureNT
+
+  joinT : Transformation F[ R ∘ R ] R
+  joinT = proj₁ joinNT
+  joinN : Natural F[ R ∘ R ] R joinT
+  joinN = proj₂ joinNT
+
+  Romap = Functor.omap R
+  Rfmap = Functor.fmap R
+
+  bind : {X Y : Object} → ℂ [ X , Romap Y ] → ℂ [ Romap X , Romap Y ]
+  bind {X} {Y} f = joinT Y ∘ Rfmap f
+
+  IsAssociative : Set _
+  IsAssociative = {X : Object}
+    → joinT X ∘ Rfmap (joinT X) ≡ joinT X ∘ joinT (Romap X)
+  IsInverse : Set _
+  IsInverse = {X : Object}
+    → joinT X ∘ pureT (Romap X) ≡ 𝟙
+    × joinT X ∘ Rfmap (pureT X) ≡ 𝟙
+  IsNatural = ∀ {X Y} f → joinT Y ∘ Rfmap f ∘ pureT X ≡ f
+  IsDistributive = ∀ {X Y Z} (g : Arrow Y (Romap Z)) (f : Arrow X (Romap Y))
+    → joinT Z ∘ Rfmap g ∘ (joinT Y ∘ Rfmap f)
+    ≡ joinT Z ∘ Rfmap (joinT Z ∘ Rfmap g ∘ f)
+
+record IsMonad (raw : RawMonad) : Set ℓ where
+  open RawMonad raw public
+  field
+    isAssociative : IsAssociative
+    isInverse     : IsInverse
+
+  private
+    module R = Functor R
+    module ℂ = Category ℂ
+
+  isNatural : IsNatural
+  isNatural {X} {Y} f = begin
+    joinT Y ∘ R.fmap f ∘ pureT X     ≡⟨ sym ℂ.isAssociative ⟩
+    joinT Y ∘ (R.fmap f ∘ pureT X)   ≡⟨ cong (λ φ → joinT Y ∘ φ) (sym (pureN f)) ⟩
+    joinT Y ∘ (pureT (R.omap Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩
+    joinT Y ∘ pureT (R.omap Y) ∘ f   ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩
+    𝟙 ∘ f                     ≡⟨ proj₂ ℂ.isIdentity ⟩
+    f                         ∎
+
+  isDistributive : IsDistributive
+  isDistributive {X} {Y} {Z} g f = sym aux
+    where
+    module R² = Functor F[ R ∘ R ]
+    distrib3 : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
+      → R.fmap (a ∘ b ∘ c)
+      ≡ R.fmap a ∘ R.fmap b ∘ R.fmap c
+    distrib3 {a = a} {b} {c} = begin
+      R.fmap (a ∘ b ∘ c)               ≡⟨ R.isDistributive ⟩
+      R.fmap (a ∘ b) ∘ R.fmap c       ≡⟨ cong (_∘ _) R.isDistributive ⟩
+      R.fmap a ∘ R.fmap b ∘ R.fmap c ∎
+    aux = begin
+      joinT Z ∘ R.fmap (joinT Z ∘ R.fmap g ∘ f)
+        ≡⟨ cong (λ φ → joinT Z ∘ φ) distrib3 ⟩
+      joinT Z ∘ (R.fmap (joinT Z) ∘ R.fmap (R.fmap g) ∘ R.fmap f)
+        ≡⟨⟩
+      joinT Z ∘ (R.fmap (joinT Z) ∘ R².fmap g ∘ R.fmap f)
+        ≡⟨ cong (_∘_ (joinT Z)) (sym ℂ.isAssociative) ⟩
+      joinT Z ∘ (R.fmap (joinT Z) ∘ (R².fmap g ∘ R.fmap f))
+        ≡⟨ ℂ.isAssociative ⟩
+      (joinT Z ∘ R.fmap (joinT Z)) ∘ (R².fmap g ∘ R.fmap f)
+        ≡⟨ cong (λ φ → φ ∘ (R².fmap g ∘ R.fmap f)) isAssociative ⟩
+      (joinT Z ∘ joinT (R.omap Z)) ∘ (R².fmap g ∘ R.fmap f)
+        ≡⟨ ℂ.isAssociative ⟩
+      joinT Z ∘ joinT (R.omap Z) ∘ R².fmap g ∘ R.fmap f
+        ≡⟨⟩
+      ((joinT Z ∘ joinT (R.omap Z)) ∘ R².fmap g) ∘ R.fmap f
+        ≡⟨ cong (_∘ R.fmap f) (sym ℂ.isAssociative) ⟩
+      (joinT Z ∘ (joinT (R.omap Z) ∘ R².fmap g)) ∘ R.fmap f
+        ≡⟨ cong (λ φ → φ ∘ R.fmap f) (cong (_∘_ (joinT Z)) (joinN g)) ⟩
+      (joinT Z ∘ (R.fmap g ∘ joinT Y)) ∘ R.fmap f
+        ≡⟨ cong (_∘ R.fmap f) ℂ.isAssociative ⟩
+      joinT Z ∘ R.fmap g ∘ joinT Y ∘ R.fmap f
+        ≡⟨ sym (Category.isAssociative ℂ) ⟩
+      joinT Z ∘ R.fmap g ∘ (joinT Y ∘ R.fmap f)
+        ∎
+
+record Monad : Set ℓ where
+  field
+    raw     : RawMonad
+    isMonad : IsMonad raw
+  open IsMonad isMonad public
+
+private
+  module _ {m : RawMonad} where
+    open RawMonad m
+    propIsAssociative : isProp IsAssociative
+    propIsAssociative x y i {X}
+      = Category.arrowsAreSets ℂ _ _ (x {X}) (y {X}) i
+    propIsInverse : isProp IsInverse
+    propIsInverse x y i {X} = e1 i , e2 i
+      where
+      xX = x {X}
+      yX = y {X}
+      e1 = Category.arrowsAreSets ℂ _ _ (proj₁ xX) (proj₁ yX)
+      e2 = Category.arrowsAreSets ℂ _ _ (proj₂ xX) (proj₂ yX)
+
+  open IsMonad
+  propIsMonad : (raw : _) → isProp (IsMonad raw)
+  IsMonad.isAssociative (propIsMonad raw a b i) j
+    = propIsAssociative {raw}
+      (isAssociative a) (isAssociative b) i j
+  IsMonad.isInverse     (propIsMonad raw a b i)
+    = propIsInverse {raw}
+      (isInverse a) (isInverse b) i
+
+module _ {m n : Monad} (eq : Monad.raw m ≡ Monad.raw n) where
+  private
+    eqIsMonad : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
+    eqIsMonad = lemPropF propIsMonad eq
+
+  Monad≡ : m ≡ n
+  Monad.raw     (Monad≡ i) = eq i
+  Monad.isMonad (Monad≡ i) = eqIsMonad i
diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda
new file mode 100644
index 0000000..3a807de
--- /dev/null
+++ b/src/Cat/Category/Monad/Voevodsky.agda
@@ -0,0 +1,211 @@
+{-
+This module provides construction 2.3 in [voe]
+-}
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
+module Cat.Category.Monad.Voevodsky where
+
+open import Agda.Primitive
+
+open import Data.Product
+
+open import Cubical
+open import Cubical.NType.Properties using (lemPropF ; lemSig ;  lemSigP)
+open import Cubical.GradLemma        using (gradLemma)
+
+open import Cat.Category
+open import Cat.Category.Functor as F
+open import Cat.Category.NaturalTransformation
+open import Cat.Category.Monad using (Monoidal≃Kleisli)
+import Cat.Category.Monad.Monoidal as Monoidal
+import Cat.Category.Monad.Kleisli  as Kleisli
+open import Cat.Categories.Fun
+
+module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  private
+    ℓ = ℓa ⊔ ℓb
+    module ℂ = Category ℂ
+    open ℂ using (Object ; Arrow)
+    open NaturalTransformation ℂ ℂ
+    open import Function using (_∘_ ; _$_)
+    module M = Monoidal ℂ
+    module K = Kleisli  ℂ
+
+  module §2-3 (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where
+    record §1 : Set ℓ where
+      open M
+
+      field
+        fmap : Fmap ℂ ℂ omap
+        join : {A : Object} → ℂ [ omap (omap A) , omap A ]
+
+      Rraw : RawFunctor ℂ ℂ
+      Rraw = record
+        { omap = omap
+        ; fmap = fmap
+        }
+
+      field
+        RisFunctor : IsFunctor ℂ ℂ Rraw
+
+      R : EndoFunctor ℂ
+      R = record
+        { raw = Rraw
+        ; isFunctor = RisFunctor
+        }
+
+      pureT : (X : Object) → Arrow X (omap X)
+      pureT X = pure {X}
+
+      field
+        pureN : Natural F.identity R pureT
+
+      pureNT : NaturalTransformation F.identity R
+      pureNT = pureT , pureN
+
+      joinT : (A : Object) → ℂ [ omap (omap A) , omap A ]
+      joinT A = join {A}
+
+      field
+        joinN : Natural F[ R ∘ R ] R joinT
+
+      joinNT : NaturalTransformation F[ R ∘ R ] R
+      joinNT = joinT , joinN
+
+      rawMnd : RawMonad
+      rawMnd = record
+        { R = R
+        ; pureNT = pureNT
+        ; joinNT = joinNT
+        }
+
+      field
+        isMnd : IsMonad rawMnd
+
+      toMonad : Monad
+      toMonad = record
+        { raw     = rawMnd
+        ; isMonad = isMnd
+        }
+
+    record §2 : Set ℓ where
+      open K
+
+      field
+        bind : {X Y : Object} → ℂ [ X , omap Y ] → ℂ [ omap X , omap Y ]
+
+      rawMnd : RawMonad
+      rawMnd = record
+        { omap = omap
+        ; pure = pure
+        ; bind = bind
+        }
+
+      field
+        isMnd : IsMonad rawMnd
+
+      toMonad : Monad
+      toMonad = record
+        { raw     = rawMnd
+        ; isMonad = isMnd
+        }
+
+  §1-fromMonad : (m : M.Monad) → §2-3.§1 (M.Monad.Romap m) (λ {X} → M.Monad.pureT m X)
+  -- voe-2-3-1-fromMonad : (m : M.Monad) → voe.§2-3.§1 (M.Monad.Romap m) (λ {X} → M.Monad.pureT m X)
+  §1-fromMonad m = record
+    { fmap = Functor.fmap R
+    ; RisFunctor = Functor.isFunctor R
+    ; pureN = pureN
+    ; join = λ {X} → joinT X
+    ; joinN = joinN
+    ; isMnd = M.Monad.isMonad m
+    }
+    where
+    raw = M.Monad.raw m
+    R   = M.RawMonad.R raw
+    pureT = M.RawMonad.pureT raw
+    pureN = M.RawMonad.pureN raw
+    joinT = M.RawMonad.joinT raw
+    joinN = M.RawMonad.joinN raw
+
+  §2-fromMonad : (m : K.Monad) → §2-3.§2 (K.Monad.omap m) (K.Monad.pure m)
+  §2-fromMonad m = record
+    { bind  = K.Monad.bind    m
+    ; isMnd = K.Monad.isMonad m
+    }
+
+  module _ (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where
+    private
+      Monoidal→Kleisli : M.Monad → K.Monad
+      Monoidal→Kleisli = proj₁ Monoidal≃Kleisli
+
+      Kleisli→Monoidal : K.Monad → M.Monad
+      Kleisli→Monoidal = inverse Monoidal≃Kleisli
+
+      forth : §2-3.§1 omap pure → §2-3.§2 omap pure
+      forth = §2-fromMonad ∘ Monoidal→Kleisli ∘ §2-3.§1.toMonad
+
+      back : §2-3.§2 omap pure → §2-3.§1 omap pure
+      back = §1-fromMonad ∘ Kleisli→Monoidal ∘ §2-3.§2.toMonad
+
+      forthEq : ∀ m → _ ≡ _
+      forthEq m = begin
+        (forth ∘ back) m ≡⟨⟩
+        -- In full gory detail:
+        ( §2-fromMonad
+        ∘ Monoidal→Kleisli
+        ∘ §2-3.§1.toMonad
+        ∘ §1-fromMonad
+        ∘ Kleisli→Monoidal
+        ∘ §2-3.§2.toMonad
+        ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
+        ( §2-fromMonad
+        ∘ Monoidal→Kleisli
+        ∘ Kleisli→Monoidal
+        ∘ §2-3.§2.toMonad
+        ) m ≡⟨ u ⟩
+        -- Monoidal→Kleisli and Kleisli→Monoidal are inverses
+        -- I should be able to prove this using congruence and `lem` below.
+        ( §2-fromMonad
+        ∘ §2-3.§2.toMonad
+        ) m ≡⟨⟩
+        (  §2-fromMonad
+        ∘ §2-3.§2.toMonad
+        ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
+        m ∎
+        where
+        lem : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id
+        lem = {!!} -- verso-recto Monoidal≃Kleisli
+        t : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad)
+          ≡ (§2-fromMonad ∘ §2-3.§2.toMonad)
+        t = cong (λ φ → §2-fromMonad ∘ (λ{ {ω} → φ {{!????!}}}) ∘ §2-3.§2.toMonad) {!lem!}
+        u : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad) m
+          ≡ (§2-fromMonad ∘ §2-3.§2.toMonad) m
+        u = cong (λ φ → φ m) t
+
+      backEq : ∀ m → (back ∘ forth) m ≡ m
+      backEq m = begin
+        (back ∘ forth) m ≡⟨⟩
+        ( §1-fromMonad
+        ∘ Kleisli→Monoidal
+        ∘ §2-3.§2.toMonad
+        ∘ §2-fromMonad
+        ∘ Monoidal→Kleisli
+        ∘ §2-3.§1.toMonad
+        ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
+        ( §1-fromMonad
+        ∘ Kleisli→Monoidal
+        ∘ Monoidal→Kleisli
+        ∘ §2-3.§1.toMonad
+        ) m ≡⟨ cong (λ φ → φ m) t ⟩ -- Monoidal→Kleisli and Kleisli→Monoidal are inverses
+        ( §1-fromMonad
+        ∘ §2-3.§1.toMonad
+        ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
+        m ∎
+        where
+        t = {!!} -- cong (λ φ → voe-2-3-1-fromMonad ∘ φ ∘ voe-2-3.voe-2-3-1.toMonad) (recto-verso Monoidal≃Kleisli)
+
+      voe-isEquiv : isEquiv (§2-3.§1 omap pure) (§2-3.§2 omap pure) forth
+      voe-isEquiv = gradLemma forth back forthEq backEq
+
+    equiv-2-3 : §2-3.§1 omap pure ≃ §2-3.§2 omap pure
+    equiv-2-3 = forth , voe-isEquiv
diff --git a/src/Cat/Category/Monoid.agda b/src/Cat/Category/Monoid.agda
index 3323487..a17468e 100644
--- a/src/Cat/Category/Monoid.agda
+++ b/src/Cat/Category/Monoid.agda
@@ -12,10 +12,14 @@ module _ (ℓa ℓb : Level) where
   private
     ℓ = lsuc (ℓa ⊔ ℓb)
 
-  -- Might not need this to be able to form products of categories!
-  postulate unprovable : IsCategory (Cat.RawCat ℓa ℓb)
-
-  open HasProducts (Cat.hasProducts unprovable)
+    -- *If* the category of categories existed `_×_` would be equivalent to the
+    -- one brought into scope by doing:
+    --
+    --     open HasProducts (Cat.hasProducts unprovable) using (_×_)
+    --
+    -- Since it doesn't we'll make the following (definitionally equivalent) ad-hoc definition.
+    _×_ : ∀ {ℓa ℓb} → Category ℓa ℓb → Category ℓa ℓb → Category ℓa ℓb
+    ℂ × 𝔻 = Cat.CatProduct.obj ℂ 𝔻
 
   record RawMonoidalCategory : Set ℓ where
     field
@@ -23,9 +27,10 @@ module _ (ℓa ℓb : Level) where
     open Category category public
     field
       {{hasProducts}} : HasProducts category
-      mempty  : Object
+      empty  : Object
       -- aka. tensor product, monoidal product.
-      mappend : Functor (category × category) category
+      append : Functor (category × category) category
+    open HasProducts hasProducts public
 
   record MonoidalCategory : Set ℓ where
     field
@@ -36,10 +41,10 @@ module _ {ℓa ℓb : Level} (ℂ : MonoidalCategory ℓa ℓb) where
   private
     ℓ = ℓa ⊔ ℓb
 
-  module MC = MonoidalCategory ℂ
-  open HasProducts MC.hasProducts
+  open MonoidalCategory ℂ public
+
   record Monoid : Set ℓ where
     field
-      carrier : MC.Object
-      mempty  : MC.Arrow (carrier × carrier)  carrier
-      mappend : MC.Arrow MC.mempty carrier
+      carrier : Object
+      mempty  : Arrow empty carrier
+      mappend : Arrow (carrier × carrier) carrier
diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda
index 8de0f34..dea2e50 100644
--- a/src/Cat/Category/NaturalTransformation.agda
+++ b/src/Cat/Category/NaturalTransformation.agda
@@ -21,15 +21,24 @@
 module Cat.Category.NaturalTransformation where
 open import Agda.Primitive
 open import Data.Product
+open import Data.Nat using (_≤_ ; z≤n ; s≤s)
+module Nat = Data.Nat
 
 open import Cubical
+open import Cubical.Sigma
+open import Cubical.NType.Properties
 
 open import Cat.Category
 open import Cat.Category.Functor hiding (identity)
+open import Cat.Wishlist
 
 module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
   (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
+
   open Category using (Object ; 𝟙)
+  private
+    module ℂ = Category ℂ
+    module 𝔻 = Category 𝔻
 
   module _ (F G : Functor ℂ 𝔻) where
     private
@@ -37,28 +46,25 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
       module G = Functor G
     -- What do you call a non-natural tranformation?
     Transformation : Set (ℓc ⊔ ℓd')
-    Transformation = (C : Object ℂ) → 𝔻 [ F.func* C , G.func* C ]
+    Transformation = (C : Object ℂ) → 𝔻 [ F.omap C , G.omap C ]
 
     Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
     Natural θ
       = {A B : Object ℂ}
       → (f : ℂ [ A , B ])
-      → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
+      → 𝔻 [ θ B ∘ F.fmap f ] ≡ 𝔻 [ G.fmap f ∘ θ A ]
 
     NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
     NaturalTransformation = Σ Transformation Natural
 
-    -- TODO: Since naturality is a mere proposition this principle can be
-    -- simplified.
+    -- Think I need propPi and that arrows are sets
+    propIsNatural : (θ : _) → isProp (Natural θ)
+    propIsNatural θ x y i {A} {B} f = 𝔻.arrowsAreSets _ _ (x f) (y f) i
+
     NaturalTransformation≡ : {α β : NaturalTransformation}
       → (eq₁ : α .proj₁ ≡ β .proj₁)
-      → (eq₂ : PathP
-          (λ i → {A B : Object ℂ} (f : ℂ [ A , B ])
-            → 𝔻 [ eq₁ i B ∘ F.func→ f ]
-            ≡ 𝔻 [ G.func→ f ∘ eq₁ i A ])
-        (α .proj₂) (β .proj₂))
       → α ≡ β
-    NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i
+    NaturalTransformation≡ eq = lemSig propIsNatural _ _ eq
 
   identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
   identityTrans F C = 𝟙 𝔻
@@ -72,8 +78,7 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
     𝔻 [ F→ f ∘ identityTrans F A ]  ∎
     where
       module F = Functor F
-      F→ = F.func→
-      module 𝔻 = Category 𝔻
+      F→ = F.fmap
 
   identity : (F : Functor ℂ 𝔻) → NaturalTransformation F F
   identity F = identityTrans F , identityNatural F
@@ -89,13 +94,27 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
     NT[_∘_] : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
     proj₁ NT[ (θ , _) ∘ (η , _) ] = T[ θ ∘ η ]
     proj₂ NT[ (θ , θNat) ∘ (η , ηNat) ] {A} {B} f = begin
-      𝔻 [ T[ θ ∘ η ] B ∘ F.func→ f ]     ≡⟨⟩
-      𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.func→ f ] ≡⟨ sym isAssociative ⟩
-      𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
-      𝔻 [ θ B ∘ 𝔻 [ G.func→ f ∘ η A ] ] ≡⟨ isAssociative ⟩
-      𝔻 [ 𝔻 [ θ B ∘ G.func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
-      𝔻 [ 𝔻 [ H.func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym isAssociative ⟩
-      𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
-      𝔻 [ H.func→ f ∘ T[ θ ∘ η ] A ]     ∎
+      𝔻 [ T[ θ ∘ η ] B ∘ F.fmap f ]     ≡⟨⟩
+      𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.fmap f ] ≡⟨ sym 𝔻.isAssociative ⟩
+      𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.fmap f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
+      𝔻 [ θ B ∘ 𝔻 [ G.fmap f ∘ η A ] ] ≡⟨ 𝔻.isAssociative ⟩
+      𝔻 [ 𝔻 [ θ B ∘ G.fmap f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
+      𝔻 [ 𝔻 [ H.fmap f ∘ θ A ] ∘ η A ] ≡⟨ sym 𝔻.isAssociative ⟩
+      𝔻 [ H.fmap f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
+      𝔻 [ H.fmap f ∘ T[ θ ∘ η ] A ]     ∎
+
+  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
-        open Category 𝔻
+      lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
+      lem = λ i f → 𝔻.arrowsAreSets _ _ (θNat f) (θNat' f) i
+
+    naturalTransformationIsSet : isSet (NaturalTransformation F G)
+    naturalTransformationIsSet = sigPresSet transformationIsSet
+      λ θ → ntypeCommulative
+      (s≤s {n = Nat.suc Nat.zero} z≤n)
+      (naturalIsProp θ)
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 5eca0e0..dff488a 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -1,54 +1,68 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Category.Product where
 
 open import Agda.Primitive
 open import Cubical
-open import Data.Product as P hiding (_×_)
+open import Data.Product as P hiding (_×_ ; proj₁ ; proj₂)
 
-open import Cat.Category
+open import Cat.Category hiding (module Propositionality)
 
-open Category
+module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 
-module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} where
-  IsProduct : (π₁ : ℂ [ obj , A ]) (π₂ : ℂ [ obj , B ]) → Set (ℓ ⊔ ℓ')
-  IsProduct π₁ π₂
-    = ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
-    → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ P.× ℂ [ π₂ ∘ x ] ≡ x₂)
+  open Category ℂ
 
--- Tip from Andrea; Consider this style for efficiency:
--- record IsProduct {ℓa ℓb : Level} (ℂ : Category ℓa ℓb)
---   {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) : Set (ℓa ⊔ ℓb) where
---   field
---      issProduct : ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
---        → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ P.× ℂ [ π₂ ∘ x ] ≡ x₂)
+  module _ (A B : Object) where
+    record RawProduct : Set (ℓa ⊔ ℓb) where
+      no-eta-equality
+      field
+        object : Object
+        proj₁  : ℂ [ object , A ]
+        proj₂  : ℂ [ object , B ]
 
--- open IsProduct
+    -- FIXME Not sure this is actually a proposition - so this name is
+    -- misleading.
+    record IsProduct (raw : RawProduct) : Set (ℓa ⊔ ℓb) where
+      open RawProduct raw public
+      field
+        isProduct : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ])
+          → ∃![ f×g ] (ℂ [ proj₁ ∘ f×g ] ≡ f P.× ℂ [ proj₂ ∘ f×g ] ≡ g)
 
-record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Object ℂ) : Set (ℓ ⊔ ℓ') where
-  no-eta-equality
-  field
-    obj : Object ℂ
-    proj₁ : ℂ [ obj , A ]
-    proj₂ : ℂ [ obj , B ]
-    {{isProduct}} : IsProduct ℂ proj₁ proj₂
+      -- | Arrow product
+      _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
+        → ℂ [ X , object ]
+      _P[_×_] π₁ π₂ = P.proj₁ (isProduct π₁ π₂)
 
-  _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
-    → ℂ [ X , obj ]
-  _P[_×_] π₁ π₂ = proj₁ (isProduct π₁ π₂)
+    record Product : Set (ℓa ⊔ ℓb) where
+      field
+        raw        : RawProduct
+        isProduct  : IsProduct raw
 
-record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
-  field
-    product : ∀ (A B : Object ℂ) → Product {ℂ = ℂ} A B
+      open IsProduct isProduct public
 
-  open Product
+  record HasProducts : Set (ℓa ⊔ ℓb) where
+    field
+      product : ∀ (A B : Object) → Product A B
 
-  _×_ : (A B : Object ℂ) → Object ℂ
-  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' B B' : Object ℂ} → ℂ [ A , A' ] → ℂ [ B , B' ]
-    → ℂ [ A × B , A' × B' ]
-  _|×|_ {A = A} {A' = A'} {B = B} {B' = B'} a b
-    = product A' B'
-      P[ ℂ [ a ∘ (product A B) .proj₁ ]
-      ×  ℂ [ b ∘ (product A B) .proj₂ ]
-      ]
+    _×_ : Object → Object → Object
+    A × B = Product.object (product A B)
+
+    -- | Parallel product of arrows
+    --
+    -- The product mentioned in awodey in Def 6.1 is not the regular product of
+    -- arrows. It's a "parallel" product
+    module _ {A A' B B' : Object} where
+      open Product
+      open Product (product A B) hiding (_P[_×_]) renaming (proj₁ to fst ; proj₂ to snd)
+      _|×|_ : ℂ [ A , A' ] → ℂ [ B , B' ] → ℂ [ A × B , A' × B' ]
+      f |×| g = product A' B'
+        P[ ℂ [ f ∘ fst ]
+        ×  ℂ [ g ∘ snd ]
+        ]
+
+module Propositionality {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where
+  -- TODO I'm not sure this is actually provable. Check with Thierry.
+  propProduct : isProp (Product ℂ A B)
+  propProduct = {!!}
+
+  propHasProducts : isProp (HasProducts ℂ)
+  propHasProducts = {!!}
diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda
index baf298b..af7567a 100644
--- a/src/Cat/Category/Yoneda.agda
+++ b/src/Cat/Category/Yoneda.agda
@@ -5,60 +5,76 @@ module Cat.Category.Yoneda where
 open import Agda.Primitive
 open import Data.Product
 open import Cubical
+open import Cubical.NType.Properties
 
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Equality
-open Equality.Data.Product
 
--- 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.Categories.Fun
+open import Cat.Categories.Sets
+open import Cat.Categories.Cat
 
-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 ℓ
-  open Fun (opposite ℂ) 𝓢
+module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
   private
-    Catℓ : Category _ _
-    Catℓ = record { raw = RawCat ℓ ℓ ; isCategory = unprovable}
-    prshf = presheaf {ℂ = ℂ}
+    𝓢 = Sets ℓ
+    open Fun (opposite ℂ) 𝓢
+    prshf = presheaf ℂ
     module ℂ = Category ℂ
 
-    _⇑_ : (A B : Category.Object Catℓ) → Category.Object Catℓ
-    A ⇑ B = (exponent A B) .obj
-      where
-        open HasExponentials (Cat.hasExponentials ℓ unprovable)
+    -- There is no (small) category of categories. So we won't use _⇑_ from
+    -- `HasExponential`
+    --
+    --     open HasExponentials (Cat.hasExponentials ℓ unprovable) using (_⇑_)
+    --
+    -- In stead we'll use an ad-hoc definition -- which is definitionally
+    -- equivalent to that other one.
+    _⇑_ = CatExponential.object
 
     module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where
-      :func→: : NaturalTransformation (prshf A) (prshf B)
-      :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.isAssociative
+      fmap : Transformation (prshf A) (prshf B)
+      fmap C x = ℂ [ f ∘ x ]
 
-    module _ {c : Category.Object ℂ} where
-      eqTrans : (λ _ → Transformation (prshf c) (prshf c))
-        [ (λ _ x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
-      eqTrans = funExt λ x → funExt λ x → ℂ.isIdentity .proj₂
+      fmapNatural : Natural (prshf A) (prshf B) fmap
+      fmapNatural g = funExt λ _ → ℂ.isAssociative
 
-      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
+      fmapNT : NaturalTransformation (prshf A) (prshf B)
+      fmapNT = fmap , fmapNatural
+
+    rawYoneda : RawFunctor ℂ Fun
+    RawFunctor.omap rawYoneda = prshf
+    RawFunctor.fmap rawYoneda = fmapNT
+    open RawFunctor rawYoneda hiding (fmap)
+
+    isIdentity : IsIdentity
+    isIdentity {c} = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq
+      where
+      eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c)
+      eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
+
+    isDistributive : IsDistributive
+    isDistributive {A} {B} {C} {f = f} {g}
+      = lemSig (propIsNatural (prshf A) (prshf C)) _ _ eq
+      where
+      T[_∘_]' = T[_∘_] {F = prshf A} {prshf B} {prshf C}
+      eqq : (X : ℂ.Object) → (x : ℂ [ X , A ])
+        → fmap (ℂ [ g ∘ f ]) X x ≡ T[ fmap g ∘ fmap f ]' X x
+      eqq X x = begin
+        fmap (ℂ [ g ∘ f ]) X x ≡⟨⟩
+        ℂ [ ℂ [ g ∘ f ] ∘ x ] ≡⟨ sym ℂ.isAssociative ⟩
+        ℂ [ g ∘ ℂ [ f ∘ x ] ] ≡⟨⟩
+        ℂ [ g ∘ fmap f X x ]  ≡⟨⟩
+        T[ fmap g ∘ fmap f ]' X x ∎
+      eq : fmap (ℂ [ g ∘ f ]) ≡ T[ fmap g ∘ fmap f ]'
+      eq = begin
+        fmap (ℂ [ g ∘ f ])    ≡⟨ funExt (λ X → funExt λ α → eqq X α) ⟩
+        T[ fmap g ∘ fmap f ]' ∎
+
+    instance
+      isFunctor : IsFunctor ℂ Fun rawYoneda
+      IsFunctor.isIdentity     isFunctor = isIdentity
+      IsFunctor.isDistributive isFunctor = isDistributive
 
   yoneda : Functor ℂ Fun
-  yoneda = record
-    { raw = record
-      { func* = prshf
-      ; func→ = :func→:
-      }
-    ; isFunctor = record
-      { isIdentity = :ident:
-      ; isDistributive = {!!}
-      }
-    }
+  Functor.raw yoneda = rawYoneda
+  Functor.isFunctor yoneda = isFunctor
diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda
index d23f52a..8385afd 100644
--- a/src/Cat/Wishlist.agda
+++ b/src/Cat/Wishlist.agda
@@ -1,15 +1,41 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Wishlist where
 
-open import Level
+open import Level hiding (suc)
+open import Cubical
 open import Cubical.NType
-open import Data.Nat using (_≤_ ; z≤n ; s≤s)
+open import Data.Nat using (_≤_ ; z≤n ; s≤s ; zero ; suc)
+open import Agda.Builtin.Sigma
 
-postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
+open import Cubical.NType.Properties
+
+step : ∀ {ℓ} {A : Set ℓ} → isContr A → (x y : A) → isContr (x ≡ y)
+step (a , contr) x y = {!p , c!}
+  -- where
+  -- p : x ≡ y
+  -- p = begin
+  --   x ≡⟨ sym (contr x) ⟩
+  --   a ≡⟨ contr y ⟩
+  --   y ∎
+  -- c : (q : x ≡ y) → p ≡ q
+  -- c q i j = contr (p {!!}) {!!}
+
+-- Contractible types have any given homotopy level.
+contrInitial : {ℓ : Level} {A : Set ℓ} → ∀ n → isContr A → HasLevel n A
+contrInitial ⟨-2⟩ contr = contr
+-- lem' (S ⟨-2⟩) (a , contr) = {!step!}
+contrInitial (S ⟨-2⟩) (a , contr) x y = begin
+  x ≡⟨ sym (contr x) ⟩
+  a ≡⟨ contr y ⟩
+  y ∎
+contrInitial (S (S n)) contr x y = {!lvl!} -- Why is this not well-founded?
+  where
+  c : isContr (x ≡ y)
+  c = step contr x y
+  lvl : HasLevel (S n) (x ≡ y)
+  lvl = contrInitial {A = x ≡ y} (S n) c
 
 module _ {ℓ : Level} {A : Set ℓ} where
-  -- This is §7.1.10 in [HoTT]. Andrea says the proof is in `cubical` but I
-  -- can't find it.
-  postulate propHasLevel : ∀ n → isProp (HasLevel n A)
-
-  isSetIsProp : isProp (isSet A)
-  isSetIsProp = propHasLevel (S (S ⟨-2⟩))
+  ntypeCommulative : ∀ {n m} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
+  ntypeCommulative {n = zero} {m} z≤n lvl = {!contrInitial ⟨ m ⟩₋₂ lvl!}
+  ntypeCommulative {n = .(suc _)} {.(suc _)} (s≤s x) lvl = {!!}