diff --git a/libs/agda-stdlib b/libs/agda-stdlib
index b5bfbc3..157497a 160000
--- a/libs/agda-stdlib
+++ b/libs/agda-stdlib
@@ -1 +1 @@
-Subproject commit b5bfbc3c170b0bd0c9aaac1b4d4b3f9b06832bf6
+Subproject commit 157497a5335ad0069c7aaffbc65932c40a28ee68
diff --git a/libs/cubical b/libs/cubical
index 1d6730c..12c2c62 160000
--- a/libs/cubical
+++ b/libs/cubical
@@ -1 +1 @@
-Subproject commit 1d6730c4999daa2b04e9dd39faa0791d0b5c3b48
+Subproject commit 12c2c628e9e202f1698a4c32e0356d5ca8cb6151
diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda
index 16b37c0..703a7d2 100644
--- a/src/Cat/Categories/Free.agda
+++ b/src/Cat/Categories/Free.agda
@@ -44,7 +44,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
       --   ident-r : concatenate {A} {A} {B} p (lift 𝟙) ≡ p
       --   ident-l : concatenate {A} {B} {B} (lift 𝟙) p ≡ p
     module _ {A B : Object ℂ} where
-      isSet : IsSet (Path A B)
+      isSet : Cubical.isSet (Path A B)
       isSet = {!!}
   RawFree : RawCategory ℓ (ℓ ⊔ ℓ')
   RawFree = record
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index e60a118..522bb34 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -1,13 +1,23 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --allow-unsolved-metas --cubical #-}
 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 Data.Nat using (_≤_ ; z≤n ; s≤s)
+module Nat = Data.Nat
 
 open import Cat.Category
 open import Cat.Category.Functor
+open import Cat.Wishlist
+
+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 )
@@ -27,6 +37,9 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       → (f : ℂ [ A , B ])
       → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
 
+    -- naturalIsProp : ∀ θ → isProp (Natural θ)
+    -- naturalIsProp θ x y = {!funExt!}
+
     NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
     NaturalTransformation = Σ Transformation Natural
 
@@ -86,12 +99,39 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     NatComp = _:⊕:_
 
   private
-    module _ {A B C D : Functor ℂ 𝔻} {f : NaturalTransformation A B}
-      {g : NaturalTransformation B C} {h : NaturalTransformation C D} where
+    module _ {F G : Functor ℂ 𝔻} where
+      module 𝔻 = IsCategory (isCategory 𝔻)
+
+      transformationIsSet : isSet (Transformation F G)
+      transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C)   (λ l → q l C) i j
+      IsSet'   : {ℓ : Level} (A : Set ℓ) → Set ℓ
+      IsSet' A = {x y : A} → (p q : (λ _ → A) [ x ≡ y ]) → p ≡ q
+
+      naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
+      naturalIsProp θ θNat θNat' = lem
+        where
+          lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
+          lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i
+
+      naturalTransformationIsSets : isSet (NaturalTransformation F G)
+      naturalTransformationIsSets = sigPresSet transformationIsSet
+        λ θ → ntypeCommulative
+          (s≤s {n = Nat.suc Nat.zero} z≤n)
+          (naturalIsProp θ)
+
+    module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B}
+      {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
+      private
+        θ = proj₁ θ'
+        η = proj₁ η'
+        ζ = proj₁ ζ'
       _g⊕f_ = _:⊕:_ {A} {B} {C}
       _h⊕g_ = _:⊕:_ {B} {C} {D}
-      :assoc: : (_:⊕:_ {A} {C} {D} h (_:⊕:_ {A} {B} {C} g f)) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} h g) f)
-      :assoc: = {!!}
+      :assoc: : (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ')) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
+      :assoc: = Σ≡ (funExt (λ _ → assoc)) {!!}
+        where
+          open IsCategory (isCategory 𝔻)
+
     module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
       ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
       ident-r = {!!}
@@ -116,7 +156,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     :isCategory: = record
       { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D}
       ; ident = λ {A B} → :ident: {A} {B}
-      ; arrowIsSet = {!!}
+      ; arrowIsSet = λ {F} {G} → naturalTransformationIsSets {F} {G}
       ; univalent = {!!}
       }
 
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 168b2fc..cee681f 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -11,8 +11,8 @@ open import Data.Product renaming
   )
 open import Data.Empty
 import Function
-open import Cubical hiding (isSet)
-open import Cubical.GradLemma using ( propIsEquiv )
+open import Cubical
+open import Cubical.NType.Properties using ( propIsEquiv )
 
 ∃! : ∀ {a b} {A : Set a}
   → (A → Set b) → Set (a ⊔ b)
@@ -23,8 +23,9 @@ open import Cubical.GradLemma using ( propIsEquiv )
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
-IsSet   : {ℓ : Level} (A : Set ℓ) → Set ℓ
-IsSet A = {x y : A} → (p q : x ≡ y) → p ≡ q
+-- 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.
@@ -53,12 +54,13 @@ record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
 -- (univalent).
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
   open RawCategory ℂ
+  module Raw = RawCategory ℂ
   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
-    arrowIsSet : ∀ {A B : Object} → IsSet (Arrow A B)
+    arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
 
   Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
   Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
@@ -91,22 +93,40 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
   -- This lemma will be useful to prove the equality of two categories.
   IsCategory-is-prop : isProp (IsCategory ℂ)
   IsCategory-is-prop x y i = record
-    { assoc = x.arrowIsSet x.assoc y.assoc i
+    -- 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
+      ( x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i
+      , x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i
       )
-    ; arrowIsSet = λ p q →
-      let
-        golden : x.arrowIsSet p q ≡ y.arrowIsSet p q
-        golden = {!!}
-      in
-        golden i
-      ; univalent = λ y₁ → {!!}
+    ; arrowIsSet = isSetIsProp x.arrowIsSet y.arrowIsSet i
+    ; univalent = {!!}
     }
     where
       module x = IsCategory x
       module y = IsCategory y
+      xuni : x.Univalent
+      xuni = x.univalent
+      yuni : y.Univalent
+      yuni = y.univalent
+      open RawCategory ℂ
+      T :  I → Set (ℓa ⊔ ℓb)
+      T i = {A B : Object} →
+        isEquiv (A ≡ B) (A x.≅ B)
+          (λ A≡B →
+            transp
+            (λ j →
+            Σ-syntax (Arrow A (A≡B j))
+            (λ 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
+            )
+          )
+      eqUni : T [ xuni ≡ yuni ]
+      eqUni = {!!}
+
 
 record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   field
diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index 8097071..ff5d659 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical #-}
 module Cat.Category.Functor where
 
 open import Agda.Primitive
@@ -60,14 +61,14 @@ module _
 
   IsFunctorIsProp : isProp (IsFunctor _ _ F)
   IsFunctorIsProp isF0 isF1 i = record
-    { ident = 𝔻.arrowIsSet isF0.ident isF1.ident i
-    ; distrib = 𝔻.arrowIsSet isF0.distrib isF1.distrib i
+    { ident = 𝔻.arrowIsSet _ _ isF0.ident isF1.ident i
+    ; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i
     }
     where
       module isF0 = IsFunctor isF0
       module isF1 = IsFunctor isF1
 
--- Alternate version of above where `F` is a path in 
+-- Alternate version of above where `F` is indexed by an interval
 module _
     {ℓa ℓb : Level}
     {ℂ 𝔻 : Category ℓa ℓb}
@@ -78,14 +79,11 @@ module _
   IsProp' : {ℓ : Level} (A : I → Set ℓ) → Set ℓ
   IsProp' A = (a0 : A i0) (a1 : A i1) → A [ a0 ≡ a1 ]
 
-  postulate IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
-  -- IsFunctorIsProp' isF0 isF1 i = record
-  --   { ident = {!𝔻.arrowIsSet {!isF0.ident!} {!isF1.ident!} i!}
-  --   ; distrib = {!𝔻.arrowIsSet {!isF0.distrib!} {!isF1.distrib!} i!}
-  --   }
-  --   where
-  --     module isF0 = IsFunctor isF0
-  --     module isF1 = IsFunctor isF1
+  IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
+  IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
+    (\ F → IsFunctorIsProp {F = F}) (\ i → F i)
+    where
+      open import Cubical.NType.Properties using (lemPropF)
 
 module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
   Functor≡ : {F G : Functor ℂ 𝔻}
@@ -95,14 +93,13 @@ module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
     → F ≡ G
   Functor≡ {F} {G} eq* eq→ i = record
     { raw = eqR i
-    ; isFunctor = f i
+    ; isFunctor = eqIsF i
     }
     where
       eqR : raw F ≡ raw G
       eqR i = record { func* = eq* i ; func→ = eq→ i }
-      postulate T : isSet (IsFunctor _ _ (raw F))
-      f : (λ i →  IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ]
-      f = IsFunctorIsProp' (isFunctor F) (isFunctor G)
+      eqIsF : (λ i →  IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ]
+      eqIsF = IsFunctorIsProp' (isFunctor F) (isFunctor G)
 
 module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
   private
diff --git a/src/Cat/Equality.agda b/src/Cat/Equality.agda
index bf94143..c3c333d 100644
--- a/src/Cat/Equality.agda
+++ b/src/Cat/Equality.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical #-}
 -- Defines equality-principles for data-types from the standard library.
 
 module Cat.Equality where
@@ -19,3 +20,28 @@ module Equality where
         Σ≡ : a ≡ b
         proj₁ (Σ≡ i) = proj₁≡ i
         proj₂ (Σ≡ i) = proj₂≡ i
+
+        -- Remark 2.7.1: This theorem:
+        --
+        --   (x , u) ≡ (x , v) → u ≡ v
+        --
+        -- does *not* hold! We can only conclude that there *exists* `p : x ≡ x`
+        -- such that
+        --
+        --   p* u ≡ v
+        -- thm : isSet A → (∀ {a} → isSet (B a)) → isSet (Σ A B)
+        -- thm sA sB (x , y) (x' , y') p q = res
+        --   where
+        --     x≡x'0 : x ≡ x'
+        --     x≡x'0 = λ i → proj₁ (p i)
+        --     x≡x'1 : x ≡ x'
+        --     x≡x'1 = λ i → proj₁ (q i)
+        --     someP : x ≡ x'
+        --     someP = {!!}
+        --     tricky : {!y!} ≡ y'
+        --     tricky = {!!}
+        --     -- res' : (λ _ → Σ A B) [ (x , y) ≡ (x' , y') ]
+        --     res' : ({!!} , {!!}) ≡ ({!!} , {!!})
+        --     res' = {!!}
+        --     res : p ≡ q
+        --     res i = {!res'!}
diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda
new file mode 100644
index 0000000..2e56a27
--- /dev/null
+++ b/src/Cat/Wishlist.agda
@@ -0,0 +1,6 @@
+module Cat.Wishlist where
+
+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