From a64e2484e39b8ed55cade72106ed77db846ac30e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 16 Feb 2018 12:24:58 +0100
Subject: [PATCH 01/23] Prove associativity for natural transformations

---
 src/Cat/Categories/Fun.agda | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 522bb34..610c3ea 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -9,6 +9,7 @@ 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
 
@@ -125,10 +126,18 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
         θ = proj₁ θ'
         η = proj₁ η'
         ζ = proj₁ ζ'
+        θNat = proj₂ θ'
+        ηNat = proj₂ η'
+        ζNat = proj₂ ζ'
+        L : NaturalTransformation A D
+        L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ'))
+        R : NaturalTransformation A D
+        R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
       _g⊕f_ = _:⊕:_ {A} {B} {C}
       _h⊕g_ = _:⊕:_ {B} {C} {D}
-      :assoc: : (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ')) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
-      :assoc: = Σ≡ (funExt (λ _ → assoc)) {!!}
+      :assoc: : L ≡ R
+      :assoc: = lemSig (naturalIsProp {F = A} {D})
+        L R (funExt (λ x → assoc))
         where
           open IsCategory (isCategory 𝔻)
 

From 73ab4d1836a9dd5cecf5fe4a4be62c3fced7d1e1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 16 Feb 2018 12:46:25 +0100
Subject: [PATCH 02/23] Proove identity laws for natural transformations

---
 src/Cat/Categories/Fun.agda | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 610c3ea..ada60d2 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -142,10 +142,21 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
           open IsCategory (isCategory 𝔻)
 
     module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
+      private
+        allNatural = naturalIsProp {F = A} {B}
+        f' = proj₁ f
+        module 𝔻Data = Category 𝔻
+        eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C
+        eq-r C = begin
+          𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩
+          𝔻 [ f' C ∘ 𝔻Data.𝟙 ]  ≡⟨ proj₁ (𝔻.ident {A} {B}) ⟩
+          f' C ∎
+        eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
+        eq-l C = proj₂ (𝔻.ident {A} {B})
       ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
-      ident-r = {!!}
+      ident-r = lemSig allNatural _ _ (funExt eq-r)
       ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
-      ident-l = {!!}
+      ident-l = lemSig allNatural _ _ (funExt eq-l)
       :ident:
         : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
         × (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f

From 89ad60ffefdd93b1483d36e2e59113932b94723a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 19 Feb 2018 11:09:49 +0100
Subject: [PATCH 03/23] Stuff about the free category

---
 src/Cat/Categories/Free.agda | 80 ++++++++++++++++++++----------------
 1 file changed, 45 insertions(+), 35 deletions(-)

diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda
index 703a7d2..326152a 100644
--- a/src/Cat/Categories/Free.agda
+++ b/src/Cat/Categories/Free.agda
@@ -8,55 +8,65 @@ open import Data.Product
 open import Cat.Category
 
 open IsCategory
-open Category
 
 -- data Path {ℓ : Level} {A : Set ℓ} : (a b : A) → Set ℓ where
 --   emptyPath : {a : A} → Path a a
 --   concatenate : {a b c : A} → Path a b → Path b c → Path a b
 
+-- import Data.List
+-- P : (a b : Object ℂ) → Set (ℓ ⊔ ℓ')
+-- P = {!Data.List.List ?!}
+-- Generalized paths:
+data Path {ℓ ℓ' : Level} {A : Set ℓ} (R : A → A → Set ℓ') : (a b : A) → Set (ℓ ⊔ ℓ') where
+  empty : {a : A} → Path R a a
+  cons : {a b c : A} → R b c → Path R a b → Path R a c
+
+concatenate _++_ : ∀ {ℓ ℓ'} {A : Set ℓ} {a b c : A} {R : A → A → Set ℓ'} → Path R b c → Path R a b → Path R a c
+concatenate empty p = p
+concatenate (cons x q) p = cons x (concatenate q p)
+_++_ = concatenate
+
+singleton : ∀ {ℓ} {𝓤 : Set ℓ} {ℓr} {R : 𝓤 → 𝓤 → Set ℓr} {A B : 𝓤} → R A B → Path R A B
+singleton f = cons f empty
+
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   module ℂ = Category ℂ
-
-  -- import Data.List
-  -- P : (a b : Object ℂ) → Set (ℓ ⊔ ℓ')
-  -- P = {!Data.List.List ?!}
-  -- Generalized paths:
-  -- data P {ℓ : Level} {A : Set ℓ} (R : A → A → Set ℓ) : (a b : A) → Set ℓ where
-  --   e : {a : A} → P R a a
-  --   c : {a b c : A} → R a b → P R b c → P R a c
-
-  -- Path's are like lists with directions.
-  -- This implementation is specialized to categories.
-  data Path : (a b : Object ℂ) → Set (ℓ ⊔ ℓ') where
-    empty : {A : Object ℂ} → Path A A
-    cons : ∀ {A B C} → ℂ [ B , C ] → Path A B → Path A C
-
-  concatenate : ∀ {A B C : Object ℂ}  → Path B C → Path A B → Path A C
-  concatenate empty p = p
-  concatenate (cons x q) p = cons x (concatenate q p)
+  open Category ℂ
 
   private
-    module _ {A B C D : Object ℂ} where
-      p-assoc : {r : Path A B} {q : Path B C} {p : Path C D} → concatenate p (concatenate q r) ≡ concatenate (concatenate p q) r
-      p-assoc {r} {q} {p} = {!!}
-    module _ {A B : Object ℂ} {p : Path A B} where
-      -- postulate
-      --   ident-r : concatenate {A} {A} {B} p (lift 𝟙) ≡ p
-      --   ident-l : concatenate {A} {B} {B} (lift 𝟙) p ≡ p
-    module _ {A B : Object ℂ} where
-      isSet : Cubical.isSet (Path A B)
-      isSet = {!!}
+    p-assoc : {A B C D : Object} {r : Path Arrow A B} {q : Path Arrow B C} {p : Path Arrow C D}
+      → p ++ (q ++ r) ≡ (p ++ q) ++ r
+    p-assoc {r = r} {q} {empty} = refl
+    p-assoc {A} {B} {C} {D} {r = r} {q} {cons x p} = begin
+      cons x p ++ (q ++ r)   ≡⟨ cong (cons x) lem ⟩
+      cons x ((p ++ q) ++ r) ≡⟨⟩
+      (cons x p ++ q) ++ r ∎
+      where
+        lem : p ++ (q ++ r) ≡ ((p ++ q) ++ r)
+        lem = p-assoc {r = r} {q} {p}
+
+    ident-r : ∀ {A} {B} {p : Path Arrow A B} → concatenate p empty ≡ p
+    ident-r {p = empty} = refl
+    ident-r {p = cons x p} = cong (cons x) ident-r
+
+    ident-l : ∀ {A} {B} {p : Path Arrow A B} → concatenate empty p ≡ p
+    ident-l = refl
+
+    module _ {A B : Object} where
+      isSet : Cubical.isSet (Path Arrow A B)
+      isSet a b p q = {!!}
+
   RawFree : RawCategory ℓ (ℓ ⊔ ℓ')
   RawFree = record
-    { Object = Object ℂ
-    ; Arrow = Path
-    ; 𝟙 = λ {o} → {!lift 𝟙!}
-    ; _∘_ = λ {a b c} → {!concatenate {a} {b} {c}!}
+    { Object = Object
+    ; Arrow = Path Arrow
+    ; 𝟙 = empty
+    ; _∘_ = concatenate
     }
   RawIsCategoryFree : IsCategory RawFree
   RawIsCategoryFree = record
-    { assoc = {!p-assoc!}
-    ; ident = {!ident-r , ident-l!}
+    { assoc = λ { {f = f} {g} {h} → p-assoc {r = f} {g} {h}}
+    ; ident = ident-r , ident-l
     ; arrowIsSet = {!!}
     ; univalent = {!!}
     }

From bec5acdc59ca50377252399fdaa06bfaf9c287c0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 19 Feb 2018 11:25:16 +0100
Subject: [PATCH 04/23] Move proposition to wishlist

---
 src/Cat/Category.agda | 6 ++----
 src/Cat/Wishlist.agda | 5 +++++
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index cee681f..1b542be 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -14,6 +14,8 @@ import Function
 open import Cubical
 open import Cubical.NType.Properties using ( propIsEquiv )
 
+open import Cat.Wishlist
+
 ∃! : ∀ {a b} {A : Set a}
   → (A → Set b) → Set (a ⊔ b)
 ∃! = ∃!≈ _≡_
@@ -23,10 +25,6 @@ open import Cubical.NType.Properties using ( propIsEquiv )
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
--- This follows from [HoTT-book: §7.1.10]
--- Andrea says the proof is in `cubical` but I can't find it.
-postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (isSet A)
-
 record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
   -- adding no-eta-equality can speed up type-checking.
   -- ONLY IF you define your categories with copatterns though.
diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda
index 2e56a27..7103b9d 100644
--- a/src/Cat/Wishlist.agda
+++ b/src/Cat/Wishlist.agda
@@ -1,6 +1,11 @@
 module Cat.Wishlist where
 
+open import Level
 open import Cubical.NType
 open import Data.Nat using (_≤_ ; z≤n ; s≤s)
 
 postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
+
+-- This follows from [HoTT-book: §7.1.10]
+-- Andrea says the proof is in `cubical` but I can't find it.
+postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (isSet A)

From 44eda0ced0685dfc521d358496b4abaa478418cb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 19 Feb 2018 15:46:19 +0100
Subject: [PATCH 05/23] Stuff about propositionality of fields of `IsCategory`

---
 src/Cat/Category.agda | 97 +++++++++++++++++++++++++++++++++----------
 src/Cat/Wishlist.agda | 10 +++--
 2 files changed, 82 insertions(+), 25 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 1b542be..8d38ec9 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -26,15 +26,9 @@ open import Cat.Wishlist
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
 record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
-  -- adding no-eta-equality can speed up type-checking.
-  -- ONLY IF you define your categories with copatterns though.
   no-eta-equality
   field
-    -- Need something like:
-    -- Object : Σ (Set ℓ) isGroupoid
     Object : Set ℓ
-    -- And:
-    -- Arrow  : Object → Object → Σ (Set ℓ') isSet
     Arrow  : Object → Object → Set ℓ'
     𝟙      : {o : Object} → Arrow o o
     _∘_    : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
@@ -53,15 +47,48 @@ record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
   open RawCategory ℂ
   module Raw = RawCategory ℂ
+
+  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
+
+  IsIdentity : ({A : Object} → Arrow A A) → Set (ℓa ⊔ ℓb)
+  IsIdentity id = {A B : Object} {f : Arrow A B}
+    → f ∘ id ≡ f × id ∘ f ≡ f
+
   field
-    assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
-      → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
-    ident : {A B : Object} {f : Arrow A B}
-      → f ∘ 𝟙 ≡ f × 𝟙 ∘ f ≡ f
+    assoc : IsAssociative
+    ident : IsIdentity 𝟙
     arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
 
+  propIsAssociative : isProp IsAssociative
+  propIsAssociative x y i = arrowIsSet _ _ x y i
+
+  propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f)
+  propIsIdentity a b i
+    = arrowIsSet _ _ (fst a) (fst b) i
+    , arrowIsSet _ _ (snd a) (snd b) i
+
+  propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
+  propArrowIsSet a b i = isSetIsProp a b i
+
+  IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb
+  IsInverseOf = λ f g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
+
+  propIsInverseOf : ∀ {A B f g} → isProp (IsInverseOf {A} {B} f g)
+  propIsInverseOf x y = λ i →
+    let
+      h : fst x ≡ fst y
+      h = arrowIsSet _ _ (fst x) (fst y)
+      hh : snd x ≡ snd y
+      hh = arrowIsSet _ _ (snd x) (snd y)
+    in h i , hh i
+
   Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
-  Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
+  Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g
+
+  inverse : ∀ {A B} {f : Arrow A B} → Isomorphism f → Arrow B A
+  inverse iso = fst iso
 
   _≅_ : (A B : Object) → Set ℓb
   _≅_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f)
@@ -86,19 +113,40 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb
     Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁
 
+  module _ {A B : Object} {f : Arrow A B} where
+    isoIsProp : isProp (Isomorphism f)
+    isoIsProp a@(g , η , ε) a'@(g' , η' , ε') =
+      lemSig (λ g → propIsInverseOf) a a' geq
+      where
+        open Cubical.NType.Properties
+        geq : g ≡ g'
+        geq = begin
+          g            ≡⟨ sym (fst ident) ⟩
+          g ∘ 𝟙        ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
+          g ∘ (f ∘ g') ≡⟨ assoc ⟩
+          (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩
+          𝟙 ∘ g'       ≡⟨ snd ident ⟩
+          g'           ∎
+
+module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} {ℂ : IsCategory C} where
+  open IsCategory ℂ
+  open import Cubical.NType
+  open import Cubical.NType.Properties
+
+  propUnivalent : isProp Univalent
+  propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
+
 module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
   -- TODO, provable by using  arrow-is-set and that isProp (isEquiv _ _ _)
   -- This lemma will be useful to prove the equality of two categories.
   IsCategory-is-prop : isProp (IsCategory ℂ)
   IsCategory-is-prop x y i = record
-    -- Why choose `x`'s `arrowIsSet`?
-    { assoc = x.arrowIsSet _ _ x.assoc y.assoc i
-    ; ident =
-      ( x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i
-      , x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i
-      )
-    ; arrowIsSet = isSetIsProp x.arrowIsSet y.arrowIsSet i
-    ; univalent = {!!}
+    -- Why choose `x`'s `propIsAssociative`?
+    -- Well, probably it could be pulled out of the record.
+    { assoc = x.propIsAssociative x.assoc y.assoc i
+    ; ident = x.propIsIdentity x.ident y.ident i
+    ; arrowIsSet = x.propArrowIsSet x.arrowIsSet y.arrowIsSet i
+    ; univalent = eqUni i
     }
     where
       module x = IsCategory x
@@ -118,12 +166,17 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
             (λ f → Σ-syntax (Arrow (A≡B j) A) (λ g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙)))
             ( 𝟙
             , 𝟙
-            , x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i
-            , x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i
+            , x.propIsIdentity x.ident y.ident i
             )
           )
+      open Cubical.NType.Properties
+      test : (λ _ → x.Univalent) [ xuni ≡ xuni ]
+      test = refl
+      t = {!!}
+      P : (uni : x.Univalent) → xuni ≡ uni → Set (ℓa ⊔ ℓb)
+      P = {!!}
       eqUni : T [ xuni ≡ yuni ]
-      eqUni = {!!}
+      eqUni = pathJprop {x = x.Univalent} P {!!} i
 
 
 record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda
index 7103b9d..d23f52a 100644
--- a/src/Cat/Wishlist.agda
+++ b/src/Cat/Wishlist.agda
@@ -6,6 +6,10 @@ open import Data.Nat using (_≤_ ; z≤n ; s≤s)
 
 postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
 
--- This follows from [HoTT-book: §7.1.10]
--- Andrea says the proof is in `cubical` but I can't find it.
-postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (isSet A)
+module _ {ℓ : Level} {A : Set ℓ} where
+  -- This is §7.1.10 in [HoTT]. Andrea says the proof is in `cubical` but I
+  -- can't find it.
+  postulate propHasLevel : ∀ n → isProp (HasLevel n A)
+
+  isSetIsProp : isProp (isSet A)
+  isSetIsProp = propHasLevel (S (S ⟨-2⟩))

From 38ec53d5c253323878d3d4a8cf18a2706cdee829 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 14:08:47 +0100
Subject: [PATCH 06/23] Cosmetics

---
 README.md                     |  7 +++++--
 src/Cat/Category.agda         | 19 +++++++++++++------
 src/Cat/Category/Functor.agda | 10 +++-------
 3 files changed, 21 insertions(+), 15 deletions(-)

diff --git a/README.md b/README.md
index 4a56ea0..5e0b0cf 100644
--- a/README.md
+++ b/README.md
@@ -5,11 +5,14 @@ consisting of the proposal for the thesis).
 
 Installation
 ============
-You probably need a very recent version of the Agda compiler. At the time
-of writing the solution has been tested with Agda version 2.6.0-5d84754.
 
 Dependencies
 ------------
+To succesfully compile the following is needed:
+
+* Agda version >= `707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43`.
+* Agda Standard Library >= `87d28d7d753f73abd20665d7bbb88f9d72ed88aa`.
+
 I've used git submodules to manage dependencies. Unfortunately Agda does not
 allow specifying libraries to be used only as local dependencies.
 
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 8d38ec9..1d85a81 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -99,7 +99,8 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
   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
+  -- 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)
@@ -144,20 +145,22 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
     -- Why choose `x`'s `propIsAssociative`?
     -- Well, probably it could be pulled out of the record.
     { assoc = x.propIsAssociative x.assoc y.assoc i
-    ; ident = x.propIsIdentity x.ident y.ident i
+    ; ident = ident' i
     ; arrowIsSet = x.propArrowIsSet x.arrowIsSet y.arrowIsSet i
     ; univalent = eqUni i
     }
     where
       module x = IsCategory x
       module y = IsCategory y
+      ident' = x.propIsIdentity x.ident y.ident
+      ident'' = ident' i
       xuni : x.Univalent
       xuni = x.univalent
       yuni : y.Univalent
       yuni = y.univalent
       open RawCategory ℂ
-      T :  I → Set (ℓa ⊔ ℓb)
-      T i = {A B : Object} →
+      Pp : (x.ident ≡ y.ident) → I → Set (ℓa ⊔ ℓb)
+      Pp eqIdent i = {A B : Object} →
         isEquiv (A ≡ B) (A x.≅ B)
           (λ A≡B →
             transp
@@ -166,17 +169,21 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
             (λ f → Σ-syntax (Arrow (A≡B j) A) (λ g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙)))
             ( 𝟙
             , 𝟙
-            , x.propIsIdentity x.ident y.ident i
+            , ident' i
             )
           )
+      T : I → Set (ℓa ⊔ ℓb)
+      T = Pp {!ident'!}
       open Cubical.NType.Properties
       test : (λ _ → x.Univalent) [ xuni ≡ xuni ]
       test = refl
       t = {!!}
       P : (uni : x.Univalent) → xuni ≡ uni → Set (ℓa ⊔ ℓb)
       P = {!!}
+      -- T i0 ≡ x.Univalent
+      -- T i1 ≡ y.Univalent
       eqUni : T [ xuni ≡ yuni ]
-      eqUni = pathJprop {x = x.Univalent} P {!!} i
+      eqUni = {!!}
 
 
 record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index ff5d659..484cfdc 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -47,7 +47,6 @@ module _ {ℓc ℓc' ℓd ℓd'}
 open IsFunctor
 open Functor
 
--- TODO: Is `IsFunctor` a proposition?
 module _
     {ℓa ℓb : Level}
     {ℂ 𝔻 : Category ℓa ℓb}
@@ -56,11 +55,8 @@ module _
   private
     module 𝔻 = IsCategory (isCategory 𝔻)
 
-  -- isProp  : Set ℓ
-  -- isProp  = (x y : A) → x ≡ y
-
-  IsFunctorIsProp : isProp (IsFunctor _ _ F)
-  IsFunctorIsProp isF0 isF1 i = record
+  propIsFunctor : isProp (IsFunctor _ _ F)
+  propIsFunctor isF0 isF1 i = record
     { ident = 𝔻.arrowIsSet _ _ isF0.ident isF1.ident i
     ; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i
     }
@@ -81,7 +77,7 @@ module _
 
   IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
   IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
-    (\ F → IsFunctorIsProp {F = F}) (\ i → F i)
+    (\ F → propIsFunctor {F = F}) (\ i → F i)
     where
       open import Cubical.NType.Properties using (lemPropF)
 

From 10df9511a4e4b878f8469d1ada472c9920e17d2c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 16:22:38 +0100
Subject: [PATCH 07/23] Move various type-synonyms to RawCategory

---
 src/Cat/Category.agda | 68 ++++++++++++++++++++++---------------------
 1 file changed, 35 insertions(+), 33 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 1d85a81..95241fe 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -25,19 +25,46 @@ open import Cat.Wishlist
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
-record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
+record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   no-eta-equality
   field
-    Object : Set ℓ
-    Arrow  : Object → Object → Set ℓ'
-    𝟙      : {o : Object} → Arrow o o
+    Object : Set ℓa
+    Arrow  : Object → Object → Set ℓb
+    𝟙      : {A : Object} → Arrow A A
     _∘_    : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
+
   infixl 10 _∘_
+
   domain : { a b : Object } → Arrow a b → Object
   domain {a = a} _ = a
+
   codomain : { a b : Object } → Arrow a b → Object
   codomain {b = b} _ = b
 
+  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
+
+  IsIdentity : ({A : Object} → Arrow A A) → Set (ℓa ⊔ ℓb)
+  IsIdentity id = {A B : Object} {f : Arrow A B}
+    → f ∘ id ≡ f × id ∘ f ≡ f
+
+  IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb
+  IsInverseOf = λ f g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
+
+  Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
+  Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g
+
+  _≅_ : (A B : Object) → Set ℓb
+  _≅_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f)
+
+  module _ {A B : Object} where
+    Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓb
+    Epimorphism {X} f = ( g₀ g₁ : Arrow B X ) → g₀ ∘ f ≡ g₁ ∘ f → g₀ ≡ g₁
+
+    Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb
+    Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁
+
 -- Thierry: All projections must be `isProp`'s
 
 -- According to definitions 9.1.1 and 9.1.6 in the HoTT book the
@@ -47,15 +74,6 @@ record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
   open RawCategory ℂ
   module Raw = RawCategory ℂ
-
-  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
-
-  IsIdentity : ({A : Object} → Arrow A A) → Set (ℓa ⊔ ℓb)
-  IsIdentity id = {A B : Object} {f : Arrow A B}
-    → f ∘ id ≡ f × id ∘ f ≡ f
-
   field
     assoc : IsAssociative
     ident : IsIdentity 𝟙
@@ -72,9 +90,6 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
   propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
   propArrowIsSet a b i = isSetIsProp a b i
 
-  IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb
-  IsInverseOf = λ f g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
-
   propIsInverseOf : ∀ {A B f g} → isProp (IsInverseOf {A} {B} f g)
   propIsInverseOf x y = λ i →
     let
@@ -84,15 +99,6 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
       hh = arrowIsSet _ _ (snd x) (snd y)
     in h i , hh i
 
-  Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
-  Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g
-
-  inverse : ∀ {A B} {f : Arrow A B} → Isomorphism f → Arrow B A
-  inverse iso = fst iso
-
-  _≅_ : (A B : Object) → Set ℓb
-  _≅_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f)
-
   idIso : (A : Object) → A ≅ A
   idIso A = 𝟙 , (𝟙 , ident)
 
@@ -107,13 +113,6 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
   field
     univalent : Univalent
 
-  module _ {A B : Object} where
-    Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓb
-    Epimorphism {X} f = ( g₀ g₁ : Arrow B X ) → g₀ ∘ f ≡ g₁ ∘ f → g₀ ≡ g₁
-
-    Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb
-    Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁
-
   module _ {A B : Object} {f : Arrow A B} where
     isoIsProp : isProp (Isomorphism f)
     isoIsProp a@(g , η , ε) a'@(g' , η' , ε') =
@@ -161,7 +160,7 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
       open RawCategory ℂ
       Pp : (x.ident ≡ y.ident) → I → Set (ℓa ⊔ ℓb)
       Pp eqIdent i = {A B : Object} →
-        isEquiv (A ≡ B) (A x.≅ B)
+        isEquiv (A ≡ B) (A ≅ B)
           (λ A≡B →
             transp
             (λ j →
@@ -191,9 +190,12 @@ record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     raw : RawCategory ℓa ℓb
     {{isCategory}} : IsCategory raw
 
+  -- What happens if we just open this up to the public?
   private
     module ℂ = RawCategory raw
 
+  open RawCategory raw public using ( Isomorphism ; Epimorphism ; Monomorphism )
+
   Object : Set ℓa
   Object = ℂ.Object
 

From 8ef61d9db06ab25a5c606fbed299badcb41cbf88 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 16:25:49 +0100
Subject: [PATCH 08/23] Simplify Category

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

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 95241fe..2d2c836 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -190,26 +190,13 @@ record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     raw : RawCategory ℓa ℓb
     {{isCategory}} : IsCategory raw
 
-  -- What happens if we just open this up to the public?
-  private
-    module ℂ = RawCategory raw
-
-  open RawCategory raw public using ( Isomorphism ; Epimorphism ; Monomorphism )
-
-  Object : Set ℓa
-  Object = ℂ.Object
-
-  Arrow = ℂ.Arrow
-
-  𝟙 = ℂ.𝟙
-
-  _∘_ = ℂ._∘_
+  open RawCategory raw public
 
   _[_,_] : (A : Object) → (B : Object) → Set ℓb
-  _[_,_] = ℂ.Arrow
+  _[_,_] = Arrow
 
-  _[_∘_] : {A B C : Object} → (g : ℂ.Arrow B C) → (f : ℂ.Arrow A B) → ℂ.Arrow A C
-  _[_∘_] = ℂ._∘_
+  _[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C
+  _[_∘_] = _∘_
 
 
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where

From 860c91f913ee87d3040472ac4ae3466d959e36c3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 16:42:56 +0100
Subject: [PATCH 09/23] Trim mess

---
 src/Cat/Category.agda | 62 +++++++++++++------------------------------
 1 file changed, 18 insertions(+), 44 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 2d2c836..6d60a4e 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -137,53 +137,27 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} {ℂ : IsCategory C} wh
   propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
 
 module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
-  -- TODO, provable by using  arrow-is-set and that isProp (isEquiv _ _ _)
-  -- This lemma will be useful to prove the equality of two categories.
-  IsCategory-is-prop : isProp (IsCategory ℂ)
-  IsCategory-is-prop x y i = record
-    -- Why choose `x`'s `propIsAssociative`?
-    -- Well, probably it could be pulled out of the record.
-    { assoc = x.propIsAssociative x.assoc y.assoc i
-    ; ident = ident' i
-    ; arrowIsSet = x.propArrowIsSet x.arrowIsSet y.arrowIsSet i
-    ; univalent = eqUni i
-    }
-    where
-      module x = IsCategory x
-      module y = IsCategory y
-      ident' = x.propIsIdentity x.ident y.ident
-      ident'' = ident' i
-      xuni : x.Univalent
-      xuni = x.univalent
-      yuni : y.Univalent
-      yuni = y.univalent
-      open RawCategory ℂ
-      Pp : (x.ident ≡ y.ident) → I → Set (ℓa ⊔ ℓb)
-      Pp eqIdent i = {A B : Object} →
-        isEquiv (A ≡ B) (A ≅ B)
-          (λ A≡B →
-            transp
-            (λ j →
-            Σ-syntax (Arrow A (A≡B j))
-            (λ f → Σ-syntax (Arrow (A≡B j) A) (λ g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙)))
-            ( 𝟙
-            , 𝟙
-            , ident' i
-            )
-          )
+  open RawCategory ℂ
+  private
+    module _ (x y : IsCategory ℂ) where
+      module IC = IsCategory
+      module X = IsCategory x
+      module Y = IsCategory y
+      ident = X.propIsIdentity X.ident Y.ident
+      done : x ≡ y
       T : I → Set (ℓa ⊔ ℓb)
-      T = Pp {!ident'!}
-      open Cubical.NType.Properties
-      test : (λ _ → x.Univalent) [ xuni ≡ xuni ]
-      test = refl
-      t = {!!}
-      P : (uni : x.Univalent) → xuni ≡ uni → Set (ℓa ⊔ ℓb)
-      P = {!!}
-      -- T i0 ≡ x.Univalent
-      -- T i1 ≡ y.Univalent
-      eqUni : T [ xuni ≡ yuni ]
+      T i = {A B : Object} →
+        isEquiv (A ≡ B) (A ≅ B)
+        (λ eq → transp (λ i₁ → A ≅ eq i₁) (𝟙 , 𝟙 , ident i))
+      eqUni : T [ X.univalent ≡ Y.univalent ]
       eqUni = {!!}
+      IC.assoc      (done i) = X.propIsAssociative X.assoc Y.assoc i
+      IC.ident      (done i) = ident i
+      IC.arrowIsSet (done i) = X.propArrowIsSet X.arrowIsSet Y.arrowIsSet i
+      IC.univalent  (done i) = eqUni i
 
+  propIsCategory : isProp (IsCategory ℂ)
+  propIsCategory = done
 
 record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   field

From ff496aae09dd5379a21787a68be8ea277f1b6626 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 17:33:02 +0100
Subject: [PATCH 10/23] Factor out a useful type-family

---
 src/Cat/Category.agda | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 6d60a4e..7896d02 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -143,13 +143,20 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
       module IC = IsCategory
       module X = IsCategory x
       module Y = IsCategory y
+      -- ident : X.ident {?} ≡ Y.ident
+      ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ]
       ident = X.propIsIdentity X.ident Y.ident
-      done : x ≡ y
-      T : I → Set (ℓa ⊔ ℓb)
-      T i = {A B : Object} →
+      -- A version of univalence indexed by the identity proof.
+      -- Not of course that since it's defined where `RawCategory ℂ` has been opened
+      -- this is specialized to that category.
+      Univ : IsIdentity 𝟙 → Set _
+      Univ idnt = {A B : Y.Raw.Object} →
         isEquiv (A ≡ B) (A ≅ B)
-        (λ eq → transp (λ i₁ → A ≅ eq i₁) (𝟙 , 𝟙 , ident i))
-      eqUni : T [ X.univalent ≡ Y.univalent ]
+        (λ eq → transp (λ j → A ≅ eq j) (𝟙 , 𝟙 , idnt))
+      done : x ≡ y
+      U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] → (b : Univ a) → Set _
+      U eqwal bbb = (λ i → Univ (eqwal i)) [ X.univalent ≡ bbb ]
+      eqUni : U ident Y.univalent
       eqUni = {!!}
       IC.assoc      (done i) = X.propIsAssociative X.assoc Y.assoc i
       IC.ident      (done i) = ident i

From a016c67b883c473ff68eaf9c9a32309cfa5041c7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 17:44:44 +0100
Subject: [PATCH 11/23] Succesfully apply path-induction.

Now all that's left to do is prove the original proposition in a
heterogenous equality
---
 src/Cat/Category.agda | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 7896d02..efc6727 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -147,7 +147,7 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
       ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ]
       ident = X.propIsIdentity X.ident Y.ident
       -- A version of univalence indexed by the identity proof.
-      -- Not of course that since it's defined where `RawCategory ℂ` has been opened
+      -- Note of course that since it's defined where `RawCategory ℂ` has been opened
       -- this is specialized to that category.
       Univ : IsIdentity 𝟙 → Set _
       Univ idnt = {A B : Y.Raw.Object} →
@@ -156,8 +156,15 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
       done : x ≡ y
       U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] → (b : Univ a) → Set _
       U eqwal bbb = (λ i → Univ (eqwal i)) [ X.univalent ≡ bbb ]
+      P : (y : IsIdentity 𝟙)
+        → (λ _ → IsIdentity 𝟙) [ X.ident ≡ y ] → Set _
+      P y eq = ∀ (b' : Univ y) → U eq b'
+      helper : ∀ (b' : Univ X.ident)
+        → (λ _ → Univ X.ident) [ X.univalent ≡ b' ]
+      helper univ = {!!}
+      foo = pathJ P helper Y.ident ident
       eqUni : U ident Y.univalent
-      eqUni = {!!}
+      eqUni = foo Y.univalent
       IC.assoc      (done i) = X.propIsAssociative X.assoc Y.assoc i
       IC.ident      (done i) = ident i
       IC.arrowIsSet (done i) = X.propArrowIsSet X.arrowIsSet Y.arrowIsSet i

From 159bffa6ae708cc76411973e33193ff0d02352a3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 17:59:48 +0100
Subject: [PATCH 12/23] Factor out more from `IsCategory`

---
 src/Cat/Category.agda | 100 ++++++++++++++++++++++--------------------
 1 file changed, 52 insertions(+), 48 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index efc6727..224e279 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -79,26 +79,6 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     ident : IsIdentity 𝟙
     arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
 
-  propIsAssociative : isProp IsAssociative
-  propIsAssociative x y i = arrowIsSet _ _ x y i
-
-  propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f)
-  propIsIdentity a b i
-    = arrowIsSet _ _ (fst a) (fst b) i
-    , arrowIsSet _ _ (snd a) (snd b) i
-
-  propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
-  propArrowIsSet a b i = isSetIsProp a b i
-
-  propIsInverseOf : ∀ {A B f g} → isProp (IsInverseOf {A} {B} f g)
-  propIsInverseOf x y = λ i →
-    let
-      h : fst x ≡ fst y
-      h = arrowIsSet _ _ (fst x) (fst y)
-      hh : snd x ≡ snd y
-      hh = arrowIsSet _ _ (snd x) (snd y)
-    in h i , hh i
-
   idIso : (A : Object) → A ≅ A
   idIso A = 𝟙 , (𝟙 , ident)
 
@@ -113,39 +93,63 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
   field
     univalent : Univalent
 
-  module _ {A B : Object} {f : Arrow A B} where
-    isoIsProp : isProp (Isomorphism f)
-    isoIsProp a@(g , η , ε) a'@(g' , η' , ε') =
-      lemSig (λ g → propIsInverseOf) a a' geq
-      where
-        open Cubical.NType.Properties
-        geq : g ≡ g'
-        geq = begin
-          g            ≡⟨ sym (fst ident) ⟩
-          g ∘ 𝟙        ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
-          g ∘ (f ∘ g') ≡⟨ assoc ⟩
-          (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩
-          𝟙 ∘ g'       ≡⟨ snd ident ⟩
-          g'           ∎
+-- `IsCategory` is a mere proposition.
+module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
+  open RawCategory C
+  module _ (ℂ : IsCategory C) where
+    open IsCategory ℂ
+    open import Cubical.NType
+    open import Cubical.NType.Properties
 
-module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} {ℂ : IsCategory C} where
-  open IsCategory ℂ
-  open import Cubical.NType
-  open import Cubical.NType.Properties
+    propIsAssociative : isProp IsAssociative
+    propIsAssociative x y i = arrowIsSet _ _ x y i
 
-  propUnivalent : isProp Univalent
-  propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
+    propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f)
+    propIsIdentity a b i
+      = arrowIsSet _ _ (fst a) (fst b) i
+      , arrowIsSet _ _ (snd a) (snd b) i
+
+    propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
+    propArrowIsSet a b i = isSetIsProp a b i
+
+    propIsInverseOf : ∀ {A B f g} → isProp (IsInverseOf {A} {B} f g)
+    propIsInverseOf x y = λ i →
+      let
+        h : fst x ≡ fst y
+        h = arrowIsSet _ _ (fst x) (fst y)
+        hh : snd x ≡ snd y
+        hh = arrowIsSet _ _ (snd x) (snd y)
+      in h i , hh i
+
+    module _ {A B : Object} {f : Arrow A B} where
+      isoIsProp : isProp (Isomorphism f)
+      isoIsProp a@(g , η , ε) a'@(g' , η' , ε') =
+        lemSig (λ g → propIsInverseOf) a a' geq
+          where
+            open Cubical.NType.Properties
+            geq : g ≡ g'
+            geq = begin
+              g            ≡⟨ sym (fst ident) ⟩
+              g ∘ 𝟙        ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
+              g ∘ (f ∘ g') ≡⟨ assoc ⟩
+              (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩
+              𝟙 ∘ g'       ≡⟨ snd ident ⟩
+              g'           ∎
+
+    propUnivalent : isProp Univalent
+    propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
 
-module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
-  open RawCategory ℂ
   private
-    module _ (x y : IsCategory ℂ) where
+    module _ (x y : IsCategory C) where
       module IC = IsCategory
       module X = IsCategory x
       module Y = IsCategory y
-      -- ident : X.ident {?} ≡ Y.ident
+      -- In a few places I use the result of propositionality of the various
+      -- projections of `IsCategory` - I've arbitrarily chosed to use this
+      -- result from `x : IsCategory C`. I don't know which (if any) possibly
+      -- adverse effects this may have.
       ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ]
-      ident = X.propIsIdentity X.ident Y.ident
+      ident = propIsIdentity x X.ident Y.ident
       -- A version of univalence indexed by the identity proof.
       -- Note of course that since it's defined where `RawCategory ℂ` has been opened
       -- this is specialized to that category.
@@ -165,12 +169,12 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
       foo = pathJ P helper Y.ident ident
       eqUni : U ident Y.univalent
       eqUni = foo Y.univalent
-      IC.assoc      (done i) = X.propIsAssociative X.assoc Y.assoc i
+      IC.assoc      (done i) = propIsAssociative x X.assoc Y.assoc i
       IC.ident      (done i) = ident i
-      IC.arrowIsSet (done i) = X.propArrowIsSet X.arrowIsSet Y.arrowIsSet i
+      IC.arrowIsSet (done i) = propArrowIsSet x X.arrowIsSet Y.arrowIsSet i
       IC.univalent  (done i) = eqUni i
 
-  propIsCategory : isProp (IsCategory ℂ)
+  propIsCategory : isProp (IsCategory C)
   propIsCategory = done
 
 record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where

From a4f8a37e365e01701f40a8cb83379074a9ee02d2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 18:01:26 +0100
Subject: [PATCH 13/23] Proove that `IsCategory` is a mere proposition!

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

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 224e279..df9e67f 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -165,7 +165,7 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
       P y eq = ∀ (b' : Univ y) → U eq b'
       helper : ∀ (b' : Univ X.ident)
         → (λ _ → Univ X.ident) [ X.univalent ≡ b' ]
-      helper univ = {!!}
+      helper univ = propUnivalent x X.univalent univ
       foo = pathJ P helper Y.ident ident
       eqUni : U ident Y.univalent
       eqUni = foo Y.univalent

From 0c861c4bde935e1cc1d23d46c6685ffdfe88e6b9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 18:11:14 +0100
Subject: [PATCH 14/23] Factor univalence out to a seperate module

---
 src/Cat/Category.agda | 53 ++++++++++++++++++++-----------------------
 1 file changed, 25 insertions(+), 28 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index df9e67f..ee71821 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -65,6 +65,22 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb
     Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁
 
+-- Univalence is indexed by a raw category as well as an identity proof.
+module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
+  open RawCategory ℂ
+  module _ (ident : IsIdentity 𝟙) where
+    idIso : (A : Object) → A ≅ A
+    idIso A = 𝟙 , (𝟙 , ident)
+
+    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)
+
 -- Thierry: All projections must be `isProp`'s
 
 -- According to definitions 9.1.1 and 9.1.6 in the HoTT book the
@@ -73,25 +89,12 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
 -- (univalent).
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
   open RawCategory ℂ
-  module Raw = RawCategory ℂ
+  open Univalence ℂ public
   field
     assoc : IsAssociative
     ident : IsIdentity 𝟙
     arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
-
-  idIso : (A : Object) → A ≅ A
-  idIso A = 𝟙 , (𝟙 , ident)
-
-  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)
-  field
-    univalent : Univalent
+    univalent : Univalent ident
 
 -- `IsCategory` is a mere proposition.
 module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
@@ -136,7 +139,7 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
               𝟙 ∘ g'       ≡⟨ snd ident ⟩
               g'           ∎
 
-    propUnivalent : isProp Univalent
+    propUnivalent : isProp (Univalent ident)
     propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
 
   private
@@ -144,27 +147,21 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
       module IC = IsCategory
       module X = IsCategory x
       module Y = IsCategory y
+      open Univalence C
       -- In a few places I use the result of propositionality of the various
       -- projections of `IsCategory` - I've arbitrarily chosed to use this
       -- result from `x : IsCategory C`. I don't know which (if any) possibly
       -- adverse effects this may have.
       ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ]
       ident = propIsIdentity x X.ident Y.ident
-      -- A version of univalence indexed by the identity proof.
-      -- Note of course that since it's defined where `RawCategory ℂ` has been opened
-      -- this is specialized to that category.
-      Univ : IsIdentity 𝟙 → Set _
-      Univ idnt = {A B : Y.Raw.Object} →
-        isEquiv (A ≡ B) (A ≅ B)
-        (λ eq → transp (λ j → A ≅ eq j) (𝟙 , 𝟙 , idnt))
       done : x ≡ y
-      U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] → (b : Univ a) → Set _
-      U eqwal bbb = (λ i → Univ (eqwal i)) [ X.univalent ≡ bbb ]
+      U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] → (b : Univalent a) → Set _
+      U eqwal bbb = (λ i → Univalent (eqwal i)) [ X.univalent ≡ bbb ]
       P : (y : IsIdentity 𝟙)
         → (λ _ → IsIdentity 𝟙) [ X.ident ≡ y ] → Set _
-      P y eq = ∀ (b' : Univ y) → U eq b'
-      helper : ∀ (b' : Univ X.ident)
-        → (λ _ → Univ X.ident) [ X.univalent ≡ b' ]
+      P y eq = ∀ (b' : Univalent y) → U eq b'
+      helper : ∀ (b' : Univalent X.ident)
+        → (λ _ → Univalent X.ident) [ X.univalent ≡ b' ]
       helper univ = propUnivalent x X.univalent univ
       foo = pathJ P helper Y.ident ident
       eqUni : U ident Y.univalent

From d2da84269f367c67afb127ebc87b79850fd3f107 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 18:14:42 +0100
Subject: [PATCH 15/23] Move some more things into `RawCategory`

---
 src/Cat/Category.agda | 33 ++++++++++++++++-----------------
 1 file changed, 16 insertions(+), 17 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index ee71821..27f271e 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -65,6 +65,22 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb
     Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁
 
+  unique = isContr
+
+  IsInitial : Object → Set (ℓa ⊔ ℓb)
+  IsInitial I = {X : Object} → unique (Arrow I X)
+
+  IsTerminal : Object → Set (ℓa ⊔ ℓb)
+  -- ∃![ ? ] ?
+  IsTerminal T = {X : Object} → unique (Arrow X T)
+
+  Initial : Set (ℓa ⊔ ℓb)
+  Initial = Σ (Object) IsInitial
+
+  Terminal : Set (ℓa ⊔ ℓb)
+  Terminal = Σ (Object) IsTerminal
+
+
 -- Univalence is indexed by a raw category as well as an identity proof.
 module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   open RawCategory ℂ
@@ -235,20 +251,3 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
   Opposite-is-involution : Opposite (Opposite ℂ) ≡ ℂ
   raw (Opposite-is-involution i) = rawOp i
   isCategory (Opposite-is-involution i) = rawIsCat i
-
-module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-  open Category
-  unique = isContr
-
-  IsInitial : Object ℂ → Set (ℓa ⊔ ℓb)
-  IsInitial I = {X : Object ℂ} → unique (ℂ [ I , X ])
-
-  IsTerminal : Object ℂ → Set (ℓa ⊔ ℓb)
-  -- ∃![ ? ] ?
-  IsTerminal T = {X : Object ℂ} → unique (ℂ [ X , T ])
-
-  Initial : Set (ℓa ⊔ ℓb)
-  Initial = Σ (Object ℂ) IsInitial
-
-  Terminal : Set (ℓa ⊔ ℓb)
-  Terminal = Σ (Object ℂ) IsTerminal

From edf552cb86191732c7bb6bf1949e85cdcce6a31b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 18:15:07 +0100
Subject: [PATCH 16/23] Do not define synonym for contractible

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

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 27f271e..50f21cd 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -65,14 +65,11 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb
     Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁
 
-  unique = isContr
-
   IsInitial : Object → Set (ℓa ⊔ ℓb)
-  IsInitial I = {X : Object} → unique (Arrow I X)
+  IsInitial I = {X : Object} → isContr (Arrow I X)
 
   IsTerminal : Object → Set (ℓa ⊔ ℓb)
-  -- ∃![ ? ] ?
-  IsTerminal T = {X : Object} → unique (Arrow X T)
+  IsTerminal T = {X : Object} → isContr (Arrow X T)
 
   Initial : Set (ℓa ⊔ ℓb)
   Initial = Σ (Object) IsInitial
@@ -80,7 +77,6 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   Terminal : Set (ℓa ⊔ ℓb)
   Terminal = Σ (Object) IsTerminal
 
-
 -- Univalence is indexed by a raw category as well as an identity proof.
 module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   open RawCategory ℂ

From ed40824edc3da61ea346a935eefb320c507924e5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 21 Feb 2018 12:59:31 +0100
Subject: [PATCH 17/23] Cosmetics

---
 src/Cat/Category.agda | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 50f21cd..69c4aa8 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -65,17 +65,17 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb
     Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁
 
-  IsInitial : Object → Set (ℓa ⊔ ℓb)
-  IsInitial I = {X : Object} → isContr (Arrow I X)
+  IsInitial  : Object → Set (ℓa ⊔ ℓb)
+  IsInitial  I = {X : Object} → isContr (Arrow I X)
 
   IsTerminal : Object → Set (ℓa ⊔ ℓb)
   IsTerminal T = {X : Object} → isContr (Arrow X T)
 
-  Initial : Set (ℓa ⊔ ℓb)
-  Initial = Σ (Object) IsInitial
+  Initial  : Set (ℓa ⊔ ℓb)
+  Initial  = Σ Object IsInitial
 
   Terminal : Set (ℓa ⊔ ℓb)
-  Terminal = Σ (Object) IsTerminal
+  Terminal = Σ Object IsTerminal
 
 -- Univalence is indexed by a raw category as well as an identity proof.
 module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where

From 57d7eab4cb9fc2cc366f398e96de44deb65f2a31 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 21 Feb 2018 13:37:07 +0100
Subject: [PATCH 18/23] Make sets a category according to HoTT

---
 src/Cat/Categories/Sets.agda | 168 +++++++++++++++++++++--------------
 src/Cat/Category.agda        |  13 +--
 2 files changed, 106 insertions(+), 75 deletions(-)

diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 5263aa1..4d23936 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -9,80 +9,116 @@ import Function
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
-open Category
+
+module _ (ℓ : Level) where
+  private
+    open RawCategory
+    open IsCategory
+    open import Cubical.Univalence
+    open import Cubical.NType.Properties
+    open import Cubical.Universe
+
+    SetsRaw : RawCategory (lsuc ℓ) ℓ
+    Object SetsRaw = Cubical.Universe.0-Set
+    Arrow SetsRaw (T , _) (U , _) = T → U
+    𝟙 SetsRaw = Function.id
+    _∘_ SetsRaw = Function._∘′_
+
+    setIsSet : (A : Set ℓ) → isSet A
+    setIsSet A x y p q = {!ua!}
+
+    SetsIsCategory : IsCategory SetsRaw
+    assoc SetsIsCategory = refl
+    proj₁ (ident SetsIsCategory) = funExt λ _ → refl
+    proj₂ (ident SetsIsCategory) = funExt λ _ → refl
+    arrowIsSet SetsIsCategory {B = (_ , s)} = setPi λ _ → s
+    univalent SetsIsCategory = {!!}
+
+  𝓢𝓮𝓽 Sets : Category (lsuc ℓ) ℓ
+  Category.raw 𝓢𝓮𝓽 = SetsRaw
+  Category.isCategory 𝓢𝓮𝓽 = SetsIsCategory
+  Sets = 𝓢𝓮𝓽
 
 module _ {ℓ : Level} where
-  SetsRaw : RawCategory (lsuc ℓ) ℓ
-  RawCategory.Object SetsRaw = Set ℓ
-  RawCategory.Arrow SetsRaw = λ T U → T → U
-  RawCategory.𝟙 SetsRaw = Function.id
-  RawCategory._∘_ SetsRaw = Function._∘′_
-
-  open IsCategory
-  SetsIsCategory : IsCategory SetsRaw
-  assoc SetsIsCategory = refl
-  proj₁ (ident SetsIsCategory) = funExt λ _ → refl
-  proj₂ (ident SetsIsCategory) = funExt λ _ → refl
-  arrowIsSet SetsIsCategory = {!!}
-  univalent SetsIsCategory = {!!}
-
-  Sets : Category (lsuc ℓ) ℓ
-  raw Sets = SetsRaw
-  isCategory Sets = SetsIsCategory
-
   private
-    module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
-      _&&&_ : (X → A × B)
-      _&&&_ x = f x , g x
-    module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
-      lem : Sets [ proj₁ ∘ (f &&& g)] ≡ f × Sets [ proj₂ ∘ (f &&& g)] ≡ g
-      proj₁ lem = refl
-      proj₂ lem = refl
-    instance
-      isProduct : {A B : Object Sets} → IsProduct Sets {A} {B} proj₁ proj₂
-      isProduct f g = f &&& g , lem f g
+    𝓢 = 𝓢𝓮𝓽 ℓ
+    open Category 𝓢
+    open import Cubical.Sigma
 
-    product : (A B : Object Sets) → Product {ℂ = Sets} A B
-    product A B = record { obj = A × B ; proj₁ = proj₁ ; proj₂ = proj₂ ; isProduct = isProduct }
+    module _ (0A 0B : Object) where
+      private
+        A : Set ℓ
+        A = proj₁ 0A
+        sA : isSet A
+        sA = proj₂ 0A
+        B : Set ℓ
+        B = proj₁ 0B
+        sB : isSet B
+        sB = proj₂ 0B
+        0A×0B : Object
+        0A×0B = (A × B) , sigPresSet sA λ _ → sB
+
+        module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
+          _&&&_ : (X → A × B)
+          _&&&_ x = f x , g x
+        module _ {0X : Object} where
+          X = proj₁ 0X
+          module _ (f : X → A ) (g : X → B) where
+            lem : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g
+            proj₁ lem = refl
+            proj₂ lem = refl
+        instance
+          isProduct : IsProduct 𝓢 {0A} {0B} {0A×0B} proj₁ proj₂
+          isProduct {X = X} f g = (f &&& g) , lem {0X = X} f g
+
+      product : Product {ℂ = 𝓢} 0A 0B
+      product = record
+        { obj = 0A×0B
+        ; proj₁ = Data.Product.proj₁
+        ; proj₂ = Data.Product.proj₂
+        ; isProduct = λ { {X} → isProduct {X = X}}
+        }
 
   instance
-    SetsHasProducts : HasProducts Sets
+    SetsHasProducts : HasProducts 𝓢
     SetsHasProducts = record { product = product }
 
--- Covariant Presheaf
-Representable : {ℓ ℓ' : Level} → (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
-Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
+module _ {ℓa ℓb : Level} where
+  module _ (ℂ : Category ℓa ℓb) where
+    -- Covariant Presheaf
+    Representable : Set (ℓa ⊔ lsuc ℓb)
+    Representable = Functor ℂ (𝓢𝓮𝓽 ℓb)
 
--- The "co-yoneda" embedding.
-representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
-representable {ℂ = ℂ} A = record
-  { raw = record
-    { func* = λ B → ℂ [ A , B ]
-    ; func→ = ℂ [_∘_]
-    }
-  ; isFunctor = record
-    { ident = funExt λ _ → proj₂ ident
-    ; distrib = funExt λ x → sym assoc
-    }
-  }
-  where
-    open IsCategory (isCategory ℂ)
+    -- Contravariant Presheaf
+    Presheaf : Set (ℓa ⊔ lsuc ℓb)
+    Presheaf = Functor (Opposite ℂ) (𝓢𝓮𝓽 ℓb)
 
--- Contravariant Presheaf
-Presheaf : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
-Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
-
--- Alternate name: `yoneda`
-presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ
-presheaf {ℂ = ℂ} B = record
-  { raw = record
-    { func* = λ A → ℂ [ A , B ]
-    ; func→ = λ f g → ℂ [ g ∘ f ]
-  }
-  ; isFunctor = record
-    { ident = funExt λ x → proj₁ ident
-    ; distrib = funExt λ x → assoc
+  -- The "co-yoneda" embedding.
+  representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
+  representable {ℂ = ℂ} A = record
+    { raw = record
+      { func* = λ B → ℂ [ A , B ] , arrowIsSet
+      ; func→ = ℂ [_∘_]
+      }
+    ; isFunctor = record
+      { ident = funExt λ _ → proj₂ ident
+      ; distrib = funExt λ x → sym assoc
+      }
     }
-  }
-  where
-    open IsCategory (isCategory ℂ)
+    where
+      open Category ℂ
+
+  -- Alternate name: `yoneda`
+  presheaf : {ℂ : Category ℓa ℓb} → Category.Object (Opposite ℂ) → Presheaf ℂ
+  presheaf {ℂ = ℂ} B = record
+    { raw = record
+      { func* = λ A → ℂ [ A , B ] , arrowIsSet
+      ; func→ = λ f g → ℂ [ g ∘ f ]
+    }
+    ; isFunctor = record
+      { ident = funExt λ x → proj₁ ident
+      ; distrib = funExt λ x → assoc
+      }
+    }
+    where
+      open Category ℂ
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 69c4aa8..686ae76 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -84,6 +84,7 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
     idIso : (A : Object) → A ≅ A
     idIso A = 𝟙 , (𝟙 , ident)
 
+    -- Lemma 9.1.4 in [HoTT]
     id-to-iso : (A B : Object) → A ≡ B → A ≅ B
     id-to-iso A B eq = transp (\ i → A ≅ eq i) (idIso A)
 
@@ -93,12 +94,6 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
     Univalent : Set (ℓa ⊔ ℓb)
     Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
 
--- Thierry: All projections must be `isProp`'s
-
--- According to definitions 9.1.1 and 9.1.6 in the HoTT book the
--- arrows of a category form a set (arrow-is-set), and there is an
--- equivalence between the equality of objects and isomorphisms
--- (univalent).
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
   open RawCategory ℂ
   open Univalence ℂ public
@@ -192,14 +187,16 @@ record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     {{isCategory}} : IsCategory raw
 
   open RawCategory raw public
+  open IsCategory isCategory public
 
+module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  open Category ℂ
   _[_,_] : (A : Object) → (B : Object) → Set ℓb
   _[_,_] = Arrow
 
   _[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C
   _[_∘_] = _∘_
 
-
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   private
     open Category ℂ
@@ -210,8 +207,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     RawCategory.𝟙 OpRaw = 𝟙
     RawCategory._∘_ OpRaw = Function.flip _∘_
 
-    open IsCategory isCategory
-
     OpIsCategory : IsCategory OpRaw
     IsCategory.assoc OpIsCategory = sym assoc
     IsCategory.ident OpIsCategory = swap ident

From 9e96e704e8fabbcad852b7a47836ba8716bc8b0f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 21 Feb 2018 13:40:24 +0100
Subject: [PATCH 19/23] Update `Fun` according to new naming policy

---
 src/Cat/Categories/Fun.agda      | 12 ++++++------
 src/Cat/Category/Properties.agda |  1 -
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index ada60d2..ba492d0 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -21,7 +21,7 @@ open import Cat.Equality
 open Equality.Data.Product
 
 module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
-  open Category hiding ( _∘_ ; Arrow )
+  open Category using (Object ; 𝟙)
   open Functor
 
   module _ (F G : Functor ℂ 𝔻) where
@@ -70,7 +70,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     where
       module F = Functor F
       F→ = F.func→
-      module 𝔻 = IsCategory (isCategory 𝔻)
+      module 𝔻 = Category 𝔻
 
   identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F
   identityNat F = identityTrans F , identityNatural F
@@ -95,13 +95,13 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
       𝔻 [ H.func→ f ∘ (θ ∘nt η) A ]     ∎
       where
-        open IsCategory (isCategory 𝔻)
+        open Category 𝔻
 
     NatComp = _:⊕:_
 
   private
     module _ {F G : Functor ℂ 𝔻} where
-      module 𝔻 = IsCategory (isCategory 𝔻)
+      module 𝔻 = Category 𝔻
 
       transformationIsSet : isSet (Transformation F G)
       transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C)   (λ l → q l C) i j
@@ -139,7 +139,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       :assoc: = lemSig (naturalIsProp {F = A} {D})
         L R (funExt (λ x → assoc))
         where
-          open IsCategory (isCategory 𝔻)
+          open Category 𝔻
 
     module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
       private
@@ -181,7 +181,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       }
 
   Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
-  raw Fun = RawFun
+  Category.raw Fun = RawFun
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   open import Cat.Categories.Sets
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index a656b4c..b001344 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -14,7 +14,6 @@ open Equality.Data.Product
 
 module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where
   open Category ℂ
-  open IsCategory (isCategory)
 
   iso-is-epi : Isomorphism f → Epimorphism {X = X} f
   iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin

From 8f620e0dbe9b96dcd1801c47e0d10b1852e07b78 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 21 Feb 2018 13:43:26 +0100
Subject: [PATCH 20/23] Update commit references

---
 libs/agda-stdlib | 2 +-
 libs/cubical     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/libs/agda-stdlib b/libs/agda-stdlib
index 157497a..87d28d7 160000
--- a/libs/agda-stdlib
+++ b/libs/agda-stdlib
@@ -1 +1 @@
-Subproject commit 157497a5335ad0069c7aaffbc65932c40a28ee68
+Subproject commit 87d28d7d753f73abd20665d7bbb88f9d72ed88aa
diff --git a/libs/cubical b/libs/cubical
index 12c2c62..9bfbacb 160000
--- a/libs/cubical
+++ b/libs/cubical
@@ -1 +1 @@
-Subproject commit 12c2c628e9e202f1698a4c32e0356d5ca8cb6151
+Subproject commit 9bfbacbb30d4673332566f6e4a58fd04e3904106

From 7398210a2b19e33b90bcb2d5abbd3b18560f0a77 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 21 Feb 2018 13:52:51 +0100
Subject: [PATCH 21/23] Update readme

---
 README.md | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index 5e0b0cf..dc8c40e 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,11 @@
 Description
 ===========
-This project includes code as well as my masters thesis (currently just
-consisting of the proposal for the thesis).
+This project aims to formalize some parts of category theory using cubical agda
+&mdash; an extension to agda permitting univalence. To learn more about this
+[readthedocs](https://agda.readthedocs.io/en/latest/language/cubical.html).
+
+This project draws a lot of inspiration from [the
+HoTT-book](https://homotopytypetheory.org/book/).
 
 Installation
 ============
@@ -11,10 +15,15 @@ Dependencies
 To succesfully compile the following is needed:
 
 * Agda version >= `707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43`.
-* Agda Standard Library >= `87d28d7d753f73abd20665d7bbb88f9d72ed88aa`.
+* [Agda Standard Library](https://github.com/agda/agda-stdlib)
+* [Cubical](https://github.com/Saizan/cubical-demo/)
+
+It's important to have the right version of these - but which one is the right
+is in constant flux. It's most likely the newest one.
 
 I've used git submodules to manage dependencies. Unfortunately Agda does not
-allow specifying libraries to be used only as local dependencies.
+allow specifying libraries to be used only as local dependencies. So the
+submodules are mostly used for documentation.
 
 You can let Agda know about these libraries by appending them to your global
 libraries file like so: (NB!: There is a good reason this is not in a

From a82095604d0d2b726c405f0cefd6a4582b0c344a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 21 Feb 2018 14:05:10 +0100
Subject: [PATCH 22/23] Remove unused function

---
 src/Cat/Categories/Sets.agda | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 4d23936..d6c1329 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -24,9 +24,6 @@ module _ (ℓ : Level) where
     𝟙 SetsRaw = Function.id
     _∘_ SetsRaw = Function._∘′_
 
-    setIsSet : (A : Set ℓ) → isSet A
-    setIsSet A x y p q = {!ua!}
-
     SetsIsCategory : IsCategory SetsRaw
     assoc SetsIsCategory = refl
     proj₁ (ident SetsIsCategory) = funExt λ _ → refl

From 7ed99a6bb409e500ce5c02f659933bb44b22113c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 21 Feb 2018 14:06:09 +0100
Subject: [PATCH 23/23] Add backlog and changelog

---
 BACKLOG.md   |  6 ++++++
 CHANGELOG.md | 17 +++++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 BACKLOG.md
 create mode 100644 CHANGELOG.md

diff --git a/BACKLOG.md b/BACKLOG.md
new file mode 100644
index 0000000..c791f61
--- /dev/null
+++ b/BACKLOG.md
@@ -0,0 +1,6 @@
+Backlog
+=======
+
+Prove univalence for various categories
+
+Prove postulates in `Cat.Wishlist`
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000..cc79e6c
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,17 @@
+Changelog
+=========
+
+Version 1.1.0
+-------------
+In this version categories have been refactored - there's now a notion of a raw
+category, and a proper category which has the data (raw category) as well as
+the laws.
+
+Furthermore the type of arrows must be homotopy sets and they must satisfy univalence.
+
+I've made a module `Cat.Wishlist` where I just postulate things that I hope to
+implement upstream in `cubical`.
+
+I have proven that `IsCategory` is a mere proposition.
+
+I've also updated the category of sets to adhere to this new definition.