diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..051f9ce
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,2 @@
+build: src/**.agda
+	agda src/Cat.agda
diff --git a/src/Cat.agda b/src/Cat.agda
new file mode 100644
index 0000000..6cb8e32
--- /dev/null
+++ b/src/Cat.agda
@@ -0,0 +1,12 @@
+module Cat where
+
+import Cat.Categories.Sets
+import Cat.Categories.Cat
+import Cat.Categories.Rel
+import Cat.Category.Pathy
+import Cat.Category.Bij
+import Cat.Category.Free
+import Cat.Category.Properties
+import Cat.Category
+import Cat.Cubical
+import Cat.Functor
diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 79efc49..796379b 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -1,55 +1,174 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
 
-module Category.Categories.Cat where
+module Cat.Categories.Cat where
 
 open import Agda.Primitive
 open import Cubical
 open import Function
 open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
 
-open import Category
+open import Cat.Category
+open import Cat.Functor
+
+-- Tip from Andrea:
+-- 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
+
+eqpair : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} {a a' : A} {b b' : B}
+  → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
+eqpair eqa eqb i = eqa i , eqb i
+
+open Functor
+open Category
+module _ {ℓ ℓ' : Level} {A B : Category ℓ ℓ'} where
+  lift-eq-functors : {f g : Functor A B}
+    → (eq* : f .func* ≡ g .func*)
+    → (eq→ : PathP (λ i → ∀ {x y} → A .Arrow x y → B .Arrow (eq* i x) (eq* i y))
+    (f .func→) (g .func→))
+    --        → (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 C D : Category ℓ ℓ'} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
+      eq* : func* (h ∘f (g ∘f f)) ≡ func* ((h ∘f g) ∘f f)
+      eq* = refl
+      eq→ : PathP
+        (λ i → {x y : A .Object} → A .Arrow x y → D .Arrow (eq* i x) (eq* i y))
+        (func→ (h ∘f (g ∘f f))) (func→ ((h ∘f g) ∘f f))
+      eq→ = refl
+      id-l = (h ∘f (g ∘f f)) .ident -- = func→ (h ∘f (g ∘f f)) (𝟙 A) ≡ 𝟙 D
+      id-r = ((h ∘f g) ∘f f) .ident -- = func→ ((h ∘f g) ∘f f) (𝟙 A) ≡ 𝟙 D
+      postulate eqI : PathP
+                 (λ i → ∀ {c : A .Object} → eq→ i (A .𝟙 {c}) ≡ D .𝟙 {eq* i c})
+                 (ident ((h ∘f (g ∘f f))))
+                 (ident ((h ∘f g) ∘f f))
+      postulate eqD : PathP (λ i → { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''}
+                        → eq→ i (A ._⊕_ a' a) ≡ D ._⊕_ (eq→ i a') (eq→ i a))
+                        (distrib (h ∘f (g ∘f f))) (distrib ((h ∘f g) ∘f f))
+      -- eqD = {!!}
 
-    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
-        (functor func* func→ idnt distrib)
-        (functor func*₁ func→₁ idnt₁ distrib₁)
-        eq-func* = {!!}
+      assc : h ∘f (g ∘f f) ≡ (h ∘f g) ∘f f
+      assc = lift-eq-functors eq* eq→ eqI eqD
 
-    module _ {A B : Category {ℓ} {ℓ'}} {f : Functor A B} where
-      idHere = identity {ℓ} {ℓ'} {A}
-      lem : (Functor.func* f) ∘ (Functor.func* idHere) ≡ Functor.func* f
+    module _ {A B : Category ℓ ℓ'} {f : Functor A B} where
+      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 ∘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 ∘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 ∘f identity)) (ident f)
+      -- lemz = {!!}
+      postulate ident-r : f ∘f identity ≡ f
+      -- ident-r = lift-eq-functors lem lemmm {!lemz!} {!!}
+      postulate ident-l : identity ∘f f ≡ f
+      -- ident-l = lift-eq-functors lem lemmm {!refl!} {!!}
 
-  CatCat : Category {lsuc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'}
-  CatCat =
+  Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
+  Cat =
     record
-      { Object = Category {ℓ} {ℓ'}
+      { Object = Category ℓ ℓ'
       ; Arrow = Functor
       ; 𝟙 = identity
-      ; _⊕_ = functor-comp
-      ; assoc = {!!}
-      ; ident = ident-r , ident-l
+      ; _⊕_ = _∘f_
+      -- What gives here? Why can I not name the variables directly?
+      ; isCategory = record
+        { assoc = λ {_ _ _ _ f g h} → assc {f = f} {g = g} {h = h}
+        ; ident = ident-r , ident-l
+        }
       }
+
+module _ {ℓ : Level} (C D : Category ℓ ℓ) where
+  private
+    :Object: = C .Object × D .Object
+    :Arrow:  : :Object: → :Object: → Set ℓ
+    :Arrow: (c , d) (c' , d') = Arrow C c c' × Arrow D d d'
+    :𝟙: : {o : :Object:} → :Arrow: o o
+    :𝟙: = C .𝟙 , D .𝟙
+    _:⊕:_ :
+      {a b c : :Object:} →
+      :Arrow: b c →
+      :Arrow: a b →
+      :Arrow: a c
+    _:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → (C ._⊕_) bc∈C ab∈C , D ._⊕_ bc∈D ab∈D}
+
+    instance
+      :isCategory: : IsCategory :Object: :Arrow: :𝟙: _:⊕:_
+      :isCategory: = record
+        { assoc = eqpair C.assoc D.assoc
+        ; ident
+        = eqpair (fst C.ident) (fst D.ident)
+        , eqpair (snd C.ident) (snd D.ident)
+        }
+        where
+          open module C = IsCategory (C .isCategory)
+          open module D = IsCategory (D .isCategory)
+
+    :product: : Category ℓ ℓ
+    :product: = record
+      { Object = :Object:
+      ; Arrow = :Arrow:
+      ; 𝟙 = :𝟙:
+      ; _⊕_ = _:⊕:_
+      }
+
+    proj₁ : Arrow Cat :product: C
+    proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl }
+
+    proj₂ : Arrow Cat :product: D
+    proj₂ = record { func* = snd ; func→ = snd ; ident = refl ; distrib = refl }
+
+    module _ {X : Object (Cat {ℓ} {ℓ})} (x₁ : Arrow Cat X C) (x₂ : Arrow Cat 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 :product:
+      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.
+      postulate isUniqL : (Cat ⊕ proj₁) x ≡ x₁
+      -- isUniqL = lift-eq-functors refl refl {!!} {!!}
+
+      postulate isUniqR : (Cat ⊕ proj₂) x ≡ x₂
+      -- isUniqR = lift-eq-functors refl refl {!!} {!!}
+
+      isUniq : (Cat ⊕ proj₁) x ≡ x₁ × (Cat ⊕ proj₂) x ≡ x₂
+      isUniq = isUniqL , isUniqR
+
+      uniq : ∃![ x ] ((Cat ⊕ proj₁) x ≡ x₁ × (Cat ⊕ proj₂) x ≡ x₂)
+      uniq = x , isUniq
+
+    instance
+      isProduct : IsProduct Cat proj₁ proj₂
+      isProduct = uniq
+
+  product : Product {ℂ = Cat} C D
+  product = record
+    { obj = :product:
+    ; proj₁ = proj₁
+    ; proj₂ = proj₂
+    }
diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index 32e07f4..b398aa9 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -154,12 +154,11 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset
          ≡ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
   is-assoc = equivToPath equi
 
-Rel : Category
+Rel : Category (lsuc lzero) (lsuc lzero)
 Rel = record
   { Object = Set
   ; Arrow = λ S R → Subset (S × R)
   ; 𝟙 = λ {S} → Diag S
   ; _⊕_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
-  ; assoc = funExt is-assoc
-  ; ident = funExt ident-l , funExt ident-r
+  ; isCategory = record { assoc = funExt is-assoc ; ident = funExt ident-l , funExt ident-r }
   }
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index bd026dc..3579b52 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -9,44 +9,45 @@ open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
 
 open import Cat.Category
 open import Cat.Functor
+open Category
 
--- Sets are built-in to Agda. The set of all small sets is called Set.
-
-Fun : {ℓ : Level} → ( T U : Set ℓ ) → Set ℓ
-Fun T U = T → U
-
-Sets : {ℓ : Level} → Category {lsuc ℓ} {ℓ}
+Sets : {ℓ : Level} → Category (lsuc ℓ) ℓ
 Sets {ℓ} = record
   { Object = Set ℓ
-  ; Arrow = λ T U → Fun {ℓ} T U
-  ; 𝟙 = λ x → x
-  ; _⊕_  = λ g f x → g ( f x )
-  ; assoc = refl
-  ; ident = funExt (λ x → refl) , funExt (λ x → refl)
+  ; Arrow = λ T U → T → U
+  ; 𝟙 = id
+  ; _⊕_ = _∘′_
+  ; isCategory = record { assoc = refl ; ident = funExt (λ _ → refl) , funExt (λ _ → refl) }
   }
+  where
+    open import Function
 
-Representable : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → Set (ℓ ⊔ lsuc ℓ')
+-- Covariant Presheaf
+Representable : {ℓ ℓ' : Level} → (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
 Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
 
-representable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Representable ℂ
+-- The "co-yoneda" embedding.
+representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
 representable {ℂ = ℂ} A = record
-  { func* = λ B → ℂ.Arrow A B
-  ; func→ = λ f g → f ℂ.⊕ g
-  ; ident = funExt λ _ → snd ℂ.ident
-  ; distrib = funExt λ x → sym ℂ.assoc
+  { func* = λ B → ℂ .Arrow A B
+  ; func→ = ℂ ._⊕_
+  ; ident = funExt λ _ → snd ident
+  ; distrib = funExt λ x → sym assoc
   }
   where
-    open module ℂ = Category ℂ
+    open IsCategory (ℂ .isCategory)
 
-Presheaf : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → Set (ℓ ⊔ lsuc ℓ')
+-- Contravariant Presheaf
+Presheaf : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
 Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
 
-presheaf : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object (Opposite ℂ) → Presheaf ℂ
+-- Alternate name: `yoneda`
+presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ
 presheaf {ℂ = ℂ} B = record
-  { func* = λ A → ℂ.Arrow A B
-  ; func→ = λ f g → g ℂ.⊕ f
-  ; ident = funExt λ x → fst ℂ.ident
-  ; distrib = funExt λ x → ℂ.assoc
+  { func* = λ A → ℂ .Arrow A B
+  ; func→ = λ f g → ℂ ._⊕_ g f
+  ; ident = funExt λ x → fst ident
+  ; distrib = funExt λ x → assoc
   }
   where
-    open module ℂ = Category ℂ
+    open IsCategory (ℂ .isCategory)
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index a30aee4..91e25f3 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -4,139 +4,119 @@ 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
 
-postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
+∃! : ∀ {a b} {A : Set a}
+  → (A → Set b) → Set (a ⊔ b)
+∃! = ∃!≈ _≡_
 
-record Category {ℓ ℓ'} : Set (lsuc (ℓ' ⊔ ℓ)) where
-  constructor category
+∃!-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
+∃!-syntax = ∃
+
+syntax ∃!-syntax (λ x → B) = ∃![ x ] B
+
+record IsCategory {ℓ ℓ' : Level}
+  (Object : Set ℓ)
+  (Arrow  : Object → Object → Set ℓ')
+  (𝟙      : {o : Object} → Arrow o o)
+  (_⊕_    : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c)
+  : Set (lsuc (ℓ' ⊔ ℓ)) where
+  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
+
+-- open IsCategory public
+
+record Category (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
+  -- adding no-eta-equality can speed up type-checking.
+  no-eta-equality
   field
     Object : Set ℓ
     Arrow  : Object → Object → Set ℓ'
     𝟙      : {o : Object} → Arrow o o
     _⊕_    : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c
-    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
+    {{isCategory}} : IsCategory Object Arrow 𝟙 _⊕_
   infixl 45 _⊕_
   domain : { a b : Object } → Arrow a b → Object
   domain {a = a} _ = a
   codomain : { a b : Object } → Arrow a b → Object
   codomain {b = b} _ = b
 
-open Category public
+open Category
 
-module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } where
-  private
-    open module ℂ = Category ℂ
-    _+_ = ℂ._⊕_
+module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where
+  module _ { A B : ℂ .Object } where
+    Isomorphism : (f : ℂ .Arrow A B) → Set ℓ'
+    Isomorphism f = Σ[ g ∈ ℂ .Arrow B A ] ℂ ._⊕_ g f ≡ ℂ .𝟙 × ℂ ._⊕_ f g ≡ ℂ .𝟙
 
-  Isomorphism : (f : ℂ.Arrow A B) → Set ℓ'
-  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₁
 
-  Epimorphism : {X : ℂ.Object } → (f : ℂ.Arrow A B) → Set ℓ'
-  Epimorphism {X} f = ( g₀ g₁ : ℂ.Arrow B X ) → g₀ + f ≡ g₁ + f → g₀ ≡ g₁
+    Monomorphism : {X : ℂ .Object} → (f : ℂ .Arrow A B) → Set ℓ'
+    Monomorphism {X} f = ( g₀ g₁ : ℂ .Arrow X A ) → ℂ ._⊕_ f g₀ ≡ ℂ ._⊕_ f g₁ → g₀ ≡ g₁
 
-  Monomorphism : {X : ℂ.Object} → (f : ℂ.Arrow A B) → Set ℓ'
-  Monomorphism {X} f = ( g₀ g₁ : ℂ.Arrow X A ) → f + g₀ ≡ f + g₁ → g₀ ≡ g₁
+  -- Isomorphism of objects
+  _≅_ : (A B : Object ℂ) → Set ℓ'
+  _≅_ A B = Σ[ f ∈ ℂ .Arrow A B ] (Isomorphism f)
 
-  iso-is-epi : ∀ {X} (f : ℂ.Arrow A B) → Isomorphism f → Epimorphism {X = X} f
-  -- Idea: Pre-compose with f- on both sides of the equality of eq to get
-  -- g₀ + f + f- ≡ g₁ + f + f-
-  -- which by left-inv reduces to the goal.
-  iso-is-epi f (f- , left-inv , right-inv) g₀ g₁ eq =
-     trans (sym (fst ℂ.ident))
-       ( trans (cong (_+_ g₀) (sym right-inv))
-         ( trans ℂ.assoc
-           ( trans (cong (λ x → x + f-) eq)
-             ( trans (sym ℂ.assoc)
-               ( trans (cong (_+_ g₁) right-inv) (fst ℂ.ident))
-             )
-           )
-         )
-       )
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} where
+  IsProduct : (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
+  IsProduct π₁ π₂
+    = ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B)
+    → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ ._⊕_ π₂ x ≡ x₂)
 
-  iso-is-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Monomorphism {X = X} f
-  -- For the next goal we do something similar: Post-compose with f- and use
-  -- right-inv to get the goal.
-  iso-is-mono f (f- , (left-inv , right-inv)) g₀ g₁ eq =
-    trans (sym (snd ℂ.ident))
-      ( trans (cong (λ x → x + g₀) (sym left-inv))
-        ( trans (sym ℂ.assoc)
-          ( trans (cong (_+_ f-) eq)
-            ( trans ℂ.assoc
-              ( trans (cong (λ x → x + g₁) left-inv) (snd ℂ.ident)
-              )
-            )
-          )
-        )
-      )
+-- Tip from Andrea; Consider this style for efficiency:
+-- record IsProduct {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'})
+--   {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) : Set (ℓ ⊔ ℓ') where
+--   field
+--      isProduct : ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B)
+--        → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ. _⊕_ π₂ x ≡ x₂)
 
-  iso-is-epi-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
-  iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso
+record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : ℂ .Object) : Set (ℓ ⊔ ℓ') where
+  no-eta-equality
+  field
+    obj : ℂ .Object
+    proj₁ : ℂ .Arrow obj A
+    proj₂ : ℂ .Arrow obj B
+    {{isProduct}} : IsProduct ℂ proj₁ proj₂
 
-{-
-epi-mono-is-not-iso : ∀ {ℓ ℓ'} → ¬ ((ℂ : Category {ℓ} {ℓ'}) {A B X : Object ℂ} (f : Arrow ℂ A B ) → Epimorphism {ℂ = ℂ} {X = X} f → Monomorphism {ℂ = ℂ} {X = X} f → Isomorphism {ℂ = ℂ} f)
-epi-mono-is-not-iso f =
-  let k = f {!!} {!!} {!!} {!!}
-  in {!!}
--}
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
+  Opposite : Category ℓ ℓ'
+  Opposite =
+    record
+      { Object = ℂ .Object
+      ; Arrow = flip (ℂ .Arrow)
+      ; 𝟙 = ℂ .𝟙
+      ; _⊕_ = flip (ℂ ._⊕_)
+      ; isCategory = record { assoc = sym assoc ; ident = swap ident }
+      }
+      where
+        open IsCategory (ℂ .isCategory)
 
--- Isomorphism of objects
-_≅_ : { ℓ ℓ' : Level } → { ℂ : Category {ℓ} {ℓ'} } → ( A B : Object ℂ ) → Set ℓ'
-_≅_ {ℂ = ℂ} A B = Σ[ f ∈ ℂ.Arrow A B ] (Isomorphism {ℂ = ℂ} f)
-  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) = {!!}
 
-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
-    }
-  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)}))
-
-Opposite : ∀ {ℓ ℓ'} → Category {ℓ} {ℓ'} → Category {ℓ} {ℓ'}
-Opposite ℂ =
-  record
-    { Object = ℂ.Object
-    ; Arrow = λ A B → ℂ.Arrow B A
-    ; 𝟙 = ℂ.𝟙
-    ; _⊕_ = λ g f → f ℂ.⊕ g
-    ; assoc = sym ℂ.assoc
-    ; ident = swap ℂ.ident
-    }
-  where
-    open module ℂ = Category ℂ
-
-Hom : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → (A B : Object ℂ) → Set ℓ'
+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')
+module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where
+  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 217c329..0892f55 100644
--- a/src/Cat/Category/Bij.agda
+++ b/src/Cat/Category/Bij.agda
@@ -1,6 +1,9 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
+
+module Cat.Category.Bij where
 
 open import Cubical.PathPrelude hiding ( Id )
+open import Cubical.FromStdLib
 
 module _ {A : Set} {a : A} {P : A → Set} where
   Q : A → Set
@@ -20,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 = refl
+  vw-bij a = {!!}
   -- tubij a with (t ∘ u) a
   -- ... | q = {!!}
 
diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda
index c67f25a..ff06743 100644
--- a/src/Cat/Category/Free.agda
+++ b/src/Cat/Category/Free.agda
@@ -1,21 +1,20 @@
-module Category.Free where
+module Cat.Category.Free where
 
 open import Agda.Primitive
 open import Cubical.PathPrelude hiding (Path)
+open import Data.Product
 
-open import Category as C
+open import Cat.Category as C
 
-module _ {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'}) where
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   private
     open module ℂ = Category ℂ
     Obj = ℂ.Object
 
-  Path : ( a b : Obj ) → Set
-  Path a b = undefined
-
-  postulate emptyPath : (o : Obj) → Path o o
-
-  postulate concatenate : {a b c : Obj} → Path b c → Path a b → Path a c
+  postulate
+    Path : ( a b : Obj ) → Set ℓ'
+    emptyPath : (o : Obj) → Path o o
+    concatenate : {a b c : Obj} → Path b c → Path a b → Path a c
 
   private
     module _ {A B C D : Obj} {r : Path A B} {q : Path B C} {p : Path C D} where
@@ -27,12 +26,11 @@ module _ {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'}) where
         ident-r : concatenate {A} {A} {B} p (emptyPath A) ≡ p
         ident-l : concatenate {A} {B} {B} (emptyPath B) p ≡ p
 
-  Free : Category
+  Free : Category ℓ ℓ'
   Free = record
     { Object = Obj
     ; Arrow = Path
     ; 𝟙 = λ {o} → emptyPath o
     ; _⊕_ = λ {a b c} → concatenate {a} {b} {c}
-    ; assoc = p-assoc
-    ; ident = ident-r , ident-l
+    ; isCategory = record { assoc = p-assoc ; ident = ident-r , ident-l }
     }
diff --git a/src/Cat/Category/Pathy.agda b/src/Cat/Category/Pathy.agda
index 7738726..e33a2ca 100644
--- a/src/Cat/Category/Pathy.agda
+++ b/src/Cat/Category/Pathy.agda
@@ -1,7 +1,8 @@
 {-# OPTIONS --cubical #-}
 
-module Category.Pathy where
+module Cat.Category.Pathy where
 
+open import Level
 open import Cubical.PathPrelude
 
 {-
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index d8bd40c..4ff4376 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -2,22 +2,64 @@
 
 module Cat.Category.Properties where
 
+open import Agda.Primitive
+open import Data.Product
+open import Cubical.PathPrelude
+
 open import Cat.Category
 open import Cat.Functor
 open import Cat.Categories.Sets
 
+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
+    g₀              ≡⟨ sym (proj₁ ident) ⟩
+    g₀ ⊕ 𝟙          ≡⟨ cong (_⊕_ g₀) (sym right-inv) ⟩
+    g₀ ⊕ (f ⊕ f-)   ≡⟨ assoc ⟩
+    (g₀ ⊕ f) ⊕ f-   ≡⟨ cong (λ φ → φ ⊕ f-) eq ⟩
+    (g₁ ⊕ f) ⊕ f-   ≡⟨ sym assoc ⟩
+    g₁ ⊕ (f ⊕ f-)   ≡⟨ cong (_⊕_ g₁) right-inv ⟩
+    g₁ ⊕ 𝟙          ≡⟨ proj₁ ident ⟩
+    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₂ ident) ⟩
+    𝟙 ⊕ g₀        ≡⟨ cong (λ φ → φ ⊕ g₀) (sym left-inv) ⟩
+    (f- ⊕ f) ⊕ g₀ ≡⟨ sym assoc ⟩
+    f- ⊕ (f ⊕ g₀) ≡⟨ cong (_⊕_ f-) eq ⟩
+    f- ⊕ (f ⊕ g₁) ≡⟨ assoc ⟩
+    (f- ⊕ f) ⊕ g₁ ≡⟨ cong (λ φ → φ ⊕ g₁) left-inv ⟩
+    𝟙 ⊕ g₁        ≡⟨ proj₂ ident ⟩
+    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
+
+{-
+epi-mono-is-not-iso : ∀ {ℓ ℓ'} → ¬ ((ℂ : Category {ℓ} {ℓ'}) {A B X : Object ℂ} (f : Arrow ℂ A B ) → Epimorphism {ℂ = ℂ} {X = X} f → Monomorphism {ℂ = ℂ} {X = X} f → Isomorphism {ℂ = ℂ} f)
+epi-mono-is-not-iso f =
+  let k = f {!!} {!!} {!!} {!!}
+  in {!!}
+-}
+
+
 module _ {ℓa ℓa' ℓb ℓb'} where
-  Exponential : Category {ℓa} {ℓa'} → Category {ℓb} {ℓb'} → Category {{!!}} {{!!}}
+  Exponential : Category ℓa ℓa' → Category ℓb ℓb' → Category {!!} {!!}
   Exponential A B = record
     { Object = {!!}
     ; Arrow = {!!}
     ; 𝟙 = {!!}
     ; _⊕_ = {!!}
-    ; assoc = {!!}
-    ; ident = {!!}
+    ; isCategory = {!!}
     }
 
 _⇑_ = Exponential
 
-yoneda : ∀ {ℓ ℓ'} → {ℂ : Category {ℓ} {ℓ'}} → Functor ℂ (Sets ⇑ (Opposite ℂ))
+yoneda : ∀ {ℓ ℓ'} → {ℂ : Category ℓ ℓ'} → Functor ℂ (Sets ⇑ (Opposite ℂ))
 yoneda = {!!}
diff --git a/src/Cat/Cubical.agda b/src/Cat/Cubical.agda
index cba1c41..b10afba 100644
--- a/src/Cat/Cubical.agda
+++ b/src/Cat/Cubical.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Cubical where
 
 open import Agda.Primitive
@@ -9,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 ℓ
@@ -36,13 +42,12 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
     Mor = Σ themap rules
 
   -- The category of names and substitutions
-  ℂ : Category -- {ℓo} {lsuc lzero ⊔ ℓo}
+  ℂ : Category ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
   ℂ = record
     -- { Object = FiniteDecidableSubset
     { Object = Ns → Bool
     ; Arrow = Mor
     ; 𝟙 = {!!}
     ; _⊕_ = {!!}
-    ; assoc = {!!}
-    ; ident = {!!}
+    ; isCategory = ?
     }
diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda
index 4daaef3..5965f72 100644
--- a/src/Cat/Functor.agda
+++ b/src/Cat/Functor.agda
@@ -6,7 +6,7 @@ open import Function
 
 open import Cat.Category
 
-record Functor {ℓc ℓc' ℓd ℓd'} (C : Category {ℓc} {ℓc'}) (D : Category {ℓd} {ℓd'})
+record Functor {ℓc ℓc' ℓd ℓd'} (C : Category ℓc ℓc') (D : Category ℓd ℓd')
   : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
   private
     open module C = Category C
@@ -21,43 +21,41 @@ record Functor {ℓc ℓc' ℓd ℓd'} (C : Category {ℓc} {ℓc'}) (D : Catego
     distrib : { c c' c'' : C.Object} {a : C.Arrow c c'} {a' : C.Arrow c' c''}
       → func→ (a' C.⊕ a) ≡ func→ a' D.⊕ func→ a
 
-module _ {ℓ ℓ' : Level} {A B C : Category {ℓ} {ℓ'}} (F : Functor B C) (G : Functor A B) where
+module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
+  open Functor
+  open Category
   private
-    open module F = Functor F
-    open module G = Functor G
-    open module A = Category A
-    open module B = Category B
-    open module C = Category C
+    F* = F .func*
+    F→ = F .func→
+    G* = G .func*
+    G→ = G .func→
+    _A⊕_ = A ._⊕_
+    _B⊕_ = B ._⊕_
+    _C⊕_ = C ._⊕_
+    module _ {a0 a1 a2 : A .Object} {α0 : A .Arrow a0 a1} {α1 : A .Arrow a1 a2} where
 
-    F* = F.func*
-    F→ = F.func→
-    G* = G.func*
-    G→ = G.func→
-    module _ {a0 a1 a2 : A.Object} {α0 : A.Arrow a0 a1} {α1 : A.Arrow a1 a2} where
-
-      dist : (F→ ∘ G→) (α1 A.⊕ α0) ≡ (F→ ∘ G→) α1 C.⊕ (F→ ∘ G→) α0
+      dist : (F→ ∘ G→) (α1 A⊕ α0) ≡ (F→ ∘ G→) α1 C⊕ (F→ ∘ G→) α0
       dist = begin
-        (F→ ∘ G→) (α1 A.⊕ α0)         ≡⟨ refl ⟩
-        F→ (G→ (α1 A.⊕ α0))           ≡⟨ cong F→ G.distrib ⟩
-        F→ ((G→ α1) B.⊕ (G→ α0))      ≡⟨ F.distrib ⟩
-        (F→ ∘ G→) α1 C.⊕ (F→ ∘ G→) α0 ∎
+        (F→ ∘ G→) (α1 A⊕ α0)         ≡⟨ refl ⟩
+        F→ (G→ (α1 A⊕ α0))           ≡⟨ cong F→ (G .distrib)⟩
+        F→ ((G→ α1) B⊕ (G→ α0))      ≡⟨ F .distrib ⟩
+        (F→ ∘ G→) α1 C⊕ (F→ ∘ G→) α0 ∎
 
-  functor-comp : Functor A C
-  functor-comp =
+  _∘f_ : Functor A C
+  _∘f_ =
     record
       { func* = F* ∘ G*
       ; func→ = F→ ∘ G→
       ; ident = begin
-        (F→ ∘ G→) (A.𝟙) ≡⟨ refl ⟩
-        F→ (G→ (A.𝟙))   ≡⟨ cong F→ G.ident ⟩
-        F→ (B.𝟙)        ≡⟨ F.ident ⟩
-        C.𝟙             ∎
+        (F→ ∘ G→) (A .𝟙) ≡⟨ refl ⟩
+        F→ (G→ (A .𝟙))   ≡⟨ cong F→ (G .ident)⟩
+        F→ (B .𝟙)        ≡⟨ F .ident ⟩
+        C .𝟙             ∎
       ; distrib = dist
       }
 
 -- The identity functor
-identity : {ℓ ℓ' : Level} → {C : Category {ℓ} {ℓ'}} → Functor C C
--- Identity = record { F* = λ x → x ; F→ = λ x → x ; ident = refl ; distrib = refl }
+identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C
 identity = record
   { func* = λ x → x
   ; func→ = λ x → x