From a321a9c8b2831001327ec37620d754dda26d3a08 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 13:36:54 +0100
Subject: [PATCH 01/31] Use hLevels in Fam

---
 src/Cat/Categories/Fam.agda | 43 ++++++++++++++++++-------------------
 1 file changed, 21 insertions(+), 22 deletions(-)

diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda
index 6150dd2..7727a6d 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,38 +15,35 @@ 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
+
     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 = {!!}
         ; univalent = {!!}

From 5796b791b8f110503caf82c1e4e9f08f175fe7fc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 13:59:35 +0100
Subject: [PATCH 02/31] Almost prove that arrows are sets in the cateogry of
 families

---
 src/Cat/Categories/Fam.agda | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda
index 7727a6d..d100b77 100644
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@@ -40,12 +40,29 @@ module _ (ℓa ℓb : Level) where
     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 {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 = {!!}
         }
 

From 39284b8d99812c42f242b7762aa7e5cc918fb58e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 14:13:55 +0100
Subject: [PATCH 03/31] Changes in CwF

---
 src/Cat/CwF.agda | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/Cat/CwF.agda b/src/Cat/CwF.agda
index 5735ac3..3954ea5 100644
--- a/src/Cat/CwF.agda
+++ b/src/Cat/CwF.agda
@@ -28,21 +28,21 @@ module _ {ℓa ℓb : Level} where
     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

From f5dded9561fdf30f69a3b3864b58d3a293586d8b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 16:41:17 +0100
Subject: [PATCH 04/31] Do not use IsCategory directly

---
 src/Cat/Category/Functor.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index 0269df9..a55e6bd 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 ]
 

From 689a6467c6e0fdcf405959212b80983e28eab9b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 17:33:09 +0100
Subject: [PATCH 05/31] Move stuff about natural transformations to own module

---
 src/Cat.agda                                |   4 +-
 src/Cat/Categories/Cat.agda                 |   9 +-
 src/Cat/Categories/Fun.agda                 | 114 ++++----------------
 src/Cat/Category/Monad.agda                 |   8 ++
 src/Cat/Category/NaturalTransformation.agda |  82 ++++++++++++++
 src/Cat/Category/Properties.agda            |   3 +-
 6 files changed, 123 insertions(+), 97 deletions(-)
 create mode 100644 src/Cat/Category/Monad.agda
 create mode 100644 src/Cat/Category/NaturalTransformation.agda

diff --git a/src/Cat.agda b/src/Cat.agda
index f7c744e..0619b51 100644
--- a/src/Cat.agda
+++ b/src/Cat.agda
@@ -7,12 +7,14 @@ import Cat.Category.Functor
 import Cat.Category.Product
 import Cat.Category.Exponential
 import Cat.Category.CartesianClosed
+import Cat.Category.NaturalTransformation
 import Cat.Category.Pathy
 import Cat.Category.Bij
 import Cat.Category.Properties
+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
diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index b7e306e..2bb566e 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
@@ -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/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 3e4dcbf..70dab6c 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 𝔻
@@ -147,21 +77,20 @@ 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 : (_:⊕:_ {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 : (_:⊕:_ {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
+        : (_:⊕:_ {A} {A} {B} f (NT.identity A)) ≡ f
+        × (_:⊕:_ {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} → NT.identity F
     ; _∘_ = λ {F G H} → _:⊕:_ {F} {G} {H}
     }
 
@@ -169,7 +98,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     :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} → identity F
     ; _∘_ = λ {F G H} → NatComp {F = F} {G = G} {H = H}
     }
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
new file mode 100644
index 0000000..6c73f06
--- /dev/null
+++ b/src/Cat/Category/Monad.agda
@@ -0,0 +1,8 @@
+{-# OPTIONS --cubical #-}
+module Cat.Category.Monad where
+
+open import Cubical
+
+open import Cat.Category
+open import Cat.Category.Functor
+open import Cat.Categories.Fun
diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda
new file mode 100644
index 0000000..b56694c
--- /dev/null
+++ b/src/Cat/Category/NaturalTransformation.agda
@@ -0,0 +1,82 @@
+{-# 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
+
+    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
+      _∘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 = _:⊕:_
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index 190592e..4eeb6c3 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -52,6 +52,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 +81,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

From dd11b69c71e74e9d177ae09c4bbf8658e625b736 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 17:37:27 +0100
Subject: [PATCH 06/31] Documentation for natural transformations

---
 src/Cat/Category/NaturalTransformation.agda | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda
index b56694c..4130a19 100644
--- a/src/Cat/Category/NaturalTransformation.agda
+++ b/src/Cat/Category/NaturalTransformation.agda
@@ -1,3 +1,22 @@
+-- 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
@@ -29,6 +48,8 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
     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

From cb8533b84a81733d33ce5ecb88c0659aa1fe0d94 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 17:43:38 +0100
Subject: [PATCH 07/31] Rename natural transformation composition

---
 src/Cat/Categories/Fun.agda                 | 20 ++++++++++----------
 src/Cat/Category/NaturalTransformation.agda | 16 +++++++---------
 2 files changed, 17 insertions(+), 19 deletions(-)

diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 70dab6c..ac7fd8a 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -55,11 +55,11 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
       η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))
@@ -77,13 +77,13 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
         f' C ∎
       eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
       eq-l C = proj₂ 𝔻.isIdentity
-      ident-r : (_:⊕:_ {A} {A} {B} f (NT.identity 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} (NT.identity B) f) ≡ f
+      ident-l : (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f
       ident-l = lemSig allNatural _ _ (funExt eq-l)
       isIdentity
-        : (_:⊕:_ {A} {A} {B} f (NT.identity A)) ≡ f
-        × (_:⊕:_ {A} {B} {B} (NT.identity B) f) ≡ f
+        : (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')
@@ -91,7 +91,7 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
     { Object = Functor ℂ 𝔻
     ; Arrow = NaturalTransformation
     ; 𝟙 = λ {F} → NT.identity F
-    ; _∘_ = λ {F G H} → _:⊕:_ {F} {G} {H}
+    ; _∘_ = λ {F G H} → NT[_∘_] {F} {G} {H}
     }
 
   instance
@@ -116,5 +116,5 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
     { Object = Presheaf ℂ
     ; Arrow = NaturalTransformation
     ; 𝟙 = λ {F} → identity F
-    ; _∘_ = λ {F G H} → NatComp {F = F} {G = G} {H = H}
+    ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
     }
diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda
index 4130a19..8de0f34 100644
--- a/src/Cat/Category/NaturalTransformation.agda
+++ b/src/Cat/Category/NaturalTransformation.agda
@@ -83,21 +83,19 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
       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 ]
+    T[_∘_] : Transformation G H → Transformation F G → Transformation F H
+    T[ θ ∘ η ] 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 ]     ≡⟨⟩
+    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 ∘ (θ ∘nt η) A ]     ∎
+      𝔻 [ H.func→ f ∘ T[ θ ∘ η ] A ]     ∎
       where
         open Category 𝔻
-
-    NatComp = _:⊕:_

From 8527fe0df421b0e684a7693ce3646652447dd829 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 12:52:16 +0100
Subject: [PATCH 08/31] Rename functor composition - implement monads...

In their monoidal form.
---
 src/Cat/Category/Functor.agda |  5 +--
 src/Cat/Category/Monad.agda   | 65 ++++++++++++++++++++++++++++++++++-
 2 files changed, 67 insertions(+), 3 deletions(-)

diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index a55e6bd..7a2e565 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -124,8 +124,9 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
         ; isDistributive = dist
         }
 
-  _∘f_ : Functor A C
-  raw _∘f_ = _∘fr_
+  F[_∘_] _∘f_ : Functor A C
+  raw F[_∘_] = _∘fr_
+  _∘f_ = F[_∘_]
 
 -- The identity functor
 identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 6c73f06..acd54fc 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -1,8 +1,71 @@
 {-# OPTIONS --cubical #-}
 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
+open import Cat.Category.Functor as F
+open import Cat.Category.NaturalTransformation
 open import Cat.Categories.Fun
+
+-- "A monad in the monoidal form" [vlad]
+module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  private
+    ℓ = ℓa ⊔ ℓb
+
+  open Category ℂ hiding (IsAssociative)
+  open NaturalTransformation ℂ ℂ
+  record RawMonad : Set ℓ where
+    field
+      R : Functor ℂ ℂ
+      -- pure
+      ηNat : NaturalTransformation F.identity R
+      -- (>=>)
+      μNat : NaturalTransformation F[ R ∘ R ] R
+
+    module R  = Functor R
+    module RR = Functor F[ R ∘ R ]
+    private
+      module _ {X : Object} where
+        -- module IdRX = Functor (F.identity {C = RX})
+
+        η : Transformation F.identity R
+        η = proj₁ ηNat
+        ηX  : ℂ [ X                    , R.func* X ]
+        ηX = η X
+        RηX : ℂ [ R.func* X            , R.func* (R.func* X) ] -- ℂ [ R.func* X , {!R.func* (R.func* X))!} ]
+        RηX = R.func→ ηX
+        ηRX = η (R.func* X)
+        IdRX : Arrow (R.func* X) (R.func* X)
+        IdRX = 𝟙 {R.func* X}
+
+        μ : Transformation F[ R ∘ R ] R
+        μ = proj₁ μNat
+        μX  : ℂ [ RR.func* X           , R.func* X ]
+        μX = μ X
+        RμX : ℂ [ R.func* (RR.func* X) , RR.func* X ]
+        RμX = R.func→ μX
+        μRX : ℂ [ RR.func* (R.func* X) , R.func* (R.func* X) ]
+        μRX = μ (R.func* X)
+
+        IsAssociative' : Set _
+        IsAssociative' = ℂ [ μX ∘ RμX ] ≡ ℂ [ μX ∘ μRX ]
+        IsInverse' : Set _
+        IsInverse'
+          = ℂ [ μX ∘ ηRX ] ≡ IdRX
+          × ℂ [ μX ∘ RηX ] ≡ IdRX
+
+    -- 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

From 0ca11874bcff4ad22de89b06faf406602803fb15 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 12:55:08 +0100
Subject: [PATCH 09/31] Remove old name for functor composition

---
 src/Cat/Categories/Cat.agda   | 8 ++++----
 src/Cat/Category/Functor.agda | 3 +--
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 2bb566e..5a0d2dd 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -24,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 (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
@@ -40,7 +40,7 @@ module _ (ℓ ℓ' : Level) where
       { Object = Category ℓ ℓ'
       ; Arrow = Functor
       ; 𝟙 = identity
-      ; _∘_ = _∘f_
+      ; _∘_ = F[_∘_]
       }
   private
     open RawCategory RawCat
diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index 7a2e565..d648728 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -124,9 +124,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
         ; isDistributive = dist
         }
 
-  F[_∘_] _∘f_ : Functor A C
+  F[_∘_] : Functor A C
   raw F[_∘_] = _∘fr_
-  _∘f_ = F[_∘_]
 
 -- The identity functor
 identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C

From 4ec13fe5094190519604730acfa8bb0d5d10940a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 14:00:52 +0100
Subject: [PATCH 10/31] Implement monads in the kleisli form

---
 BACKLOG.md                  |  8 ++++++++
 src/Cat/Category/Monad.agda | 37 +++++++++++++++++++++++++++++++++++--
 2 files changed, 43 insertions(+), 2 deletions(-)

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/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index acd54fc..0400ba1 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -27,9 +27,10 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       -- (>=>)
       μNat : NaturalTransformation F[ R ∘ R ] R
 
-    module R  = Functor R
-    module RR = Functor F[ R ∘ R ]
+
     private
+      module R  = Functor R
+      module RR = Functor F[ R ∘ R ]
       module _ {X : Object} where
         -- module IdRX = Functor (F.identity {C = RX})
 
@@ -69,3 +70,35 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     field
       isAssociative : IsAssociative
       isInverse : IsInverse
+
+-- "A monad in the Kleisli form" [vlad]
+module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  private
+    ℓ = ℓa ⊔ ℓb
+
+  open Category ℂ hiding (IsIdentity)
+  record RawMonad : Set ℓ where
+    field
+      RR : Object → Object
+      η : {X : Object} → ℂ [ X , RR X ]
+      rr : {X Y : Object} → ℂ [ X , RR Y ] → ℂ [ RR X , RR Y ]
+    -- Name suggestions are welcome!
+    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 ])
+
+  record IsMonad (raw : RawMonad) : Set ℓ where
+    open RawMonad raw public
+    field
+      isIdentity     : IsIdentity
+      isNatural      : IsNatural
+      isDistributive : IsDistributive
+
+  record Monad : Set ℓ where
+    field
+      raw : RawMonad
+      isMonad : IsMonad raw
+    open IsMonad isMonad public

From 3e123312948402504f8d3a6c7b0dc7ace1c518de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 14:01:57 +0100
Subject: [PATCH 11/31] Monoidal monads addendum

---
 src/Cat/Category/Monad.agda | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 0400ba1..46d0073 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -71,6 +71,12 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       isAssociative : IsAssociative
       isInverse : IsInverse
 
+  record Monad : Set ℓ where
+    field
+      raw : RawMonad
+      isMonad : IsMonad raw
+    open IsMonad isMonad public
+
 -- "A monad in the Kleisli form" [vlad]
 module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   private

From e4e327d1d28d299534e1d22d1095b250a446e09a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 15:13:25 +0100
Subject: [PATCH 12/31] [WIP] equivalence of kleisli- resp. monoidal-
 representation of monad

---
 src/Cat/Category/Monad.agda | 86 ++++++++++++++++++++++++++++++++-----
 1 file changed, 75 insertions(+), 11 deletions(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 46d0073..31b4c47 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
 module Cat.Category.Monad where
 
 open import Agda.Primitive
@@ -12,7 +12,7 @@ open import Cat.Category.Functor as F
 open import Cat.Category.NaturalTransformation
 open import Cat.Categories.Fun
 
--- "A monad in the monoidal form" [vlad]
+-- "A monad in the monoidal form" [voe]
 module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   private
     ℓ = ℓa ⊔ ℓb
@@ -27,15 +27,16 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       -- (>=>)
       μ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
         -- module IdRX = Functor (F.identity {C = RX})
-
-        η : Transformation F.identity R
-        η = proj₁ ηNat
         ηX  : ℂ [ X                    , R.func* X ]
         ηX = η X
         RηX : ℂ [ R.func* X            , R.func* (R.func* X) ] -- ℂ [ R.func* X , {!R.func* (R.func* X))!} ]
@@ -44,8 +45,6 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         IdRX : Arrow (R.func* X) (R.func* X)
         IdRX = 𝟙 {R.func* X}
 
-        μ : Transformation F[ R ∘ R ] R
-        μ = proj₁ μNat
         μX  : ℂ [ RR.func* X           , R.func* X ]
         μX = μ X
         RμX : ℂ [ R.func* (RR.func* X) , RR.func* X ]
@@ -77,7 +76,7 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       isMonad : IsMonad raw
     open IsMonad isMonad public
 
--- "A monad in the Kleisli form" [vlad]
+-- "A monad in the Kleisli form" [voe]
 module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   private
     ℓ = ℓa ⊔ ℓb
@@ -86,13 +85,14 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   record RawMonad : Set ℓ where
     field
       RR : Object → Object
-      η : {X : Object} → ℂ [ X , RR X ]
+      -- Note name-change from [voe]
+      ζ : {X : Object} → ℂ [ X , RR X ]
       rr : {X Y : Object} → ℂ [ X , RR Y ] → ℂ [ RR X , RR Y ]
     -- Name suggestions are welcome!
     IsIdentity     = {X : Object}
-      → rr η ≡ 𝟙 {RR X}
+      → rr ζ ≡ 𝟙 {RR X}
     IsNatural      = {X Y : Object}   (f : ℂ [ X , RR Y ])
-      → (ℂ [ rr f ∘ η ]) ≡ f
+      → (ℂ [ rr f ∘ ζ ]) ≡ f
     IsDistributive = {X Y Z : Object} (g : ℂ [ Y , RR Z ]) (f : ℂ [ X , RR Y ])
       → ℂ [ rr g ∘ rr f ] ≡ rr (ℂ [ rr g ∘ f ])
 
@@ -108,3 +108,67 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       raw : RawMonad
       isMonad : IsMonad raw
     open IsMonad isMonad public
+
+-- 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 ℂ
+
+    module _ (m : M.RawMonad) where
+      private
+        open M.RawMonad m
+        module Kraw = K.RawMonad
+
+      RR : Object → Object
+      RR = func* R
+
+      R→ : {A B : Object} → ℂ [ A , B ] → ℂ [ RR A , RR B ]
+      R→ = func→ R
+
+      ζ : {X : Object} → ℂ [ X , RR X ]
+      ζ = {!!}
+
+      rr : {X Y : Object} → ℂ [ X , RR Y ] → ℂ [ RR X , RR Y ]
+      -- Order is different now!
+      rr {X} {Y} f = ℂ [ f ∘ {!!} ]
+        where
+          μY : ℂ [ func* F[ R ∘ R ] Y , func* R Y ]
+          μY = μ Y
+          ζY : ℂ [ Y , RR Y ]
+          ζY = ζ {Y}
+
+      forthRaw : K.RawMonad
+      Kraw.RR forthRaw = RR
+      Kraw.ζ  forthRaw = ζ
+      Kraw.rr forthRaw = rr
+
+    module _ {raw : M.RawMonad} (m : M.IsMonad raw) where
+      open M.IsMonad m
+      module Kraw = K.RawMonad (forthRaw raw)
+      module Kis = K.IsMonad
+      isIdentity : Kraw.IsIdentity
+      isIdentity = {!!}
+
+      isNatural : Kraw.IsNatural
+      isNatural = {!!}
+
+      isDistributive : Kraw.IsDistributive
+      isDistributive = {!!}
+
+      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)
+
+    eqv : isEquiv M.Monad K.Monad forth
+    eqv = {!!}
+
+  Monoidal≃Kleisli : M.Monad ≃ K.Monad
+  Monoidal≃Kleisli = forth , eqv

From 5d9c820fa2a8c31d13f07bc55707129d4e47515f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 15:25:07 +0100
Subject: [PATCH 13/31] Add note about haskell

---
 src/Cat/Category/Monad.agda | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 31b4c47..d4084ef 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -88,7 +88,18 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       -- Note name-change from [voe]
       ζ : {X : Object} → ℂ [ X , RR X ]
       rr : {X Y : Object} → ℂ [ X , RR Y ] → ℂ [ RR X , RR Y ]
-    -- Name suggestions are welcome!
+    -- 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
+    --
     IsIdentity     = {X : Object}
       → rr ζ ≡ 𝟙 {RR X}
     IsNatural      = {X Y : Object}   (f : ℂ [ X , RR Y ])

From be505cdfbec2cab77ecac33e9e5c0ae13ef4b6ba Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 19:07:58 +0100
Subject: [PATCH 14/31] Prove `IsAssociative`

---
 src/Cat/Category/Monad.agda | 90 ++++++++++++++++++++-----------------
 1 file changed, 49 insertions(+), 41 deletions(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index d4084ef..9263c9b 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -36,28 +36,12 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       module R  = Functor R
       module RR = Functor F[ R ∘ R ]
       module _ {X : Object} where
-        -- module IdRX = Functor (F.identity {C = RX})
-        ηX  : ℂ [ X                    , R.func* X ]
-        ηX = η X
-        RηX : ℂ [ R.func* X            , R.func* (R.func* X) ] -- ℂ [ R.func* X , {!R.func* (R.func* X))!} ]
-        RηX = R.func→ ηX
-        ηRX = η (R.func* X)
-        IdRX : Arrow (R.func* X) (R.func* X)
-        IdRX = 𝟙 {R.func* X}
-
-        μX  : ℂ [ RR.func* X           , R.func* X ]
-        μX = μ X
-        RμX : ℂ [ R.func* (RR.func* X) , RR.func* X ]
-        RμX = R.func→ μX
-        μRX : ℂ [ RR.func* (R.func* X) , R.func* (R.func* X) ]
-        μRX = μ (R.func* X)
-
         IsAssociative' : Set _
-        IsAssociative' = ℂ [ μX ∘ RμX ] ≡ ℂ [ μX ∘ μRX ]
+        IsAssociative' = μ X ∘ R.func→ (μ X) ≡ μ X ∘ μ (R.func* X)
         IsInverse' : Set _
         IsInverse'
-          = ℂ [ μX ∘ ηRX ] ≡ IdRX
-          × ℂ [ μX ∘ RηX ] ≡ IdRX
+          = μ 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.
@@ -123,33 +107,28 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 -- Problem 2.3
 module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
   private
-    open Category ℂ using (Object ; Arrow ; 𝟙)
+    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
+        RR : Object → Object
+        RR = func* R
 
-      R→ : {A B : Object} → ℂ [ A , B ] → ℂ [ RR A , RR B ]
-      R→ = func→ R
+        R→ : {A B : Object} → ℂ [ A , B ] → ℂ [ RR A , RR B ]
+        R→ = func→ R
 
-      ζ : {X : Object} → ℂ [ X , RR X ]
-      ζ = {!!}
+        ζ : {X : Object} → ℂ [ X , RR X ]
+        ζ {X} = η X
 
-      rr : {X Y : Object} → ℂ [ X , RR Y ] → ℂ [ RR X , RR Y ]
-      -- Order is different now!
-      rr {X} {Y} f = ℂ [ f ∘ {!!} ]
-        where
-          μY : ℂ [ func* F[ R ∘ R ] Y , func* R Y ]
-          μY = μ Y
-          ζY : ℂ [ Y , RR Y ]
-          ζY = ζ {Y}
+        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
@@ -158,15 +137,34 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
 
     module _ {raw : M.RawMonad} (m : M.IsMonad raw) where
       open M.IsMonad m
-      module Kraw = K.RawMonad (forthRaw raw)
+      open K.RawMonad (forthRaw raw)
       module Kis = K.IsMonad
-      isIdentity : Kraw.IsIdentity
-      isIdentity = {!!}
 
-      isNatural : Kraw.IsNatural
-      isNatural = {!!}
+      isIdentity : IsIdentity
+      isIdentity {X} = begin
+        rr ζ                      ≡⟨⟩
+        rr (η X)                  ≡⟨⟩
+        ℂ [ μ X ∘ func→ R (η X) ] ≡⟨ proj₂ isInverse ⟩
+        𝟙 ∎
 
-      isDistributive : Kraw.IsDistributive
+      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
+          module ℂ = Category ℂ
+          open NaturalTransformation
+          ηN : Natural ℂ ℂ F.identity R η
+          ηN = proj₂ ηNat
+
+      isDistributive : IsDistributive
       isDistributive = {!!}
 
       forthIsMonad : K.IsMonad (forthRaw raw)
@@ -178,8 +176,18 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
     Kleisli.Monad.raw     (forth m) = forthRaw (M.Monad.raw m)
     Kleisli.Monad.isMonad (forth m) = forthIsMonad (M.Monad.isMonad m)
 
+    back : K.Monad → M.Monad
+    back = {!!}
+
+    fortheq : (m : K.Monad) → forth (back m) ≡ m
+    fortheq = {!!}
+
+    backeq : (m : M.Monad) → back (forth m) ≡ m
+    backeq = {!!}
+
+    open import Cubical.GradLemma
     eqv : isEquiv M.Monad K.Monad forth
-    eqv = {!!}
+    eqv = gradLemma forth back fortheq backeq
 
   Monoidal≃Kleisli : M.Monad ≃ K.Monad
   Monoidal≃Kleisli = forth , eqv

From e7abab0e4c6bf57a40df5742274a7f8cf9b1d61c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 19:08:20 +0100
Subject: [PATCH 15/31] Add `pure` and `>=>` to kleisli category

---
 src/Cat/Category/Monad.agda | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 9263c9b..2a4f0a3 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -84,6 +84,15 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     --     pure : x → m x
     --     flip (>>=) :: (a → m b) → m a → m b
     --
+    pure : {X : Object} → ℂ [ X , RR X ]
+    pure = ζ
+    -- 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 ]
+
     IsIdentity     = {X : Object}
       → rr ζ ≡ 𝟙 {RR X}
     IsNatural      = {X Y : Object}   (f : ℂ [ X , RR Y ])

From 9d09363f783a50d990149d17a5991a7f8185eb0f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 20:37:21 +0100
Subject: [PATCH 16/31] Expand definition of `isDistributive` somewhat

Also contains some side-tracks
---
 src/Cat/Category.agda       |  2 ++
 src/Cat/Category/Monad.agda | 69 +++++++++++++++++++++++++++++++------
 2 files changed, 61 insertions(+), 10 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index cec311d..31b7cdd 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -41,6 +41,8 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   codomain : { a b : Object } → Arrow a b → Object
   codomain {b = b} _ = b
 
+  -- 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
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 2a4f0a3..6bc9e92 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -21,10 +21,11 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   open NaturalTransformation ℂ ℂ
   record RawMonad : Set ℓ where
     field
+      -- R ~ m
       R : Functor ℂ ℂ
-      -- pure
+      -- η ~ pure
       ηNat : NaturalTransformation F.identity R
-      -- (>=>)
+      -- μ ~ join
       μNat : NaturalTransformation F[ R ∘ R ] R
 
     η : Transformation F.identity R
@@ -59,6 +60,33 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       raw : RawMonad
       isMonad : IsMonad raw
     open IsMonad isMonad public
+    module R = Functor R
+    module RR = Functor F[ R ∘ R ]
+    module _ {X Y Z : _} {g : ℂ [ Y , R.func* Z ]} {f : ℂ [ X , R.func* Y ]} where
+      lem : μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ≡ μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f)
+      lem = begin
+        μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ≡⟨ {!!} ⟩
+        μ Z ∘ R.func→     (μ Z ∘ R.func→ g ∘ f) ∎
+        where
+          open Category ℂ using () renaming (isAssociative to c-assoc)
+          μN : Natural F[ R ∘ R ] R μ
+          -- μN : (f : ℂ [ Y , R.func* Z ]) → μ (R.func* Z) ∘ RR.func→ f ≡ R.func→ f ∘ μ Y
+          μN = proj₂ μNat
+          μg : μ (R.func* Z) ∘ RR.func→ g ≡ R.func→ g ∘ μ Y
+          μg = μN g
+          μf : μ (R.func* Y) ∘ RR.func→ f ≡ R.func→ f ∘ μ X
+          μf = μN f
+          ηN : Natural F.identity R η
+          ηN = proj₂ ηNat
+          ηg : η (R.func* Z) ∘ g ≡ R.func→ g ∘ η Y
+          ηg = ηN g
+          -- Alternate route:
+          res = begin
+            μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ≡⟨ c-assoc ⟩
+            μ Z ∘ R.func→ g ∘ μ Y ∘ R.func→ f   ≡⟨ {!!} ⟩
+            μ Z ∘ (R.func→ g ∘ μ Y) ∘ R.func→ f ≡⟨ {!!} ⟩
+            μ Z ∘ (μ (R.func* Z) ∘ RR.func→ g) ∘ R.func→ f ≡⟨ {!!} ⟩
+            μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f) ∎
 
 -- "A monad in the Kleisli form" [voe]
 module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
@@ -93,12 +121,32 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     _>=>_ : {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
+      → rr f ∘ ζ ≡ f
     IsDistributive = {X Y Z : Object} (g : ℂ [ Y , RR Z ]) (f : ℂ [ X , RR Y ])
-      → ℂ [ rr g ∘ rr f ] ≡ rr (ℂ [ rr g ∘ f ])
+      → rr g ∘ rr f ≡ rr (rr g ∘ f)
+    -- I assume `Fusion` is admissable - it certainly looks more like the
+    -- distributive law for monads I know from Haskell.
+    Fusion = {X Y Z : Object} (g : ℂ [ Y , Z ]) (f : ℂ [ X , Y ])
+      → rr (ζ ∘ g ∘ f) ≡ rr (ζ ∘ g) ∘ rr (ζ ∘ f)
+    -- NatDist2Fus : IsNatural → IsDistributive → Fusion
+    -- NatDist2Fus isNatural isDistributive g f =
+    --   let
+    --     ζf = ζ ∘ f
+    --     ζg = ζ ∘ g
+    --     Nζf : rr (ζ ∘ f) ∘ ζ ≡ ζ ∘ f
+    --     Nζf = isNatural ζf
+    --     Nζg : rr (ζ ∘ g) ∘ ζ ≡ ζ ∘ g
+    --     Nζg = isNatural ζg
+    --     ζgf = ζ ∘ g ∘ f
+    --     Nζgf : rr (ζ ∘ g ∘ f) ∘ ζ ≡ ζ ∘ g ∘ f
+    --     Nζgf = isNatural ζgf
+    --     res  : rr (ζ ∘ g ∘ f) ≡ rr (ζ ∘ g) ∘ rr (ζ ∘ f)
+    --     res = {!!}
+    --   in res
 
   record IsMonad (raw : RawMonad) : Set ℓ where
     open RawMonad raw public
@@ -130,9 +178,6 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
         RR : Object → Object
         RR = func* R
 
-        R→ : {A B : Object} → ℂ [ A , B ] → ℂ [ RR A , RR B ]
-        R→ = func→ R
-
         ζ : {X : Object} → ℂ [ X , RR X ]
         ζ {X} = η X
 
@@ -168,13 +213,17 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
         𝟙 ∘ f                     ≡⟨ proj₂ ℂ.isIdentity ⟩
         f ∎
         where
-          module ℂ = Category ℂ
           open NaturalTransformation
+          module ℂ = Category ℂ
           ηN : Natural ℂ ℂ F.identity R η
           ηN = proj₂ ηNat
 
       isDistributive : IsDistributive
-      isDistributive = {!!}
+      isDistributive {X} {Y} {Z} g f = begin
+        rr g ∘ rr f                         ≡⟨⟩
+        μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ≡⟨ {!!} ⟩
+        μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f) ≡⟨⟩
+        μ Z ∘ R.func→ (rr g ∘ f) ∎
 
       forthIsMonad : K.IsMonad (forthRaw raw)
       Kis.isIdentity forthIsMonad = isIdentity
@@ -189,7 +238,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
     back = {!!}
 
     fortheq : (m : K.Monad) → forth (back m) ≡ m
-    fortheq = {!!}
+    fortheq m = {!!}
 
     backeq : (m : M.Monad) → back (forth m) ≡ m
     backeq = {!!}

From a447cd9c7c33475d6dd2e3da95c52cc099c397fc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 20:41:47 +0100
Subject: [PATCH 17/31] Syntax

---
 src/Cat/Category/Monad.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 6bc9e92..7336c80 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -119,7 +119,7 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     -- (>>=) : 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 ]
+    f >=> g = rr g ∘ f
 
     -- fmap id ≡ id
     IsIdentity     = {X : Object}
@@ -182,7 +182,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
         ζ {X} = η X
 
         rr : {X Y : Object} → ℂ [ X , RR Y ] → ℂ [ RR X , RR Y ]
-        rr {X} {Y} f = ℂ [ μ Y ∘ func→ R f ]
+        rr {X} {Y} f = μ Y ∘ func→ R f
 
       forthRaw : K.RawMonad
       Kraw.RR forthRaw = RR
@@ -198,7 +198,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       isIdentity {X} = begin
         rr ζ                      ≡⟨⟩
         rr (η X)                  ≡⟨⟩
-        ℂ [ μ X ∘ func→ R (η X) ] ≡⟨ proj₂ isInverse ⟩
+        μ X ∘ func→ R (η X)       ≡⟨ proj₂ isInverse ⟩
         𝟙 ∎
 
       module R = Functor R

From a6b01929f0b243fe780cdda79a663addf20c2bd1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 01:27:20 +0100
Subject: [PATCH 18/31] Prove distributive law

---
 src/Cat/Category/Monad.agda | 60 +++++++++++++++++++------------------
 1 file changed, 31 insertions(+), 29 deletions(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 7336c80..1b0e3da 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -17,7 +17,7 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   private
     ℓ = ℓa ⊔ ℓb
 
-  open Category ℂ hiding (IsAssociative)
+  open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
   open NaturalTransformation ℂ ℂ
   record RawMonad : Set ℓ where
     field
@@ -60,33 +60,6 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       raw : RawMonad
       isMonad : IsMonad raw
     open IsMonad isMonad public
-    module R = Functor R
-    module RR = Functor F[ R ∘ R ]
-    module _ {X Y Z : _} {g : ℂ [ Y , R.func* Z ]} {f : ℂ [ X , R.func* Y ]} where
-      lem : μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ≡ μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f)
-      lem = begin
-        μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ≡⟨ {!!} ⟩
-        μ Z ∘ R.func→     (μ Z ∘ R.func→ g ∘ f) ∎
-        where
-          open Category ℂ using () renaming (isAssociative to c-assoc)
-          μN : Natural F[ R ∘ R ] R μ
-          -- μN : (f : ℂ [ Y , R.func* Z ]) → μ (R.func* Z) ∘ RR.func→ f ≡ R.func→ f ∘ μ Y
-          μN = proj₂ μNat
-          μg : μ (R.func* Z) ∘ RR.func→ g ≡ R.func→ g ∘ μ Y
-          μg = μN g
-          μf : μ (R.func* Y) ∘ RR.func→ f ≡ R.func→ f ∘ μ X
-          μf = μN f
-          ηN : Natural F.identity R η
-          ηN = proj₂ ηNat
-          ηg : η (R.func* Z) ∘ g ≡ R.func→ g ∘ η Y
-          ηg = ηN g
-          -- Alternate route:
-          res = begin
-            μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ≡⟨ c-assoc ⟩
-            μ Z ∘ R.func→ g ∘ μ Y ∘ R.func→ f   ≡⟨ {!!} ⟩
-            μ Z ∘ (R.func→ g ∘ μ Y) ∘ R.func→ f ≡⟨ {!!} ⟩
-            μ Z ∘ (μ (R.func* Z) ∘ RR.func→ g) ∘ R.func→ f ≡⟨ {!!} ⟩
-            μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f) ∎
 
 -- "A monad in the Kleisli form" [voe]
 module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
@@ -221,9 +194,38 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       isDistributive : IsDistributive
       isDistributive {X} {Y} {Z} g f = begin
         rr g ∘ rr f                         ≡⟨⟩
-        μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ 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

From 4c298855e07ae7fa6ddf43eb64bac122f789ceb1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 03:09:25 +0100
Subject: [PATCH 19/31] [WIP] Proving other fusion law

Also set up framework for equality principle for monads
---
 src/Cat/Category/Monad.agda | 244 +++++++++++++++++++++++-------------
 1 file changed, 160 insertions(+), 84 deletions(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 1b0e3da..d16a030 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -61,12 +61,21 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       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 ℂ hiding (IsIdentity)
+  open Category ℂ using (Arrow ; 𝟙 ; Object ; _∘_)
   record RawMonad : Set ℓ where
     field
       RR : Object → Object
@@ -87,6 +96,8 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     --
     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
@@ -101,25 +112,8 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       → rr f ∘ ζ ≡ f
     IsDistributive = {X Y Z : Object} (g : ℂ [ Y , RR Z ]) (f : ℂ [ X , RR Y ])
       → rr g ∘ rr f ≡ rr (rr g ∘ f)
-    -- I assume `Fusion` is admissable - it certainly looks more like the
-    -- distributive law for monads I know from Haskell.
-    Fusion = {X Y Z : Object} (g : ℂ [ Y , Z ]) (f : ℂ [ X , Y ])
-      → rr (ζ ∘ g ∘ f) ≡ rr (ζ ∘ g) ∘ rr (ζ ∘ f)
-    -- NatDist2Fus : IsNatural → IsDistributive → Fusion
-    -- NatDist2Fus isNatural isDistributive g f =
-    --   let
-    --     ζf = ζ ∘ f
-    --     ζg = ζ ∘ g
-    --     Nζf : rr (ζ ∘ f) ∘ ζ ≡ ζ ∘ f
-    --     Nζf = isNatural ζf
-    --     Nζg : rr (ζ ∘ g) ∘ ζ ≡ ζ ∘ g
-    --     Nζg = isNatural ζg
-    --     ζgf = ζ ∘ g ∘ f
-    --     Nζgf : rr (ζ ∘ g ∘ f) ∘ ζ ≡ ζ ∘ g ∘ f
-    --     Nζgf = isNatural ζgf
-    --     res  : rr (ζ ∘ g ∘ f) ≡ rr (ζ ∘ g) ∘ rr (ζ ∘ f)
-    --     res = {!!}
-    --   in res
+    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
@@ -127,6 +121,16 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       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
@@ -134,6 +138,15 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       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
@@ -163,69 +176,70 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       Kraw.rr forthRaw = rr
 
     module _ {raw : M.RawMonad} (m : M.IsMonad raw) where
-      open M.IsMonad m
-      open K.RawMonad (forthRaw raw)
-      module Kis = K.IsMonad
+      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 ⟩
-        𝟙 ∎
+        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
+        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
+        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
@@ -233,17 +247,79 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       Kis.isDistributive forthIsMonad = 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 = {!!}
+
+      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
-    back = {!!}
+    Monoidal.Monad.raw     (back m) = backRaw     m
+    Monoidal.Monad.isMonad (back m) = backIsMonad m
+
+
+    forthRawEq : (m : K.Monad) → forthRaw (backRaw m) ≡ K.Monad.raw m
+    K.RawMonad.RR (forthRawEq m _) = K.RawMonad.RR (K.Monad.raw m)
+    K.RawMonad.ζ  (forthRawEq m _) = K.RawMonad.ζ  (K.Monad.raw m)
+    -- stuck
+    K.RawMonad.rr (forthRawEq m i) = {!!}
 
     fortheq : (m : K.Monad) → forth (back m) ≡ m
-    fortheq m = {!!}
+    fortheq m = K.Monad≡ (forthRawEq m)
+
+    backRawEq : (m : M.Monad) → backRaw (forth m) ≡ M.Monad.raw m
+    -- stuck
+    M.RawMonad.R    (backRawEq m _) = ?
+    M.RawMonad.ηNat (backRawEq m x) = {!!}
+    M.RawMonad.μNat (backRawEq m x) = {!!}
 
     backeq : (m : M.Monad) → back (forth m) ≡ m
-    backeq = {!!}
+    backeq m = M.Monad≡ (backRawEq m)
 
     open import Cubical.GradLemma
     eqv : isEquiv M.Monad K.Monad forth

From 12dddc20679d0bf1558a9fdd4f67d778401da461 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 03:12:23 +0100
Subject: [PATCH 20/31] Use a module

---
 src/Cat/Category/Monad.agda | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index d16a030..92805e0 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -302,21 +302,25 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
     Monoidal.Monad.raw     (back m) = backRaw     m
     Monoidal.Monad.isMonad (back m) = backIsMonad m
 
-
-    forthRawEq : (m : K.Monad) → forthRaw (backRaw m) ≡ K.Monad.raw m
-    K.RawMonad.RR (forthRawEq m _) = K.RawMonad.RR (K.Monad.raw m)
-    K.RawMonad.ζ  (forthRawEq m _) = K.RawMonad.ζ  (K.Monad.raw m)
-    -- stuck
-    K.RawMonad.rr (forthRawEq m i) = {!!}
+    -- 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)
 
-    backRawEq : (m : M.Monad) → backRaw (forth m) ≡ M.Monad.raw m
-    -- stuck
-    M.RawMonad.R    (backRawEq m _) = ?
-    M.RawMonad.ηNat (backRawEq m x) = {!!}
-    M.RawMonad.μNat (backRawEq m x) = {!!}
+    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)

From ce46e0ae7ad10f7196aa61c32f40ec2c6dbd19f7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 14:27:37 +0100
Subject: [PATCH 21/31] Module-ify

---
 src/Cat/Category/Properties.agda | 51 ++++++++++++++++----------------
 1 file changed, 26 insertions(+), 25 deletions(-)

diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index 4eeb6c3..e929d81 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -8,38 +8,39 @@ 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
+-- Maybe inline into RawCategory"
+module _ {ℓa ℓb : Level} (ℂ : Category ℓ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₁              ∎
+  module _ {A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.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 (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-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
+    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).

From 5deabb7546b3d26c710556ef712698f374449705 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 14:28:01 +0100
Subject: [PATCH 22/31] Forgot to add monoid-module

---
 src/Cat/Category/Monoid.agda | 45 ++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100644 src/Cat/Category/Monoid.agda

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

From caddf83a097d7fb9eba022bf4a0751c7001179d0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 14:37:28 +0100
Subject: [PATCH 23/31] Let `IsCategory` reexport RawCategory

---
 src/Cat/Categories/Free.agda | 2 --
 src/Cat/Category.agda        | 5 ++---
 2 files changed, 2 insertions(+), 5 deletions(-)

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/Category.agda b/src/Cat/Category.agda
index 31b7cdd..dba717a 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -100,7 +100,7 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
     Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
 
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
-  open RawCategory ℂ
+  open RawCategory ℂ public
   open Univalence ℂ public
   field
     isAssociative : IsAssociative
@@ -112,7 +112,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
 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
 
@@ -196,7 +196,6 @@ record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     raw : RawCategory ℓa ℓb
     {{isCategory}} : IsCategory raw
 
-  open RawCategory raw public
   open IsCategory isCategory public
 
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where

From d63ecc3a6577463bddcd7f1d5dd53bdd760605ac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 14:39:11 +0100
Subject: [PATCH 24/31] Use abbreviation

---
 src/Cat/Category/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index e929d81..1b75397 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -15,7 +15,7 @@ open Equality.Data.Product
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   open Category ℂ
 
-  module _ {A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where
+  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 (proj₁ isIdentity) ⟩

From 2e7220567aebefe13623ee64d45ae5ab37c9c495 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 14:44:03 +0100
Subject: [PATCH 25/31] Move lemma into `IsCategory`

---
 src/Cat/Category.agda            | 26 ++++++++++++++++++++++++++
 src/Cat/Category/Properties.agda | 31 -------------------------------
 2 files changed, 26 insertions(+), 31 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index dba717a..df13850 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -107,6 +107,32 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     isIdentity    : IsIdentity 𝟙
     arrowsAreSets : ArrowsAreSets
     univalent     : Univalent isIdentity
+  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
 
 -- `IsCategory` is a mere proposition.
 module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index 1b75397..957b31f 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -11,37 +11,6 @@ open import Cat.Category.Functor
 open import Cat.Equality
 open Equality.Data.Product
 
--- Maybe inline into RawCategory"
-module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-  open Category ℂ
-
-  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 (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)

From cd98736d028b27d168f7b0bad05d1ebc0f5ad9b1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 15:21:38 +0100
Subject: [PATCH 26/31] Add documentation in Category-module

---
 src/Cat/Category.agda | 146 +++++++++++++++++++++++++++++-------------
 1 file changed, 103 insertions(+), 43 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index df13850..7ba7eb9 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,16 @@ 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)
@@ -93,12 +140,16 @@ 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 ℂ public
   open Univalence ℂ public
@@ -107,6 +158,8 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     isIdentity    : IsIdentity 𝟙
     arrowsAreSets : ArrowsAreSets
     univalent     : Univalent isIdentity
+
+  -- 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
@@ -134,7 +187,10 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     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
 
--- `IsCategory` is a mere proposition.
+-- | 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
@@ -217,6 +273,9 @@ 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
@@ -224,6 +283,7 @@ record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
 
   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
@@ -232,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 renaming (opposite to Opposite)

From f0beec1530b428713ff177068566a7d845ea112a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 15:23:33 +0100
Subject: [PATCH 27/31] Rename Opposite to opposite

---
 src/Cat/Categories/Fun.agda      | 2 +-
 src/Cat/Categories/Sets.agda     | 4 ++--
 src/Cat/Category.agda            | 2 +-
 src/Cat/Category/Properties.agda | 2 +-
 src/Cat/CwF.agda                 | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index ac7fd8a..2af9e55 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -108,7 +108,7 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   open import Cat.Categories.Sets
-  open NaturalTransformation (Opposite ℂ) (𝓢𝓮𝓽 ℓ')
+  open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
 
   -- Restrict the functors to Presheafs.
   RawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
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 7ba7eb9..d70fc65 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -336,4 +336,4 @@ module Opposite {ℓa ℓb : Level} where
     Category.raw        (oppositeIsInvolution i) = rawInv i
     Category.isCategory (oppositeIsInvolution x) = {!!}
 
-open Opposite public renaming (opposite to Opposite)
+open Opposite public
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index 957b31f..5462f13 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -22,7 +22,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat
   open import Cat.Category.Exponential
   open Functor
   𝓢 = Sets ℓ
-  open Fun (Opposite ℂ) 𝓢
+  open Fun (opposite ℂ) 𝓢
   private
     Catℓ : Category _ _
     Catℓ = record { raw = RawCat ℓ ℓ ; isCategory = unprovable}
diff --git a/src/Cat/CwF.agda b/src/Cat/CwF.agda
index 3954ea5..584268d 100644
--- a/src/Cat/CwF.agda
+++ b/src/Cat/CwF.agda
@@ -22,7 +22,7 @@ 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

From 44526b85eb1f0b6970c9891c4716e338b5cb1556 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 15:24:44 +0100
Subject: [PATCH 28/31] Move CwF

---
 src/Cat.agda                      | 2 +-
 src/Cat/{ => Categories}/CwF.agda | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)
 rename src/Cat/{ => Categories}/CwF.agda (98%)

diff --git a/src/Cat.agda b/src/Cat.agda
index 0619b51..4a0b4a0 100644
--- a/src/Cat.agda
+++ b/src/Cat.agda
@@ -1,7 +1,6 @@
 module Cat where
 
 import Cat.Category
-import Cat.CwF
 
 import Cat.Category.Functor
 import Cat.Category.Product
@@ -19,3 +18,4 @@ 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/CwF.agda b/src/Cat/Categories/CwF.agda
similarity index 98%
rename from src/Cat/CwF.agda
rename to src/Cat/Categories/CwF.agda
index 584268d..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

From 5caecf9796a1e815a37b32d3e6ecbf0a619b438e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 15:28:42 +0100
Subject: [PATCH 29/31] Rename properties to yoneda

---
 src/Cat.agda                                      | 2 +-
 src/Cat/Category/{Properties.agda => Yoneda.agda} | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)
 rename src/Cat/Category/{Properties.agda => Yoneda.agda} (98%)

diff --git a/src/Cat.agda b/src/Cat.agda
index 4a0b4a0..7d8b396 100644
--- a/src/Cat.agda
+++ b/src/Cat.agda
@@ -9,7 +9,7 @@ import Cat.Category.CartesianClosed
 import Cat.Category.NaturalTransformation
 import Cat.Category.Pathy
 import Cat.Category.Bij
-import Cat.Category.Properties
+import Cat.Category.Yoneda
 import Cat.Category.Monad
 
 import Cat.Categories.Sets
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Yoneda.agda
similarity index 98%
rename from src/Cat/Category/Properties.agda
rename to src/Cat/Category/Yoneda.agda
index 5462f13..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

From 2c6132768e723e43ba5bcf41a67e2d7d28fd9260 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 15:29:52 +0100
Subject: [PATCH 30/31] Remove `Pathy` and `Bij`

---
 src/Cat.agda                |  2 --
 src/Cat/Category/Bij.agda   | 46 --------------------------------
 src/Cat/Category/Pathy.agda | 53 -------------------------------------
 3 files changed, 101 deletions(-)
 delete mode 100644 src/Cat/Category/Bij.agda
 delete mode 100644 src/Cat/Category/Pathy.agda

diff --git a/src/Cat.agda b/src/Cat.agda
index 7d8b396..20c5d69 100644
--- a/src/Cat.agda
+++ b/src/Cat.agda
@@ -7,8 +7,6 @@ import Cat.Category.Product
 import Cat.Category.Exponential
 import Cat.Category.CartesianClosed
 import Cat.Category.NaturalTransformation
-import Cat.Category.Pathy
-import Cat.Category.Bij
 import Cat.Category.Yoneda
 import Cat.Category.Monad
 
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/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 = {!!}

From 7518a642f67f227692ffcf39c5cb1f56feba6c49 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 15:38:12 +0100
Subject: [PATCH 31/31] Update changelog

---
 CHANGELOG.md | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

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.