diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 1133eee..79aeb58 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -10,36 +10,57 @@ open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
 open import Cat.Category
 open import Cat.Functor
 
+-- Use co-patterns - they help with showing more understandable types in goals.
+lift-eq : ∀ {ℓ} {A B : Set ℓ} {a a' : A} {b b' : B} → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
+fst (lift-eq a b i) = a i
+snd (lift-eq a b i) = b i
+--lift-eq a b = λ i → a i , b i
+
+
+
+open Functor
+open Category
+module _ {ℓ ℓ' : Level} {A B : Category {ℓ} {ℓ'}} where
+  lift-eq-functors : {f g : Functor A B}
+    → (eq* : Functor.func* f ≡ Functor.func* g)
+    → (eq→ : PathP (λ i → ∀ {x y} → Arrow A x y → Arrow B (eq* i x) (eq* i y))
+    (func→ f) (func→ g))
+    --        → (eq→ : Functor.func→ f ≡ {!!}) -- Functor.func→ g)
+    -- Use PathP
+    -- directly to show heterogeneous equalities by using previous
+    -- equalities (i.e. continuous paths) to create new continuous paths.
+    → (eqI : PathP (λ i → ∀ {c : A .Object} → eq→ i (A .𝟙 {c}) ≡ B .𝟙 {eq* i c})
+    (ident f) (ident g))
+    → (eqD : PathP (λ i → { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''}
+    → eq→ i (A ._⊕_ a' a) ≡ B ._⊕_ (eq→ i a') (eq→ i a))
+    (distrib f) (distrib g))
+    → f ≡ g
+  lift-eq-functors eq* eq→ eqI eqD i = record { func* = eq* i ; func→ = eq→ i ; ident = eqI i ; distrib = eqD i }
+
 -- The category of categories
 module _ {ℓ ℓ' : Level} where
   private
     _⊛_ = functor-comp
     module _ {A B C D : Category {ℓ} {ℓ'}} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
-      assc : h ⊛ (g ⊛ f) ≡ (h ⊛ g) ⊛ f
-      assc = {!!}
-
-    module _ {A B : Category {ℓ} {ℓ'}} where
-      lift-eq : (f g : Functor A B)
-        → (eq* : Functor.func* f ≡ Functor.func* g)
-        -- TODO: Must transport here using the equality from above.
-        -- Reason:
-        --   func→  : Arrow A dom cod → Arrow B (func* dom) (func* cod)
-        --   func→₁ : Arrow A dom cod → Arrow B (func*₁ dom) (func*₁ cod)
-        -- In other words, func→ and func→₁ does not have the same type.
-  --      → Functor.func→ f ≡ Functor.func→ g
-  --      → Functor.ident f ≡ Functor.ident g
-  --       → Functor.distrib f ≡ Functor.distrib g
-        → f ≡ g
-      lift-eq f g eq* x = {!!}
+      postulate assc : h ⊛ (g ⊛ f) ≡ (h ⊛ g) ⊛ f
+      -- assc = lift-eq-functors refl refl {!refl!} λ i j → {!!}
 
     module _ {A B : Category {ℓ} {ℓ'}} {f : Functor A B} where
-      idHere = identity {ℓ} {ℓ'} {A}
-      lem : (Functor.func* f) ∘ (Functor.func* idHere) ≡ Functor.func* f
+      lem : (func* f) ∘ (func* (identity {C = A})) ≡ func* f
       lem = refl
-      ident-r : f ⊛ identity ≡ f
-      ident-r = lift-eq (f ⊛ identity) f refl
-      ident-l : identity ⊛ f ≡ f
-      ident-l = {!!}
+      -- lemmm : func→ {C = A} {D = B} (f ⊛ identity) ≡ func→ f
+      lemmm : PathP
+        (λ i →
+        {x y : Object A} → Arrow A x y → Arrow B (func* f x) (func* f y))
+        (func→ (f ⊛ identity)) (func→ f)
+      lemmm = refl
+      postulate lemz : PathP (λ i → {c : A .Object} → PathP (λ _ → Arrow B (func* f c) (func* f c)) (func→ f (A .𝟙)) (B .𝟙))
+                  (ident (f ⊛ identity)) (ident f)
+      -- lemz = {!!}
+      postulate ident-r : f ⊛ identity ≡ f
+      -- ident-r = lift-eq-functors lem lemmm {!lemz!} {!!}
+      postulate ident-l : identity ⊛ f ≡ f
+      -- ident-l = lift-eq-functors lem lemmm {!refl!} {!!}
 
   CatCat : Category {lsuc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'}
   CatCat =
@@ -48,6 +69,54 @@ module _ {ℓ ℓ' : Level} where
       ; Arrow = Functor
       ; 𝟙 = identity
       ; _⊕_ = functor-comp
-      ; assoc = {!!}
+      -- What gives here? Why can I not name the variables directly?
+      ; assoc = λ {_ _ _ _ f g h} → assc {f = f} {g = g} {h = h}
       ; ident = ident-r , ident-l
       }
+
+module _  {ℓ : Level} (C D : Category {ℓ} {ℓ}) where
+  private
+    proj₁ : Arrow CatCat (catProduct C D) C
+    proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl }
+
+    proj₂ : Arrow CatCat (catProduct C D) D
+    proj₂ = record { func* = snd ; func→ = snd ; ident = refl ; distrib = refl }
+
+    module _ {X : Object (CatCat {ℓ} {ℓ})} (x₁ : Arrow CatCat X C) (x₂ : Arrow CatCat X D) where
+      open Functor
+
+      -- ident' : {c : Object X} → ((func→ x₁) {dom = c} (𝟙 X) , (func→ x₂) {dom = c} (𝟙 X)) ≡ 𝟙 (catProduct C D)
+      -- ident' {c = c} = lift-eq (ident x₁) (ident x₂)
+
+      x : Functor X (catProduct C D)
+      x = record
+        { func* = λ x → (func* x₁) x , (func* x₂) x
+        ; func→ = λ x → func→ x₁ x , func→ x₂ x
+        ; ident = lift-eq (ident x₁) (ident x₂)
+        ; distrib = lift-eq (distrib x₁) (distrib x₂)
+        }
+
+      -- Need to "lift equality of functors"
+      -- If I want to do this like I do it for pairs it's gonna be a pain.
+      isUniqL : (CatCat ⊕ proj₁) x ≡ x₁
+      isUniqL = lift-eq-functors refl refl {!!} {!!}
+
+      isUniqR : (CatCat ⊕ proj₂) x ≡ x₂
+      isUniqR = lift-eq-functors refl refl {!!} {!!}
+
+      isUniq : (CatCat ⊕ proj₁) x ≡ x₁ × (CatCat ⊕ proj₂) x ≡ x₂
+      isUniq = isUniqL , isUniqR
+
+      uniq : ∃![ x ] ((CatCat ⊕ proj₁) x ≡ x₁ × (CatCat ⊕ proj₂) x ≡ x₂)
+      uniq = x , isUniq
+
+    instance
+      isProduct : IsProduct CatCat proj₁ proj₂
+      isProduct = uniq
+
+  product : Product {ℂ = CatCat} C D
+  product = record
+    { obj = catProduct C D
+    ; proj₁ = proj₁
+    ; proj₂ = proj₂
+    }
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index bd026dc..62c463e 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -25,9 +25,11 @@ Sets {ℓ} = record
   ; ident = funExt (λ x → refl) , funExt (λ x → refl)
   }
 
+-- Covariant Presheaf
 Representable : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → Set (ℓ ⊔ lsuc ℓ')
 Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
 
+-- The "co-yoneda" embedding.
 representable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Representable ℂ
 representable {ℂ = ℂ} A = record
   { func* = λ B → ℂ.Arrow A B
@@ -38,9 +40,11 @@ representable {ℂ = ℂ} A = record
   where
     open module ℂ = Category ℂ
 
+-- Contravariant Presheaf
 Presheaf : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → Set (ℓ ⊔ lsuc ℓ')
 Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
 
+-- Alternate name: `yoneda`
 presheaf : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object (Opposite ℂ) → Presheaf ℂ
 presheaf {ℂ = ℂ} B = record
   { func* = λ A → ℂ.Arrow A B
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index a30aee4..7d84df8 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -4,15 +4,29 @@ module Cat.Category where
 
 open import Agda.Primitive
 open import Data.Unit.Base
-open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
+open import Data.Product renaming
+  ( proj₁ to fst
+  ; proj₂ to snd
+  ; ∃! to ∃!≈
+  )
 open import Data.Empty
 open import Function
 open import Cubical
 
+∃! : ∀ {a b} {A : Set a}
+  → (A → Set b) → Set (a ⊔ b)
+∃! = ∃!≈ _≡_
+
+∃!-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
+∃!-syntax = ∃
+
+syntax ∃!-syntax (λ x → B) = ∃![ x ] B
+
 postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
 
 record Category {ℓ ℓ'} : Set (lsuc (ℓ' ⊔ ℓ)) where
-  constructor category
+  -- adding no-eta-equality can speed up type-checking.
+  no-eta-equality
   field
     Object : Set ℓ
     Arrow  : Object → Object → Set ℓ'
@@ -36,7 +50,7 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } w
     _+_ = ℂ._⊕_
 
   Isomorphism : (f : ℂ.Arrow A B) → Set ℓ'
-  Isomorphism f = Σ[ g ∈ ℂ.Arrow B A ] g + f ≡ ℂ.𝟙 × f + g ≡ ℂ.𝟙
+  Isomorphism f = Σ[ g ∈ ℂ.Arrow B A ] g ℂ.⊕ f ≡ ℂ.𝟙 × f + g ≡ ℂ.𝟙
 
   Epimorphism : {X : ℂ.Object } → (f : ℂ.Arrow A B) → Set ℓ'
   Epimorphism {X} f = ( g₀ g₁ : ℂ.Arrow B X ) → g₀ + f ≡ g₁ + f → g₀ ≡ g₁
@@ -92,28 +106,55 @@ _≅_ {ℂ = ℂ} A B = Σ[ f ∈ ℂ.Arrow A B ] (Isomorphism {ℂ = ℂ} f)
   where
     open module ℂ = Category ℂ
 
-Product : {ℓ : Level} → ( C D : Category {ℓ} {ℓ} ) → Category {ℓ} {ℓ}
-Product C D =
-  record
-    { Object = C.Object × D.Object
-    ; Arrow = λ { (c , d) (c' , d') →
-      let carr = C.Arrow c c'
-          darr = D.Arrow d d'
-      in carr × darr}
-    ; 𝟙 = C.𝟙 , D.𝟙
-    ; _⊕_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → bc∈C C.⊕ ab∈C , bc∈D D.⊕ ab∈D}
-    ; assoc = eqpair C.assoc D.assoc
-    ; ident =
-      let (Cl , Cr) = C.ident
-          (Dl , Dr) = D.ident
-      in eqpair Cl Dl , eqpair Cr Dr
-    }
+IsProduct : ∀ {ℓ ℓ'} (ℂ : Category {ℓ} {ℓ'}) {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
+IsProduct ℂ {A = A} {B = B} π₁ π₂
+  = ∀ {X : ℂ.Object} (x₁ : ℂ.Arrow X A) (x₂ : ℂ.Arrow X B)
+  → ∃![ x ] (π₁ ℂ.⊕ x ≡ x₁ × π₂ ℂ.⊕ x ≡ x₂)
   where
-    open module C = Category C
-    open module D = Category D
-    -- Two pairs are equal if their components are equal.
-    eqpair : {ℓ : Level} → { A : Set ℓ } → { B : Set ℓ } → { a a' : A } → { b b' : B } → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
-    eqpair {a = a} {b = b} eqa eqb = subst eqa (subst eqb (refl {x = (a , b)}))
+    open module ℂ = Category ℂ
+
+-- Consider this style for efficiency:
+-- record R : Set where
+--   field
+--     isP : IsProduct {!!} {!!} {!!}
+
+record Product {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} (A B : Category.Object ℂ) : Set (ℓ ⊔ ℓ') where
+  no-eta-equality
+  field
+    obj : Category.Object ℂ
+    proj₁ : Category.Arrow ℂ obj A
+    proj₂ : Category.Arrow ℂ obj B
+    {{isProduct}} : IsProduct ℂ proj₁ proj₂
+
+mutual
+  catProduct : {ℓ : Level} → ( C D : Category {ℓ} {ℓ} ) → Category {ℓ} {ℓ}
+  catProduct C D =
+    record
+      { Object = C.Object × D.Object
+      -- Why does "outlining   with `arrowProduct` not work?
+      ; Arrow = λ {(c , d) (c' , d') → Arrow C c c' × Arrow D d d'}
+      ; 𝟙 = C.𝟙 , D.𝟙
+      ; _⊕_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → bc∈C C.⊕ ab∈C , bc∈D D.⊕ ab∈D}
+      ; assoc = eqpair C.assoc D.assoc
+      ; ident =
+        let (Cl , Cr) = C.ident
+            (Dl , Dr) = D.ident
+        in eqpair Cl Dl , eqpair Cr Dr
+      }
+    where
+      open module C = Category C
+      open module D = Category D
+      -- Two pairs are equal if their components are equal.
+      eqpair : {ℓ : Level} → { A : Set ℓ } → { B : Set ℓ } → { a a' : A } → { b b' : B } → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
+      eqpair {a = a} {b = b} eqa eqb = subst eqa (subst eqb (refl {x = (a , b)}))
+
+
+  -- arrowProduct : ∀ {ℓ} {C D : Category {ℓ} {ℓ}} → (Object C) × (Object D) → (Object C) × (Object D) → Set ℓ
+  -- arrowProduct = {!!}
+
+  -- Arrows in the product-category
+  arrowProduct : ∀ {ℓ} {C D : Category {ℓ} {ℓ}} (c d : Object (catProduct C D)) → Set ℓ
+  arrowProduct {C = C} {D = D} (c , d) (c' , d') = Arrow C c c' × Arrow D d d'
 
 Opposite : ∀ {ℓ ℓ'} → Category {ℓ} {ℓ'} → Category {ℓ} {ℓ'}
 Opposite ℂ =
@@ -128,15 +169,21 @@ Opposite ℂ =
   where
     open module ℂ = Category ℂ
 
+-- A consequence of no-eta-equality; `Opposite-is-involution` is no longer
+-- definitional - i.e.; you must match on the fields:
+--
+-- Opposite-is-involution : ∀ {ℓ ℓ'} → {C : Category {ℓ} {ℓ'}} → Opposite (Opposite C) ≡ C
+-- Object (Opposite-is-involution {C = C} i) = Object C
+-- Arrow (Opposite-is-involution i) = {!!}
+-- 𝟙 (Opposite-is-involution i) = {!!}
+-- _⊕_ (Opposite-is-involution i) = {!!}
+-- assoc (Opposite-is-involution i) = {!!}
+-- ident (Opposite-is-involution i) = {!!}
+
 Hom : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → (A B : Object ℂ) → Set ℓ'
 Hom ℂ A B = Arrow ℂ A B
 
 module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} where
-  private
-    Obj = Object ℂ
-    Arr = Arrow ℂ
-    _+_ = _⊕_ ℂ
-
-  HomFromArrow : (A : Obj) → {B B' : Obj} → (g : Arr B B')
+  HomFromArrow : (A : ℂ .Object) → {B B' : ℂ .Object} → (g : ℂ .Arrow B B')
     → Hom ℂ A B → Hom ℂ A B'
-  HomFromArrow _A g = λ f → g + f
+  HomFromArrow _A = _⊕_ ℂ
diff --git a/src/Cat/Category/Bij.agda b/src/Cat/Category/Bij.agda
index 0d55500..0892f55 100644
--- a/src/Cat/Category/Bij.agda
+++ b/src/Cat/Category/Bij.agda
@@ -23,7 +23,7 @@ module _ {A : Set} {a : A} {P : A → Set} where
   w x = {!!}
 
   vw-bij : (a : P a) → (w ∘ v) a ≡ a
-  vw-bij a = ?
+  vw-bij a = {!!}
   -- tubij a with (t ∘ u) a
   -- ... | q = {!!}
 
diff --git a/src/Cat/Cubical.agda b/src/Cat/Cubical.agda
index f5abda3..92f3d12 100644
--- a/src/Cat/Cubical.agda
+++ b/src/Cat/Cubical.agda
@@ -10,8 +10,13 @@ open import Data.Empty
 
 open import Cat.Category
 
+-- See chapter 1 for a discussion on how presheaf categories are CwF's.
+
+-- See section 6.8 in Huber's thesis for details on how to implement the
+-- categorical version of CTT
+
 module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
-  -- Σ is the "namespace"
+  -- Ns is the "namespace"
   ℓo = (lsuc lzero ⊔ ℓ)
 
   FiniteDecidableSubset : Set ℓ