diff --git a/BACKLOG.md b/BACKLOG.md
index c791f61..bfbb32b 100644
--- a/BACKLOG.md
+++ b/BACKLOG.md
@@ -4,3 +4,11 @@ Backlog
 Prove univalence for various categories
 
 Prove postulates in `Cat.Wishlist`
+
+* Functor ✓
+* Applicative Functor ✗
+  * Lax monoidal functor ✗
+    * Monoidal functor ✗
+  * Tensorial strength ✗
+* Category ✓
+  * Monoidal category ✗
\ No newline at end of file
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 56020da..a7a3d14 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,27 @@
 Changelog
 =========
 
+Version 1.3.0
+-------------
+
+Removed unused modules and streamlined things more: All specific categories are
+in the namespace `Cat.Categories`.
+
+Lemmas about categories are now in the appropriate record e.g. `IsCategory`.
+Also changed how category reexports stuff.
+
+Rename the module Properties to Yoneda - because that's all it talks about now.
+
+Rename Opposite to opposite
+
+Add documentation in Category-module
+
+Formulation of monads in two ways; the "monoidal-" and "kleisli-" form.
+
+WIP: Equivalence of these two formulations
+
+Also use hSets in a few concrete categories rather than just pure `Set`.
+
 Version 1.2.0
 -------------
 This version is mainly a huge refactor.
diff --git a/src/Cat.agda b/src/Cat.agda
index f7c744e..20c5d69 100644
--- a/src/Cat.agda
+++ b/src/Cat.agda
@@ -1,19 +1,19 @@
 module Cat where
 
 import Cat.Category
-import Cat.CwF
 
 import Cat.Category.Functor
 import Cat.Category.Product
 import Cat.Category.Exponential
 import Cat.Category.CartesianClosed
-import Cat.Category.Pathy
-import Cat.Category.Bij
-import Cat.Category.Properties
+import Cat.Category.NaturalTransformation
+import Cat.Category.Yoneda
+import Cat.Category.Monad
 
 import Cat.Categories.Sets
--- import Cat.Categories.Cat
+import Cat.Categories.Cat
 import Cat.Categories.Rel
 import Cat.Categories.Free
 import Cat.Categories.Fun
 import Cat.Categories.Cube
+import Cat.Categories.CwF
diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index b7e306e..5a0d2dd 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -12,6 +12,7 @@ open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
 open import Cat.Category.Exponential
+open import Cat.Category.NaturalTransformation
 
 open import Cat.Equality
 open Equality.Data.Product
@@ -23,14 +24,14 @@ open Category using (Object ; 𝟙)
 module _ (ℓ ℓ' : Level) where
   private
     module _ {𝔸 𝔹 ℂ 𝔻 : Category ℓ ℓ'} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻} where
-      assc : H ∘f (G ∘f F) ≡ (H ∘f G) ∘f F
+      assc : F[ H ∘ F[ G ∘ F ] ] ≡ F[ F[ H ∘ G ] ∘ F ]
       assc = Functor≡ refl refl
 
     module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where
-      ident-r : F ∘f identity ≡ F
+      ident-r : F[ F ∘ identity ] ≡ F
       ident-r = Functor≡ refl refl
 
-      ident-l : identity ∘f F ≡ F
+      ident-l : F[ identity ∘ F ] ≡ F
       ident-l = Functor≡ refl refl
 
   RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
@@ -39,7 +40,7 @@ module _ (ℓ ℓ' : Level) where
       { Object = Category ℓ ℓ'
       ; Arrow = Functor
       ; 𝟙 = identity
-      ; _∘_ = _∘f_
+      ; _∘_ = F[_∘_]
       }
   private
     open RawCategory RawCat
@@ -176,9 +177,10 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
     Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ)
     Catℓ = Cat ℓ ℓ unprovable
     module _ (ℂ 𝔻 : Category ℓ ℓ) where
+      open Fun ℂ 𝔻 renaming (identity to idN)
       private
         :obj: : Object Catℓ
-        :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻}
+        :obj: = Fun
 
         :func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻
         :func*: (F , A) = func* F A
@@ -234,10 +236,11 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
         --   where
         --     open module 𝔻 = IsCategory (𝔻 .isCategory)
         -- Unfortunately the equational version has some ambigous arguments.
-        :ident: : :func→: {c} {c} (identityNat F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻
+
+        :ident: : :func→: {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻
         :ident: = begin
           :func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩
-          :func→: {c} {c} (identityNat F , 𝟙 ℂ)             ≡⟨⟩
+          :func→: {c} {c} (idN F , 𝟙 ℂ)             ≡⟨⟩
           𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)]           ≡⟨⟩
           𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)]                        ≡⟨ proj₂ 𝔻.isIdentity ⟩
           func→ F (𝟙 ℂ)                                    ≡⟨ F.isIdentity ⟩
diff --git a/src/Cat/CwF.agda b/src/Cat/Categories/CwF.agda
similarity index 63%
rename from src/Cat/CwF.agda
rename to src/Cat/Categories/CwF.agda
index 5735ac3..4b9ce32 100644
--- a/src/Cat/CwF.agda
+++ b/src/Cat/Categories/CwF.agda
@@ -1,4 +1,4 @@
-module Cat.CwF where
+module Cat.Categories.CwF where
 
 open import Agda.Primitive
 open import Data.Product
@@ -22,27 +22,27 @@ module _ {ℓa ℓb : Level} where
     Substitutions = Arrow ℂ
     field
       -- A functor T
-      T : Functor (Opposite ℂ) (Fam ℓa ℓb)
+      T : Functor (opposite ℂ) (Fam ℓa ℓb)
       -- Empty context
       [] : Terminal ℂ
     private
       module T = Functor T
     Type : (Γ : Object ℂ) → Set ℓa
-    Type Γ = proj₁ (T.func* Γ)
+    Type Γ = proj₁ (proj₁ (T.func* Γ))
 
     module _ {Γ : Object ℂ} {A : Type Γ} where
 
-      module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
-        k : Σ (proj₁ (func* T B) → proj₁ (func* 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)
-        k₁ = proj₁ k
-        k₂ : ({x : proj₁ (func* T B)} →
-          proj₂ (func* T B) x → proj₂ (func* T A) (k₁ x))
-        k₂ = proj₂ k
+      -- module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
+      --   k : Σ (proj₁ (func* T B) → proj₁ (func* 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)
+      --   k₁ = proj₁ k
+      --   k₂ : ({x : proj₁ (func* T B)} →
+      --     proj₂ (func* T B) x → proj₂ (func* T A) (k₁ x))
+      --   k₂ = proj₂ k
 
       record ContextComprehension : Set (ℓa ⊔ ℓb) where
         field
diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda
index 6150dd2..d100b77 100644
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@@ -3,9 +3,11 @@ module Cat.Categories.Fam where
 
 open import Agda.Primitive
 open import Data.Product
-open import Cubical
 import Function
 
+open import Cubical
+open import Cubical.Universe
+
 open import Cat.Category
 open import Cat.Equality
 
@@ -13,40 +15,54 @@ open Equality.Data.Product
 
 module _ (ℓa ℓb : Level) where
   private
-    Obj' = Σ[ A ∈ Set ℓa ] (A → Set ℓb)
-    Arr : Obj' → Obj' → Set (ℓa ⊔ ℓb)
-    Arr (A , B) (A' , B') = Σ[ f ∈ (A → A') ] ({x : A} → B x → B' (f x))
-    one : {o : Obj'} → Arr o o
-    proj₁ one = λ x → x
-    proj₂ one = λ b → b
-    _∘_ : {a b c : Obj'} → Arr b c → Arr a b → Arr a c
+    Object = Σ[ hA ∈ hSet {ℓa} ] (proj₁ hA → hSet {ℓb})
+    Arr : Object → Object → Set (ℓa ⊔ ℓb)
+    Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → proj₁ (B x) → proj₁ (B' (f x)))
+    𝟙 : {A : Object} → Arr A A
+    proj₁ 𝟙 = λ x → x
+    proj₂ 𝟙 = λ b → b
+    _∘_ : {a b c : Object} → Arr b c → Arr a b → Arr a c
     (g , g') ∘ (f , f') = g Function.∘ f , g' Function.∘ f'
-    _⟨_∘_⟩ : {a b : Obj'} → (c : Obj') → Arr b c → Arr a b → Arr a c
-    c ⟨ g ∘ f ⟩ = _∘_ {c = c} g f
-
-    module _ {A B C D : Obj'} {f : Arr A B} {g : Arr B C} {h : Arr C D} where
-      isAssociative : (D ⟨ h ∘ C ⟨ g ∘ f ⟩ ⟩) ≡ D ⟨ D ⟨ h ∘ g ⟩ ∘ f ⟩
-      isAssociative = Σ≡ refl refl
-
-    module _ {A B : Obj'} {f : Arr A B} where
-      isIdentity : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f
-      isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
-
 
     RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
     RawFam = record
-      { Object = Obj'
+      { Object = Object
       ; Arrow = Arr
-      ; 𝟙 = one
+      ; 𝟙 = λ { {A} → 𝟙 {A = A}}
       ; _∘_ = λ {a b c} → _∘_ {a} {b} {c}
       }
 
+    open RawCategory RawFam hiding (Object ; 𝟙)
+
+    isAssociative : IsAssociative
+    isAssociative = Σ≡ refl refl
+
+    isIdentity : IsIdentity λ { {A} → 𝟙 {A} }
+    isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
+
+    open import Cubical.NType.Properties
+    open import Cubical.Sigma
     instance
       isCategory : IsCategory RawFam
       isCategory = record
-        { isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {D = D} {f} {g} {h}
+        { isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {A} {B} {C} {D} {f} {g} {h}
         ; isIdentity = λ {A} {B} {f} → isIdentity {A} {B} {f = f}
-        ; arrowsAreSets = {!!}
+        ; arrowsAreSets = λ {
+          {((A , hA) , famA)}
+          {((B , hB) , famB)}
+            → setSig
+              {sA = setPi λ _ → hB}
+              {sB = λ f →
+                let
+                  helpr : isSet ((a : A) → proj₁ (famA a) → proj₁ (famB (f a)))
+                  helpr = setPi λ a → setPi λ _ → proj₂ (famB (f a))
+                  -- It's almost like above, but where the first argument is
+                  -- implicit.
+                  res : isSet ({a : A} → proj₁ (famA a) → proj₁ (famB (f a)))
+                  res = {!!}
+                in res
+              }
+          }
         ; univalent = {!!}
         }
 
diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda
index 5441abc..9a0c891 100644
--- a/src/Cat/Categories/Free.agda
+++ b/src/Cat/Categories/Free.agda
@@ -7,8 +7,6 @@ open import Data.Product
 
 open import Cat.Category
 
-open IsCategory
-
 data Path {ℓ ℓ' : Level} {A : Set ℓ} (R : A → A → Set ℓ') : (a b : A) → Set (ℓ ⊔ ℓ') where
   empty : {a : A} → Path R a a
   cons : {a b c : A} → R b c → Path R a b → Path R a c
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 3e4dcbf..2af9e55 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -2,99 +2,29 @@
 module Cat.Categories.Fun where
 
 open import Agda.Primitive
-open import Cubical
-open import Function
 open import Data.Product
-import Cubical.GradLemma
-module UIP = Cubical.GradLemma
-open import Cubical.Sigma
-open import Cubical.NType
-open import Cubical.NType.Properties
+
 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.NType.Properties
 
 open import Cat.Category
-open import Cat.Category.Functor
+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 _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
+module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
   open Category using (Object ; 𝟙)
-  open Functor
-
-  module _ (F G : Functor ℂ 𝔻) where
-    private
-      module F = Functor F
-      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 ]
-
-    Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
-    Natural θ
-      = {A B : Object ℂ}
-      → (f : ℂ [ A , B ])
-      → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
-
-    NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
-    NaturalTransformation = Σ Transformation Natural
-
-    -- NaturalTranformation : Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
-    -- NaturalTranformation = ∀ (θ : Transformation) {A B : ℂ .Object} → (f : ℂ .Arrow A B) → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A)
-
-    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
-
-  identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
-  identityTrans F C = 𝟙 𝔻
-
-  identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
-  identityNatural F {A = A} {B = B} f = begin
-    𝔻 [ identityTrans F B ∘ F→ f ]  ≡⟨⟩
-    𝔻 [ 𝟙 𝔻 ∘  F→ f ]              ≡⟨ proj₂ 𝔻.isIdentity ⟩
-    F→ f                            ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩
-    𝔻 [ F→ f ∘ 𝟙 𝔻 ]               ≡⟨⟩
-    𝔻 [ F→ f ∘ identityTrans F A ]  ∎
-    where
-      module F = Functor F
-      F→ = F.func→
-      module 𝔻 = Category 𝔻
-
-  identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F
-  identityNat F = identityTrans F , identityNatural F
-
-  module _ {F G H : Functor ℂ 𝔻} where
-    private
-      module F = Functor F
-      module G = Functor G
-      module H = Functor H
-      _∘nt_ : Transformation G H → Transformation F G → Transformation F H
-      (θ ∘nt η) C = 𝔻 [ θ C ∘ η C ]
-
-    NatComp _:⊕:_ : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
-    proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η
-    proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin
-      𝔻 [ (θ ∘nt η) 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 ∘ (θ ∘nt η) A ]     ∎
-      where
-        open Category 𝔻
-
-    NatComp = _:⊕:_
+  module NT = NaturalTransformation ℂ 𝔻
+  open NT public
 
   private
     module 𝔻 = Category 𝔻
@@ -125,11 +55,11 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       ηNat = proj₂ η'
       ζNat = proj₂ ζ'
       L : NaturalTransformation A D
-      L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ'))
+      L = (NT[_∘_] {A} {C} {D} ζ' (NT[_∘_] {A} {B} {C} η' θ'))
       R : NaturalTransformation A D
-      R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
-    _g⊕f_ = _:⊕:_ {A} {B} {C}
-    _h⊕g_ = _:⊕:_ {B} {C} {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))
@@ -147,29 +77,28 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
         f' C ∎
       eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
       eq-l C = proj₂ 𝔻.isIdentity
-      ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
+      ident-r : (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f
       ident-r = lemSig allNatural _ _ (funExt eq-r)
-      ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
+      ident-l : (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f
       ident-l = lemSig allNatural _ _ (funExt eq-l)
-      :ident:
-        : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
-        × (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
-      :ident: = ident-r , ident-l
-
+      isIdentity
+        : (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f
+        × (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f
+      isIdentity = ident-r , ident-l
   -- Functor categories. Objects are functors, arrows are natural transformations.
   RawFun : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
   RawFun = record
     { Object = Functor ℂ 𝔻
     ; Arrow = NaturalTransformation
-    ; 𝟙 = λ {F} → identityNat F
-    ; _∘_ = λ {F G H} → _:⊕:_ {F} {G} {H}
+    ; 𝟙 = λ {F} → NT.identity F
+    ; _∘_ = λ {F G H} → NT[_∘_] {F} {G} {H}
     }
 
   instance
     :isCategory: : IsCategory RawFun
     :isCategory: = record
       { isAssociative = λ {A B C D} → :isAssociative: {A} {B} {C} {D}
-      ; isIdentity = λ {A B} → :ident: {A} {B}
+      ; isIdentity = λ {A B} → isIdentity {A} {B}
       ; arrowsAreSets = λ {F} {G} → naturalTransformationIsSets {F} {G}
       ; univalent = {!!}
       }
@@ -179,12 +108,13 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   open import Cat.Categories.Sets
+  open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
 
   -- Restrict the functors to Presheafs.
   RawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
   RawPresh = record
     { Object = Presheaf ℂ
     ; Arrow = NaturalTransformation
-    ; 𝟙 = λ {F} → identityNat F
-    ; _∘_ = λ {F G H} → NatComp {F = F} {G = G} {H = H}
+    ; 𝟙 = λ {F} → identity F
+    ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
     }
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 035c743..0ed99a3 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -88,7 +88,7 @@ module _ {ℓa ℓb : Level} where
 
     -- Contravariant Presheaf
     Presheaf : Set (ℓa ⊔ lsuc ℓb)
-    Presheaf = Functor (Opposite ℂ) (𝓢𝓮𝓽 ℓb)
+    Presheaf = Functor (opposite ℂ) (𝓢𝓮𝓽 ℓb)
 
   -- The "co-yoneda" embedding.
   representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
@@ -106,7 +106,7 @@ module _ {ℓa ℓb : Level} where
       open Category ℂ
 
   -- Alternate name: `yoneda`
-  presheaf : {ℂ : Category ℓa ℓb} → Category.Object (Opposite ℂ) → Presheaf ℂ
+  presheaf : {ℂ : Category ℓa ℓb} → Category.Object (opposite ℂ) → Presheaf ℂ
   presheaf {ℂ = ℂ} B = record
     { raw = record
       { func* = λ A → ℂ [ A , B ] , arrowsAreSets
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index cec311d..d70fc65 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -1,3 +1,32 @@
+-- | Univalent categories
+--
+-- This module defines:
+--
+-- Categories
+-- ==========
+--
+-- Types
+-- ------
+--
+-- Object, Arrow
+--
+-- Data
+-- ----
+-- 𝟙; the identity arrow
+-- _∘_; function composition
+--
+-- Laws
+-- ----
+--
+-- associativity, identity, arrows form sets, univalence.
+--
+-- Lemmas
+-- ------
+--
+-- 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
@@ -16,6 +45,11 @@ open import Cubical.NType.Properties using ( propIsEquiv )
 
 open import Cat.Wishlist
 
+-----------------
+-- * Utilities --
+-----------------
+
+-- | Unique existensials.
 ∃! : ∀ {a b} {A : Set a}
   → (A → Set b) → Set (a ⊔ b)
 ∃! = ∃!≈ _≡_
@@ -25,6 +59,15 @@ open import Cat.Wishlist
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
+-----------------
+-- * Categories --
+-----------------
+
+-- | Raw categories
+--
+-- This record desribes the data that a category consist of as well as some laws
+-- about these. The laws defined are the types the propositions - not the
+-- witnesses to them!
 record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   no-eta-equality
   field
@@ -35,12 +78,18 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
 
   infixl 10 _∘_
 
+  -- | Operations on data
+
   domain : { a b : Object } → Arrow a b → Object
   domain {a = a} _ = a
 
   codomain : { a b : Object } → Arrow a b → Object
   codomain {b = b} _ = b
 
+  -- | Laws about the data
+
+  -- TODO: 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}
     → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
@@ -91,14 +140,18 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
     id-to-iso : (A B : Object) → A ≡ B → A ≅ B
     id-to-iso A B eq = transp (\ i → A ≅ eq i) (idIso A)
 
-    -- TODO: might want to implement isEquiv
-    -- differently, there are 3
-    -- equivalent formulations in the book.
     Univalent : Set (ℓa ⊔ ℓb)
     Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
 
+-- | The mere proposition of being a category.
+--
+-- Also defines a few lemmas:
+--
+--     iso-is-epi  : Isomorphism f → Epimorphism {X = X} f
+--     iso-is-mono : Isomorphism f → Monomorphism {X = X} f
+--
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
-  open RawCategory ℂ
+  open RawCategory ℂ public
   open Univalence ℂ public
   field
     isAssociative : IsAssociative
@@ -106,11 +159,42 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     arrowsAreSets : ArrowsAreSets
     univalent     : Univalent isIdentity
 
--- `IsCategory` is a mere proposition.
+  -- Some common lemmas about categories.
+  module _ {A B : Object} {X : Object} (f : Arrow A B) where
+    iso-is-epi : Isomorphism f → Epimorphism {X = X} f
+    iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
+      g₀              ≡⟨ sym (fst isIdentity) ⟩
+      g₀ ∘ 𝟙          ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
+      g₀ ∘ (f ∘ f-)   ≡⟨ isAssociative ⟩
+      (g₀ ∘ f) ∘ f-   ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩
+      (g₁ ∘ f) ∘ f-   ≡⟨ sym isAssociative ⟩
+      g₁ ∘ (f ∘ f-)   ≡⟨ cong (_∘_ g₁) right-inv ⟩
+      g₁ ∘ 𝟙          ≡⟨ fst isIdentity ⟩
+      g₁              ∎
+
+    iso-is-mono : Isomorphism f → Monomorphism {X = X} f
+    iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq =
+      begin
+      g₀            ≡⟨ sym (snd isIdentity) ⟩
+      𝟙 ∘ g₀        ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩
+      (f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩
+      f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩
+      f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩
+      (f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩
+      𝟙 ∘ g₁        ≡⟨ snd isIdentity ⟩
+      g₁            ∎
+
+    iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
+    iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso
+
+-- | Propositionality of being a category
+--
+-- 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
-    open IsCategory ℂ
+    open IsCategory ℂ using (isAssociative ; arrowsAreSets ; isIdentity ; Univalent)
     open import Cubical.NType
     open import Cubical.NType.Properties
 
@@ -189,14 +273,17 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
   propIsCategory : isProp (IsCategory C)
   propIsCategory = done
 
+-- | Univalent categories
+--
+-- Just bundles up the data with witnesses inhabting the propositions.
 record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   field
     raw : RawCategory ℓa ℓb
     {{isCategory}} : IsCategory raw
 
-  open RawCategory raw public
   open IsCategory isCategory public
 
+-- | Syntax for arrows- and composition in a given category.
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   open Category ℂ
   _[_,_] : (A : Object) → (B : Object) → Set ℓb
@@ -205,48 +292,48 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   _[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C
   _[_∘_] = _∘_
 
-module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-  private
+-- | The opposite category
+--
+-- The opposite category is the category where the direction of the arrows are
+-- flipped.
+module Opposite {ℓa ℓb : Level} where
+  module _ (ℂ : Category ℓa ℓb) where
     open Category ℂ
+    private
+      opRaw : RawCategory ℓa ℓb
+      RawCategory.Object opRaw = Object
+      RawCategory.Arrow  opRaw = Function.flip Arrow
+      RawCategory.𝟙      opRaw = 𝟙
+      RawCategory._∘_    opRaw = Function.flip _∘_
 
-    OpRaw : RawCategory ℓa ℓb
-    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 = {!!}
 
-    OpIsCategory : IsCategory OpRaw
-    IsCategory.isAssociative OpIsCategory = sym isAssociative
-    IsCategory.isIdentity OpIsCategory = swap isIdentity
-    IsCategory.arrowsAreSets OpIsCategory = arrowsAreSets
-    IsCategory.univalent OpIsCategory = {!!}
+    opposite : Category ℓa ℓb
+    raw opposite = opRaw
+    Category.isCategory opposite = opIsCategory
 
-  Opposite : Category ℓa ℓb
-  raw Opposite = OpRaw
-  Category.isCategory Opposite = OpIsCategory
+  -- 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
+  -- definitionally equal. I.e; a thing that would normally be provable in one
+  -- line now takes 13!! Admittedly it's a simple proof.
+  module _ {ℂ : Category ℓa ℓb} where
+    open Category ℂ
+    private
+      -- Since they really are definitionally equal we just need to pick apart
+      -- the data-type.
+      rawInv : Category.raw (opposite (opposite ℂ)) ≡ raw
+      RawCategory.Object   (rawInv _) = Object
+      RawCategory.Arrow    (rawInv _) = Arrow
+      RawCategory.𝟙        (rawInv _) = 𝟙
+      RawCategory._∘_      (rawInv _) = _∘_
 
--- 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
--- definitionally equal. I.e; a thing that would normally be provable in one
--- line now takes more than 20!!
-module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
-  private
-    open RawCategory
-    module C = Category ℂ
-    rawOp : Category.raw (Opposite (Opposite ℂ)) ≡ Category.raw ℂ
-    Object (rawOp _) = C.Object
-    Arrow (rawOp _) = C.Arrow
-    𝟙 (rawOp _) = C.𝟙
-    _∘_ (rawOp _) = C._∘_
-    open Category
-    open IsCategory
-    module IsCat = IsCategory (ℂ .isCategory)
-    rawIsCat : (i : I) → IsCategory (rawOp i)
-    isAssociative (rawIsCat i) = IsCat.isAssociative
-    isIdentity (rawIsCat i) = IsCat.isIdentity
-    arrowsAreSets (rawIsCat i) = IsCat.arrowsAreSets
-    univalent (rawIsCat i) = IsCat.univalent
+    -- TODO: Define and use Monad≡
+    oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ
+    Category.raw        (oppositeIsInvolution i) = rawInv i
+    Category.isCategory (oppositeIsInvolution x) = {!!}
 
-  Opposite-is-involution : Opposite (Opposite ℂ) ≡ ℂ
-  raw (Opposite-is-involution i) = rawOp i
-  isCategory (Opposite-is-involution i) = rawIsCat i
+open Opposite public
diff --git a/src/Cat/Category/Bij.agda b/src/Cat/Category/Bij.agda
deleted file mode 100644
index c611c6c..0000000
--- a/src/Cat/Category/Bij.agda
+++ /dev/null
@@ -1,46 +0,0 @@
-{-# OPTIONS --cubical --allow-unsolved-metas #-}
-
-module Cat.Category.Bij where
-
-open import Cubical hiding ( Id )
-open import Cubical.FromStdLib
-
-module _ {A : Set} {a : A} {P : A → Set} where
-  Q : A → Set
-  Q a = A
-
-  t : Σ[ a ∈ A ] P a → Q a
-  t (a , Pa) = a
-  u : Q a → Σ[ a ∈ A ] P a
-  u a = a , {!!}
-
-  tu-bij : (a : Q a) → (t ∘ u) a ≡ a
-  tu-bij a = refl
-
-  v : P a → Q a
-  v x = {!!}
-  w : Q a → P a
-  w x = {!!}
-
-  vw-bij : (a : P a) → (w ∘ v) a ≡ a
-  vw-bij a = {!!}
-  -- tubij a with (t ∘ u) a
-  -- ... | q = {!!}
-
-  data Id {A : Set} (a : A) : Set where
-    id : A → Id a
-
-  data Id' {A : Set} (a : A) : Set where
-    id' : A → Id' a
-
-  T U : Set
-  T = Id a
-  U = Id' a
-
-  f : T → U
-  f (id x) = id' x
-  g : U → T
-  g (id' x) = id x
-
-  fg-bij : (x : U) → (f ∘ g) x ≡ x
-  fg-bij (id' x) = {!!}
diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index 0269df9..d648728 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -51,7 +51,7 @@ module _
     (F : RawFunctor ℂ 𝔻)
     where
   private
-    module 𝔻 = IsCategory (isCategory 𝔻)
+    module 𝔻 = Category 𝔻
 
   propIsFunctor : isProp (IsFunctor _ _ F)
   propIsFunctor isF0 isF1 i = record
@@ -69,7 +69,7 @@ module _
     {F : I → RawFunctor ℂ 𝔻}
     where
   private
-    module 𝔻 = IsCategory (isCategory 𝔻)
+    module 𝔻 = Category 𝔻
   IsProp' : {ℓ : Level} (A : I → Set ℓ) → Set ℓ
   IsProp' A = (a0 : A i0) (a1 : A i1) → A [ a0 ≡ a1 ]
 
@@ -124,8 +124,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
         ; isDistributive = dist
         }
 
-  _∘f_ : Functor A C
-  raw _∘f_ = _∘fr_
+  F[_∘_] : Functor A C
+  raw F[_∘_] = _∘fr_
 
 -- The identity functor
 identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
new file mode 100644
index 0000000..92805e0
--- /dev/null
+++ b/src/Cat/Category/Monad.agda
@@ -0,0 +1,333 @@
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
+module Cat.Category.Monad where
+
+open import Agda.Primitive
+
+open import Data.Product
+
+open import Cubical
+
+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 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
+module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
+  private
+    open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
+    open Functor using (func* ; func→)
+    module M = Monoidal ℂ
+    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
+
+      forthRaw : K.RawMonad
+      Kraw.RR forthRaw = RR
+      Kraw.ζ  forthRaw = ζ
+      Kraw.rr forthRaw = rr
+
+    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
+
+      forthIsMonad : K.IsMonad (forthRaw raw)
+      Kis.isIdentity forthIsMonad = isIdentity
+      Kis.isNatural forthIsMonad = isNatural
+      Kis.isDistributive forthIsMonad = isDistributive
+
+    forth : M.Monad → K.Monad
+    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 = {!!}
+
+      backRaw : M.RawMonad
+      Mraw.R    backRaw = R
+      Mraw.ηNat backRaw = ηNat
+      Mraw.μNat backRaw = μNat
+
+    module _ (m : K.Monad) where
+      open K.Monad m
+      open M.RawMonad (backRaw m)
+      module Mis = M.IsMonad
+
+      backIsMonad : M.IsMonad (backRaw m)
+      backIsMonad = {!!}
+
+    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)
+      forthRawEq : forthRaw (backRaw m) ≡ K.Monad.raw m
+      K.RawMonad.RR (forthRawEq _) = RR
+      K.RawMonad.ζ  (forthRawEq _) = ζ
+      -- stuck
+      K.RawMonad.rr (forthRawEq 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)
+      backRawEq : backRaw (forth m) ≡ M.Monad.raw m
+      -- stuck
+      M.RawMonad.R    (backRawEq i) = {!!}
+      M.RawMonad.ηNat (backRawEq i) = {!!}
+      M.RawMonad.μNat (backRawEq 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
+
+  Monoidal≃Kleisli : M.Monad ≃ K.Monad
+  Monoidal≃Kleisli = forth , eqv
diff --git a/src/Cat/Category/Monoid.agda b/src/Cat/Category/Monoid.agda
new file mode 100644
index 0000000..3323487
--- /dev/null
+++ b/src/Cat/Category/Monoid.agda
@@ -0,0 +1,45 @@
+module Cat.Category.Monoid where
+
+open import Agda.Primitive
+
+open import Cat.Category
+open import Cat.Category.Product
+open import Cat.Category.Functor
+import Cat.Categories.Cat as Cat
+
+-- TODO: Incorrect!
+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)
+
+  record RawMonoidalCategory : Set ℓ where
+    field
+      category : Category ℓa ℓb
+    open Category category public
+    field
+      {{hasProducts}} : HasProducts category
+      mempty  : Object
+      -- aka. tensor product, monoidal product.
+      mappend : Functor (category × category) category
+
+  record MonoidalCategory : Set ℓ where
+    field
+      raw : RawMonoidalCategory
+    open RawMonoidalCategory raw public
+
+module _ {ℓa ℓb : Level} (ℂ : MonoidalCategory ℓa ℓb) where
+  private
+    ℓ = ℓa ⊔ ℓb
+
+  module MC = MonoidalCategory ℂ
+  open HasProducts MC.hasProducts
+  record Monoid : Set ℓ where
+    field
+      carrier : MC.Object
+      mempty  : MC.Arrow (carrier × carrier)  carrier
+      mappend : MC.Arrow MC.mempty carrier
diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda
new file mode 100644
index 0000000..8de0f34
--- /dev/null
+++ b/src/Cat/Category/NaturalTransformation.agda
@@ -0,0 +1,101 @@
+-- This module Essentially just provides the data for natural transformations
+--
+-- This includes:
+--
+-- The types:
+--
+-- * Transformation        - a family of functors
+-- * Natural               - naturality condition for transformations
+-- * NaturalTransformation - both of the above
+--
+-- Elements of the above:
+--
+-- * identityTrans   - the identity transformation
+-- * identityNatural - naturality for the above
+-- * identity        - both of the above
+--
+-- Functions for manipulating the above:
+--
+-- * A composition operator.
+{-# OPTIONS --allow-unsolved-metas --cubical #-}
+module Cat.Category.NaturalTransformation where
+open import Agda.Primitive
+open import Data.Product
+
+open import Cubical
+
+open import Cat.Category
+open import Cat.Category.Functor hiding (identity)
+
+module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
+  (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
+  open Category using (Object ; 𝟙)
+
+  module _ (F G : Functor ℂ 𝔻) where
+    private
+      module F = Functor F
+      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 ]
+
+    Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
+    Natural θ
+      = {A B : Object ℂ}
+      → (f : ℂ [ A , B ])
+      → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
+
+    NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
+    NaturalTransformation = Σ Transformation Natural
+
+    -- TODO: Since naturality is a mere proposition this principle can be
+    -- simplified.
+    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
+
+  identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
+  identityTrans F C = 𝟙 𝔻
+
+  identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
+  identityNatural F {A = A} {B = B} f = begin
+    𝔻 [ identityTrans F B ∘ F→ f ]  ≡⟨⟩
+    𝔻 [ 𝟙 𝔻 ∘  F→ f ]              ≡⟨ proj₂ 𝔻.isIdentity ⟩
+    F→ f                            ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩
+    𝔻 [ F→ f ∘ 𝟙 𝔻 ]               ≡⟨⟩
+    𝔻 [ F→ f ∘ identityTrans F A ]  ∎
+    where
+      module F = Functor F
+      F→ = F.func→
+      module 𝔻 = Category 𝔻
+
+  identity : (F : Functor ℂ 𝔻) → NaturalTransformation F F
+  identity F = identityTrans F , identityNatural F
+
+  module _ {F G H : Functor ℂ 𝔻} where
+    private
+      module F = Functor F
+      module G = Functor G
+      module H = Functor H
+    T[_∘_] : Transformation G H → Transformation F G → Transformation F H
+    T[ θ ∘ η ] C = 𝔻 [ θ C ∘ η C ]
+
+    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 ]     ∎
+      where
+        open Category 𝔻
diff --git a/src/Cat/Category/Pathy.agda b/src/Cat/Category/Pathy.agda
deleted file mode 100644
index 2764999..0000000
--- a/src/Cat/Category/Pathy.agda
+++ /dev/null
@@ -1,53 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module Cat.Category.Pathy where
-
-open import Level
-open import Cubical
-
-{-
-module _ {ℓ ℓ'} {A : Set ℓ} {x : A}
-  (P : ∀ y → x ≡ y → Set ℓ') (d : P x ((λ i → x))) where
-  pathJ' : (y : A) → (p : x ≡ y) → P y p
-  pathJ' _ p = transp (λ i → uncurry P (contrSingl p i)) d
-
-  pathJprop' : pathJ' _ refl ≡ d
-  pathJprop' i
-    = primComp (λ _ → P x refl) i (λ {j (i = i1) → d}) d
-
-
-module _ {ℓ ℓ'} {A : Set ℓ}
-  (P : (x y : A) → x ≡ y → Set ℓ') (d : (x : A) → P x x refl) where
-  pathJ'' : (x y : A) → (p : x ≡ y) → P x y p
-  pathJ'' _ _ p = transp (λ i →
-    let
-      P' = uncurry P
-      q  = (contrSingl p i)
-    in
-      {!uncurry (uncurry P)!} ) d
--}
-
-module _ {ℓ ℓ'} {A : Set ℓ}
-  (C : (x y : A) → x ≡ y → Set ℓ')
-  (c : (x : A) → C x x refl) where
-
-  =-ind : (x y : A) → (p : x ≡ y) → C x y p
-  =-ind x y p = pathJ (C x) (c x) y p
-
-module _ {ℓ ℓ' : Level} {A : Set ℓ} {P : A → Set ℓ} {x y : A} where
-  private
-    D : (x y : A) → (x ≡ y) → Set ℓ
-    D x y p = P x → P y
-
-    id : {ℓ : Level} → {A : Set ℓ} → A → A
-    id x = x
-
-    d : (x : A) → D x x refl
-    d x = id {A = P x}
-
-  -- the p refers to the third argument
-  liftP : x ≡ y → P x → P y
-  liftP p = =-ind D d x y p
-
-  -- lift' : (u : P x) → (p : x ≡ y) → (x , u) ≡ (y , liftP p u)
-  -- lift' u p = {!!}
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Yoneda.agda
similarity index 56%
rename from src/Cat/Category/Properties.agda
rename to src/Cat/Category/Yoneda.agda
index 190592e..baf298b 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Yoneda.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --allow-unsolved-metas --cubical #-}
 
-module Cat.Category.Properties where
+module Cat.Category.Yoneda where
 
 open import Agda.Primitive
 open import Data.Product
@@ -8,39 +8,9 @@ open import Cubical
 
 open import Cat.Category
 open import Cat.Category.Functor
-open import Cat.Categories.Sets
 open import Cat.Equality
 open Equality.Data.Product
 
-module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where
-  open Category ℂ
-
-  iso-is-epi : Isomorphism f → Epimorphism {X = X} f
-  iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
-    g₀              ≡⟨ sym (proj₁ isIdentity) ⟩
-    g₀ ∘ 𝟙          ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
-    g₀ ∘ (f ∘ f-)   ≡⟨ isAssociative ⟩
-    (g₀ ∘ f) ∘ f-   ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩
-    (g₁ ∘ f) ∘ f-   ≡⟨ sym isAssociative ⟩
-    g₁ ∘ (f ∘ f-)   ≡⟨ cong (_∘_ g₁) right-inv ⟩
-    g₁ ∘ 𝟙          ≡⟨ proj₁ isIdentity ⟩
-    g₁              ∎
-
-  iso-is-mono : Isomorphism f → Monomorphism {X = X} f
-  iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq =
-    begin
-    g₀            ≡⟨ sym (proj₂ isIdentity) ⟩
-    𝟙 ∘ g₀        ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩
-    (f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩
-    f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩
-    f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩
-    (f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩
-    𝟙 ∘ g₁        ≡⟨ proj₂ isIdentity ⟩
-    g₁            ∎
-
-  iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
-  iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso
-
 -- 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)
@@ -52,6 +22,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat
   open import Cat.Category.Exponential
   open Functor
   𝓢 = Sets ℓ
+  open Fun (opposite ℂ) 𝓢
   private
     Catℓ : Category _ _
     Catℓ = record { raw = RawCat ℓ ℓ ; isCategory = unprovable}
@@ -80,7 +51,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat
           eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c)
           eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
 
-  yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = 𝓢})
+  yoneda : Functor ℂ Fun
   yoneda = record
     { raw = record
       { func* = prshf