Merge branch 'dev'

2018-02-05 11:51:13 +01:00 · 2018-02-05 11:51:13 +01:00 · 36d10b0556
parent f13b98b009 22a9a71870
commit 36d10b0556
19 changed files with 786 additions and 441 deletions
--- a/cat.agda-lib
+++ b/cat.agda-lib
@ -7,3 +7,6 @@ depend:
  cubical
 include:
  src
+-- libraries:
+--   libs/agda-stdlib
+--   libs/cubical
--- a/libs/agda-stdlib
+++ b/libs/agda-stdlib
@ -1 +1 @@
-Subproject commit de23244a73d6dab55715fd5a107a5de805c55764
+Subproject commit b5bfbc3c170b0bd0c9aaac1b4d4b3f9b06832bf6
--- a/libs/cubical
+++ b/libs/cubical
@ -1 +1 @@
-Subproject commit a83f5f4c63e5dfd8143ac03163868c63a56802de
+Subproject commit 1d6730c4999daa2b04e9dd39faa0791d0b5c3b48
--- a/proposal/Makefile
+++ b/proposal/Makefile
@ -0,0 +1,46 @@
+# Latex Makefile using latexmk
+# Modified by Dogukan Cagatay <dcagatay@gmail.com>
+# Originally from : http://tex.stackexchange.com/a/40759
+#
+# Change only the variable below to the name of the main tex file.
+PROJNAME=proposal
+
+# You want latexmk to *always* run, because make does not have all the info.
+# Also, include non-file targets in .PHONY so they are run regardless of any
+# file of the given name existing.
+.PHONY: $(PROJNAME).pdf all clean
+
+# The first rule in a Makefile is the one executed by default ("make"). It
+# should always be the "all" rule, so that "make" and "make all" are identical.
+all: $(PROJNAME).pdf
+
+# CUSTOM BUILD RULES
+
+# In case you didn't know, '$@' is a variable holding the name of the target,
+# and '$<' is a variable holding the (first) dependency of a rule.
+# "raw2tex" and "dat2tex" are just placeholders for whatever custom steps
+# you might have.
+
+%.tex: %.raw
+	./raw2tex $< > $@
+
+%.tex: %.dat
+	./dat2tex $< > $@
+
+# MAIN LATEXMK RULE
+
+# -pdf tells latexmk to generate PDF directly (instead of DVI).
+# -pdflatex="" tells latexmk to call a specific backend with specific options.
+# -use-make tells latexmk to call make for generating missing files.
+
+# -interactive=nonstopmode keeps the pdflatex backend from stopping at a
+# missing file reference and interactively asking you for an alternative.
+
+$(PROJNAME).pdf: $(PROJNAME).tex
+	latexmk -pdf -pdflatex="pdflatex -interactive=nonstopmode" -use-make $<
+
+cleanall:
+	latexmk -C
+
+clean:
+	latexmk -c
--- a/proposal/macros.tex
+++ b/proposal/macros.tex
@ -6,7 +6,7 @@
 \newcommand{\bN}{\mathbb{N}}
 \newcommand{\bC}{\mathbb{C}}
 \newcommand{\bX}{\mathbb{X}}
-\newcommand{\to}{\rightarrow}
+% \newcommand{\to}{\rightarrow}
 \newcommand{\mto}{\mapsto}
 \newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace}
 \let\type\UU
--- a/src/Cat.agda
+++ b/src/Cat.agda
@ -1,13 +1,14 @@
 module Cat where

-import Cat.Cubical
 import Cat.Category
 import Cat.Functor
+import Cat.CwF
 import Cat.Category.Pathy
 import Cat.Category.Bij
 import Cat.Category.Free
 import Cat.Category.Properties
 import Cat.Categories.Sets
-import Cat.Categories.Cat
+-- import Cat.Categories.Cat
 import Cat.Categories.Rel
 import Cat.Categories.Fun
+import Cat.Categories.Cube
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@ -1,3 +1,4 @@
+-- There is no category of categories in our interpretation
 {-# OPTIONS --cubical --allow-unsolved-metas #-}

 module Cat.Categories.Cat where
@ -10,40 +11,39 @@ open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
 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 import Cat.Equality
+open Equality.Data.Product

 open Functor
-open Category
+open IsFunctor
+open Category hiding (_∘_)

 -- The category of categories
 module _ (ℓ ℓ' : Level) where
  private
-    module _ {A B C D : Category ℓ ℓ'} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
+    module _ {𝔸 𝔹 ℂ 𝔻 : Category ℓ ℓ'} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻} where
      private
-        eq* : func* (h ∘f (g ∘f f)) ≡ func* ((h ∘f g) ∘f f)
+        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))
+          (λ i → {A B : 𝔸 .Object} → 𝔸 [ A , B ] → 𝔻 [ eq* i A , eq* i B ])
+          (func→ (H ∘f (G ∘f F))) (func→ ((H ∘f G) ∘f F))
        eq→ = refl
-        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))
+        postulate
+          eqI
+            : (λ i → ∀ {A : 𝔸 .Object} → eq→ i (𝔸 .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A})
+            [ (H ∘f (G ∘f F)) .isFunctor .ident
+            ≡ ((H ∘f G) ∘f F) .isFunctor .ident
+            ]
+          eqD
+            : (λ i → ∀ {A B C} {f : 𝔸 [ A , B ]} {g : 𝔸 [ B , C ]}
+              → eq→ i (𝔸 [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
+            [ (H ∘f (G ∘f F)) .isFunctor .distrib
+            ≡ ((H ∘f G) ∘f F) .isFunctor .distrib
+            ]

-      assc : h ∘f (g ∘f f) ≡ (h ∘f g) ∘f f
-      assc = Functor≡ eq* eq→ eqI eqD
+      assc : H ∘f (G ∘f F) ≡ (H ∘f G) ∘f F
+      assc = Functor≡ eq* eq→ (IsFunctor≡ eqI eqD)

    module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where
      module _ where
@ -57,16 +57,17 @@ module _ (ℓ ℓ' : Level) where
            (func→ (F ∘f identity)) (func→ F)
          eq→ = refl
          postulate
-            eqI-r : PathP (λ i → {c : ℂ .Object}
-                → PathP (λ _ → Arrow 𝔻 (func* F c) (func* F c)) (func→ F (ℂ .𝟙)) (𝔻 .𝟙))
-                        (ident (F ∘f identity)) (ident F)
+            eqI-r
+              : (λ i → {c : ℂ .Object} → (λ _ → 𝔻 [ func* F c , func* F c ])
+                [ func→ F (ℂ .𝟙) ≡ 𝔻 .𝟙 ])
+              [(F ∘f identity) .isFunctor .ident ≡ F .isFunctor .ident ]
            eqD-r : PathP
                        (λ i →
                        {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C} →
-                        eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f))
-                        ((F ∘f identity) .distrib) (distrib F)
+                        eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
+                        ((F ∘f identity) .isFunctor .distrib) (F .isFunctor .distrib)
        ident-r : F ∘f identity ≡ F
-        ident-r = Functor≡ eq* eq→ eqI-r eqD-r
+        ident-r = Functor≡ eq* eq→ (IsFunctor≡ eqI-r eqD-r)
      module _ where
        private
          postulate
@ -74,13 +75,14 @@ module _ (ℓ ℓ' : Level) where
            eq→ : PathP
              (λ i → {x y : Object ℂ} → ℂ .Arrow x y → 𝔻 .Arrow (eq* i x) (eq* i y))
              ((identity ∘f F) .func→) (F .func→)
-            eqI : PathP (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A})
-                 (ident (identity ∘f F)) (ident F)
+            eqI : (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A})
+                  [ ((identity ∘f F) .isFunctor .ident) ≡ (F .isFunctor .ident) ]
            eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C}
-                 → eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f))
-                 (distrib (identity ∘f F)) (distrib F)
+                 → eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
+                 ((identity ∘f F) .isFunctor .distrib) (F .isFunctor .distrib)
+                 -- (λ z → eq* i z) (eq→ i)
        ident-l : identity ∘f F ≡ F
-        ident-l = Functor≡ eq* eq→ eqI eqD
+        ident-l = Functor≡ eq* eq→ λ i → record { ident = eqI i ; distrib = eqD i }

  Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
  Cat =
@ -88,19 +90,18 @@ module _ (ℓ ℓ' : Level) where
      { Object = Category ℓ ℓ'
      ; Arrow = Functor
      ; 𝟙 = identity
-      ; _⊕_ = _∘f_
+      ; _∘_ = _∘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}
+        { assoc = λ {_ _ _ _ F G H} → assc {F = F} {G = G} {H = H}
        ; ident = ident-r , ident-l
        }
      }

 module _ {ℓ ℓ' : Level} where
-  Catt = Cat ℓ ℓ'
-
  module _ (ℂ 𝔻 : Category ℓ ℓ') where
    private
+      Catt = Cat ℓ ℓ'
      :Object: = ℂ .Object × 𝔻 .Object
      :Arrow:  : :Object: → :Object: → Set ℓ'
      :Arrow: (c , d) (c' , d') = Arrow ℂ c c' × Arrow 𝔻 d d'
@ -111,15 +112,15 @@ module _ {ℓ ℓ' : Level} where
        :Arrow: b c →
        :Arrow: a b →
        :Arrow: a c
-      _:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → (ℂ ._⊕_) bc∈C ab∈C , 𝔻 ._⊕_ bc∈D ab∈D}
+      _:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]}

      instance
        :isCategory: : IsCategory :Object: :Arrow: :𝟙: _:⊕:_
        :isCategory: = record
-          { assoc = eqpair C.assoc D.assoc
+          { assoc = Σ≡ C.assoc D.assoc
          ; ident
-          = eqpair (fst C.ident) (fst D.ident)
-          , eqpair (snd C.ident) (snd D.ident)
+          = Σ≡ (fst C.ident) (fst D.ident)
+          , Σ≡ (snd C.ident) (snd D.ident)
          }
          where
            open module C = IsCategory (ℂ .isCategory)
@ -130,41 +131,49 @@ module _ {ℓ ℓ' : Level} where
        { Object = :Object:
        ; Arrow = :Arrow:
        ; 𝟙 = :𝟙:
-        ; _⊕_ = _:⊕:_
+        ; _∘_ = _:⊕:_
        }

-      proj₁ : Arrow Catt :product: ℂ
-      proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl }
+      proj₁ : Catt [ :product: , ℂ ]
+      proj₁ = record { func* = fst ; func→ = fst ; isFunctor = record { ident = refl ; distrib = refl } }

-      proj₂ : Arrow Catt :product: 𝔻
-      proj₂ = record { func* = snd ; func→ = snd ; ident = refl ; distrib = refl }
+      proj₂ : Catt [ :product: , 𝔻 ]
+      proj₂ = record { func* = snd ; func→ = snd ; isFunctor = record { ident = refl ; distrib = refl } }

-      module _ {X : Object Catt} (x₁ : Arrow Catt X ℂ) (x₂ : Arrow Catt X 𝔻) where
+      module _ {X : Object Catt} (x₁ : Catt [ X , ℂ ]) (x₂ : Catt [ X , 𝔻 ]) 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 → x₁ .func* x , x₂ .func* x
          ; func→ = λ x → func→ x₁ x , func→ x₂ x
-          ; ident = lift-eq (ident x₁) (ident x₂)
-          ; distrib = lift-eq (distrib x₁) (distrib x₂)
+          ; isFunctor = record
+            { ident   = Σ≡ x₁.ident x₂.ident
+            ; distrib = Σ≡ x₁.distrib x₂.distrib
+            }
          }
+          where
+            open module x₁ = IsFunctor (x₁ .isFunctor)
+            open module x₂ = IsFunctor (x₂ .isFunctor)

-        -- 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 : (Catt ⊕ proj₁) x ≡ x₁
-        -- isUniqL = Functor≡ refl refl {!!} {!!}
+        isUniqL : Catt [ proj₁ ∘ x ] ≡ x₁
+        isUniqL = Functor≡ eq* eq→ eqIsF -- Functor≡ refl refl λ i → record { ident = refl i ; distrib = refl i }
+          where
+            eq* : (Catt [ proj₁ ∘ x ]) .func* ≡ x₁ .func*
+            eq* = refl
+            eq→ : (λ i → {A : X .Object} {B : X .Object} → X [ A , B ] → ℂ [ eq* i A , eq* i B ])
+                    [ (Catt [ proj₁ ∘ x ]) .func→ ≡ x₁ .func→ ]
+            eq→ = refl
+            postulate eqIsF : (Catt [ proj₁ ∘ x ]) .isFunctor ≡ x₁ .isFunctor
+            -- eqIsF = IsFunctor≡ {!refl!} {!!}

-        postulate isUniqR : (Catt ⊕ proj₂) x ≡ x₂
+        postulate isUniqR : Catt [ proj₂ ∘ x ] ≡ x₂
        -- isUniqR = Functor≡ refl refl {!!} {!!}

-        isUniq : (Catt ⊕ proj₁) x ≡ x₁ × (Catt ⊕ proj₂) x ≡ x₂
+        isUniq : Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂
        isUniq = isUniqL , isUniqR

-        uniq : ∃![ x ] ((Catt ⊕ proj₁) x ≡ x₁ × (Catt ⊕ proj₂) x ≡ x₂)
+        uniq : ∃![ x ] (Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂)
        uniq = x , isUniq

    instance
@ -193,9 +202,6 @@ module _ (ℓ : Level) where
    Catℓ = Cat ℓ ℓ
    module _ (ℂ 𝔻 : Category ℓ ℓ) where
      private
-        _𝔻⊕_ = 𝔻 ._⊕_
-        _ℂ⊕_ = ℂ ._⊕_
-
        :obj: : Cat ℓ ℓ .Object
        :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻}

@ -227,13 +233,13 @@ module _ (ℓ : Level) where
            G→f : 𝔻 .Arrow (G .func* A) (G .func* B)
            G→f = G .func→ f
            l : 𝔻 .Arrow (F .func* A) (G .func* B)
-            l = θB 𝔻⊕ F→f
+            l = 𝔻 [ θB ∘ F→f ]
            r : 𝔻 .Arrow (F .func* A) (G .func* B)
-            r = G→f 𝔻⊕ θA
+            r = 𝔻 [ G→f ∘ θA ]
            -- There are two choices at this point,
            -- but I suppose the whole point is that
            -- by `θNat f` we have `l ≡ r`
-            --     lem : θ B 𝔻⊕ F .func→ f ≡ G .func→ f 𝔻⊕ θ A
+            --     lem : 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
            --     lem = θNat f
            result : 𝔻 .Arrow (F .func* A) (G .func* B)
            result = l
@ -251,19 +257,20 @@ module _ (ℓ : Level) where
        -- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙
        -- :ident: = trans (proj₂ 𝔻.ident) (F .ident)
        --   where
-        --     _𝔻⊕_ = 𝔻 ._⊕_
        --     open module 𝔻 = IsCategory (𝔻 .isCategory)
        -- Unfortunately the equational version has some ambigous arguments.
        :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙 {o = proj₂ c}) ≡ 𝔻 .𝟙
        :ident: = begin
          :func→: {c} {c} ((:obj: ×p ℂ) .Product.obj .𝟙 {c}) ≡⟨⟩
          :func→: {c} {c} (identityNat F , ℂ .𝟙)             ≡⟨⟩
-          (identityTrans F C 𝔻⊕ F .func→ (ℂ .𝟙))             ≡⟨⟩
-          𝔻 .𝟙 𝔻⊕ F .func→ (ℂ .𝟙)                            ≡⟨ proj₂ 𝔻.ident ⟩
-          F .func→ (ℂ .𝟙)                                    ≡⟨ F .ident ⟩
-          𝔻 .𝟙 ∎
+          𝔻 [ identityTrans F C ∘ F .func→ (ℂ .𝟙)]           ≡⟨⟩
+          𝔻 [ 𝔻 .𝟙 ∘ F .func→ (ℂ .𝟙)]                        ≡⟨ proj₂ 𝔻.ident ⟩
+          F .func→ (ℂ .𝟙)                                    ≡⟨ F.ident ⟩
+          𝔻 .𝟙                                               ∎
          where
            open module 𝔻 = IsCategory (𝔻 .isCategory)
+            open module F = IsFunctor (F .isFunctor)
+
      module _ {F×A G×B H×C : Functor ℂ 𝔻 × ℂ .Object} where
        F = F×A .proj₁
        A = F×A .proj₂
@ -272,7 +279,7 @@ module _ (ℓ : Level) where
        H = H×C .proj₁
        C = H×C .proj₂
        -- Not entirely clear what this is at this point:
-        _P⊕_ = (:obj: ×p ℂ) .Product.obj ._⊕_ {F×A} {G×B} {H×C}
+        _P⊕_ = (:obj: ×p ℂ) .Product.obj .Category._∘_ {F×A} {G×B} {H×C}
        module _
          -- NaturalTransformation F G × ℂ .Arrow A B
          {θ×f : NaturalTransformation F G × ℂ .Arrow A B}
@ -292,35 +299,45 @@ module _ (ℓ : Level) where
            g = proj₂ η×g

            ηθNT : NaturalTransformation F H
-            ηθNT = Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat)
+            ηθNT = Fun .Category._∘_ {F} {G} {H} (η , ηNat) (θ , θNat)

            ηθ = proj₁ ηθNT
            ηθNat = proj₂ ηθNT

          :distrib: :
-              (η C 𝔻⊕ θ C) 𝔻⊕ F .func→ (g ℂ⊕ f)
-            ≡ (η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f)
+              𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F .func→ ( ℂ [ g ∘ f ] ) ]
+            ≡ 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ θ B ∘ F .func→ f ] ]
          :distrib: = begin
-            (ηθ C) 𝔻⊕ F .func→ (g ℂ⊕ f)                ≡⟨ ηθNat (g ℂ⊕ f) ⟩
-            H .func→ (g ℂ⊕ f) 𝔻⊕ (ηθ A)                ≡⟨ cong (λ φ → φ 𝔻⊕ ηθ A) (H .distrib) ⟩
-            (H .func→ g 𝔻⊕ H .func→ f) 𝔻⊕ (ηθ A)       ≡⟨ sym assoc ⟩
-            H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (ηθ A))       ≡⟨⟩
-            H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (ηθ A))       ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) assoc ⟩
-            H .func→ g 𝔻⊕ ((H .func→ f 𝔻⊕ η A) 𝔻⊕ θ A) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) (cong (λ φ → φ 𝔻⊕ θ A) (sym (ηNat f))) ⟩
-            H .func→ g 𝔻⊕ ((η B 𝔻⊕ G .func→ f) 𝔻⊕ θ A) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) (sym assoc) ⟩
-            H .func→ g 𝔻⊕ (η B 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) ≡⟨ assoc ⟩
-            (H .func→ g 𝔻⊕ η B) 𝔻⊕ (G .func→ f 𝔻⊕ θ A) ≡⟨ cong (λ φ → φ 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) (sym (ηNat g)) ⟩
-            (η C 𝔻⊕ G .func→ g) 𝔻⊕ (G .func→ f 𝔻⊕ θ A) ≡⟨ cong (λ φ → (η C 𝔻⊕ G .func→ g) 𝔻⊕ φ) (sym (θNat f)) ⟩
-            (η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f) ∎
+            𝔻 [ (ηθ C) ∘ F .func→ (ℂ [ g ∘ f ]) ]
+              ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩
+            𝔻 [ H .func→ (ℂ [ g ∘ f ]) ∘ (ηθ A) ]
+              ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.distrib) ⟩
+            𝔻 [ 𝔻 [ H .func→ g ∘ H .func→ f ] ∘ (ηθ A) ]
+              ≡⟨ sym assoc ⟩
+            𝔻 [ H .func→ g ∘ 𝔻 [ H .func→ f ∘ ηθ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) assoc ⟩
+            𝔻 [ H .func→ g ∘ 𝔻 [ 𝔻 [ H .func→ f ∘ η A ] ∘ θ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩
+            𝔻 [ H .func→ g ∘ 𝔻 [ 𝔻 [ η B ∘ G .func→ f ] ∘ θ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) (sym assoc) ⟩
+            𝔻 [ H .func→ g ∘ 𝔻 [ η B ∘ 𝔻 [ G .func→ f ∘ θ A ] ] ] ≡⟨ assoc ⟩
+            𝔻 [ 𝔻 [ H .func→ g ∘ η B ] ∘ 𝔻 [ G .func→ f ∘ θ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ G .func→ f ∘ θ A ] ]) (sym (ηNat g)) ⟩
+            𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ G .func→ f ∘ θ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ φ ]) (sym (θNat f)) ⟩
+            𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ θ B ∘ F .func→ f ] ] ∎
            where
              open IsCategory (𝔻 .isCategory)
+              open module H = IsFunctor (H .isFunctor)

      :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻
      :eval: = record
        { func* = :func*:
        ; func→ = λ {dom} {cod} → :func→: {dom} {cod}
-        ; ident = λ {o} → :ident: {o}
-        ; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y}
+        ; isFunctor = record
+          { ident = λ {o} → :ident: {o}
+          ; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y}
+          }
        }

      module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where
@ -328,9 +345,9 @@ module _ (ℓ : Level) where

        postulate
          transpose : Functor 𝔸 :obj:
-          eq : Catℓ ._⊕_ :eval: (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ≡ F
+          eq : Catℓ [ :eval: ∘ (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ] ≡ F

-        catTranspose : ∃![ F~ ] (Catℓ ._⊕_ :eval: (parallelProduct F~ (Catℓ .𝟙 {o = ℂ})) ≡ F)
+        catTranspose : ∃![ F~ ] (Catℓ [ :eval: ∘ (parallelProduct F~ (Catℓ .𝟙 {o = ℂ}))] ≡ F )
        catTranspose = transpose , eq

      :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
--- a/src/Cat/Categories/Cube.agda
+++ b/src/Cat/Categories/Cube.agda
@ -0,0 +1,79 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module Cat.Categories.Cube where
+
+open import Level
+open import Data.Bool hiding (T)
+open import Data.Sum hiding ([_,_])
+open import Data.Unit
+open import Data.Empty
+open import Data.Product
+open import Cubical
+open import Function
+open import Relation.Nullary
+open import Relation.Nullary.Decidable
+
+open import Cat.Category
+open import Cat.Functor
+open import Cat.Equality
+open Equality.Data.Product
+
+-- 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
+
+open Category hiding (_∘_)
+open Functor
+
+module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
+  -- Ns is the "namespace"
+  ℓo = (suc zero ⊔ ℓ)
+
+  FiniteDecidableSubset : Set ℓ
+  FiniteDecidableSubset = Ns → Dec ⊤
+
+  isTrue : Bool → Set
+  isTrue false = ⊥
+  isTrue true = ⊤
+
+  elmsof : FiniteDecidableSubset → Set ℓ
+  elmsof P = Σ Ns (λ σ → True (P σ)) -- (σ : Ns) → isTrue (P σ)
+
+  𝟚 : Set
+  𝟚 = Bool
+
+  module _ (I J : FiniteDecidableSubset) where
+    private
+      Hom' : Set ℓ
+      Hom' = elmsof I → elmsof J ⊎ 𝟚
+      isInl : {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} → A ⊎ B → Set
+      isInl (inj₁ _) = ⊤
+      isInl (inj₂ _) = ⊥
+
+      Def : Set ℓ
+      Def = (f : Hom') → Σ (elmsof I) (λ i → isInl (f i))
+
+      rules : Hom' → Set ℓ
+      rules f = (i j : elmsof I)
+        → case (f i) of λ
+          { (inj₁ (fi , _)) → case (f j) of λ
+            { (inj₁ (fj , _)) → fi ≡ fj → i ≡ j
+            ; (inj₂ _) → Lift ⊤
+            }
+          ; (inj₂ _) → Lift ⊤
+          }
+
+    Hom = Σ Hom' rules
+
+  -- The category of names and substitutions
+  Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
+  Rawℂ = record
+    { Object = FiniteDecidableSubset
+    -- { Object = Ns → Bool
+    ; Arrow = Hom
+    ; 𝟙 = λ { {o} → inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} } }
+    ; _∘_ = {!!}
+    }
+  postulate RawIsCategoryℂ : IsCategory Rawℂ
+  ℂ : Category ℓ ℓ
+  ℂ = Rawℂ , RawIsCategoryℂ
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@ -0,0 +1,54 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module Cat.Categories.Fam where
+
+open import Agda.Primitive
+open import Data.Product
+open import Cubical
+import Function
+
+open import Cat.Category
+open import Cat.Equality
+
+open Equality.Data.Product
+
+module _ (ℓa ℓb : Level) where
+  private
+    Obj' = Σ[ A ∈ Set ℓa ] (A → Set ℓb)
+    Arr : Obj' → Obj' → Set (ℓa ⊔ ℓb)
+    Arr (A , B) (A' , B') = Σ[ f ∈ (A → A') ] ({x : A} → B x → B' (f x))
+    one : {o : Obj'} → Arr o o
+    proj₁ one = λ x → x
+    proj₂ one = λ b → b
+    _∘_ : {a b c : Obj'} → Arr b c → Arr a b → Arr a c
+    (g , g') ∘ (f , f') = g Function.∘ f , g' Function.∘ f'
+    _⟨_∘_⟩ : {a b : Obj'} → (c : Obj') → Arr b c → Arr a b → Arr a c
+    c ⟨ g ∘ f ⟩ = _∘_ {c = c} g f
+
+    module _ {A B C D : Obj'} {f : Arr A B} {g : Arr B C} {h : Arr C D} where
+      assoc : (D ⟨ h ∘ C ⟨ g ∘ f ⟩ ⟩) ≡ D ⟨ D ⟨ h ∘ g ⟩ ∘ f ⟩
+      assoc = Σ≡ refl refl
+
+    module _ {A B : Obj'} {f : Arr A B} where
+      ident : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f
+      ident = (Σ≡ refl refl) , Σ≡ refl refl
+
+
+    RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
+    RawFam = record
+      { Object = Obj'
+      ; Arrow = Arr
+      ; 𝟙 = one
+      ; _∘_ = λ {a b c} → _∘_ {a} {b} {c}
+      }
+
+    instance
+      isCategory : IsCategory RawFam
+      isCategory = record
+        { assoc = λ {A} {B} {C} {D} {f} {g} {h} → assoc {D = D} {f} {g} {h}
+        ; ident = λ {A} {B} {f} → ident {A} {B} {f = f}
+        ; arrow-is-set = ?
+        ; univalent = ?
+        }
+
+  Fam : Category (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
+  Fam = RawFam , isCategory
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@ -10,19 +10,19 @@ open import Cat.Category
 open import Cat.Functor

 module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
-  open Category
+  open Category hiding ( _∘_ ; Arrow )
  open Functor

  module _ (F G : Functor ℂ 𝔻) where
    -- What do you call a non-natural tranformation?
    Transformation : Set (ℓc ⊔ ℓd')
-    Transformation = (C : ℂ .Object) → 𝔻 .Arrow (F .func* C) (G .func* C)
+    Transformation = (C : ℂ .Object) → 𝔻 [ F .func* C , G .func* C ]

    Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
    Natural θ
      = {A B : ℂ .Object}
-      → (f : ℂ .Arrow A B)
-      → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A)
+      → (f : ℂ [ A , B ])
+      → 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]

    NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
    NaturalTransformation = Σ Transformation Natural
@ -30,43 +30,53 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
    -- NaturalTranformation : Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
    -- NaturalTranformation = ∀ (θ : Transformation) {A B : ℂ .Object} → (f : ℂ .Arrow A B) → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A)

+  module _ {F G : Functor ℂ 𝔻} where
+    NaturalTransformation≡ : {α β : NaturalTransformation F G}
+      → (eq₁ : α .proj₁ ≡ β .proj₁)
+      → (eq₂ : PathP
+          (λ i → {A B : ℂ .Object} (f : ℂ [ A , B ])
+            → 𝔻 [ eq₁ i B ∘ F .func→ f ]
+            ≡ 𝔻 [ G .func→ f ∘ eq₁ i A ])
+        (α .proj₂) (β .proj₂))
+      → α ≡ β
+    NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i
+
  identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
  identityTrans F C = 𝔻 .𝟙

  identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
  identityNatural F {A = A} {B = B} f = begin
-    identityTrans F B 𝔻⊕ F→ f                 ≡⟨⟩
-    𝔻 .𝟙              𝔻⊕ F→ f                 ≡⟨ proj₂ 𝔻.ident ⟩
-    F→ f                                       ≡⟨ sym (proj₁ 𝔻.ident) ⟩
-    F→ f              𝔻⊕ 𝔻 .𝟙                 ≡⟨⟩
-    F→ f              𝔻⊕ identityTrans F A     ∎
+    𝔻 [ identityTrans F B ∘ F→ f ]  ≡⟨⟩
+    𝔻 [ 𝔻 .𝟙 ∘  F→ f ]              ≡⟨ proj₂ 𝔻.ident ⟩
+    F→ f                            ≡⟨ sym (proj₁ 𝔻.ident) ⟩
+    𝔻 [ F→ f ∘ 𝔻 .𝟙 ]               ≡⟨⟩
+    𝔻 [ F→ f ∘ identityTrans F A ]  ∎
    where
-      _𝔻⊕_ = 𝔻 ._⊕_
      F→ = F .func→
-      open module 𝔻 = IsCategory (𝔻 .isCategory)
+      module 𝔻 = IsCategory (isCategory 𝔻)

  identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F
  identityNat F = identityTrans F , identityNatural F

  module _ {F G H : Functor ℂ 𝔻} where
    private
-      _𝔻⊕_ = 𝔻 ._⊕_
      _∘nt_ : Transformation G H → Transformation F G → Transformation F H
-      (θ ∘nt η) C = θ C 𝔻⊕ η C
+      (θ ∘nt η) C = 𝔻 [ θ C ∘ η C ]

    NatComp _:⊕:_ : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
    proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η
    proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin
-      ((θ ∘nt η) B) 𝔻⊕ (F .func→ f)    ≡⟨⟩
-      (θ B 𝔻⊕ η B) 𝔻⊕ (F .func→ f)     ≡⟨ sym assoc ⟩
-      θ B 𝔻⊕ (η B 𝔻⊕ (F .func→ f))     ≡⟨ cong (λ φ → θ B 𝔻⊕ φ) (ηNat f) ⟩
-      θ B 𝔻⊕ ((G .func→ f) 𝔻⊕ η A)     ≡⟨ assoc ⟩
-      (θ B 𝔻⊕ (G .func→ f)) 𝔻⊕ η A     ≡⟨ cong (λ φ → φ 𝔻⊕ η A) (θNat f) ⟩
-      (((H .func→ f) 𝔻⊕ θ A) 𝔻⊕ η A)   ≡⟨ sym assoc ⟩
-      ((H .func→ f) 𝔻⊕ (θ A 𝔻⊕ η A))   ≡⟨⟩
-      ((H .func→ f)  𝔻⊕ ((θ ∘nt η) A)) ∎
+      𝔻 [ (θ ∘nt η) B ∘ F .func→ f ]     ≡⟨⟩
+      𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F .func→ f ] ≡⟨ sym assoc ⟩
+      𝔻 [ θ B ∘ 𝔻 [ η B ∘ F .func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
+      𝔻 [ θ B ∘ 𝔻 [ G .func→ f ∘ η A ] ] ≡⟨ assoc ⟩
+      𝔻 [ 𝔻 [ θ B ∘ G .func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
+      𝔻 [ 𝔻 [ H .func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym assoc ⟩
+      𝔻 [ H .func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
+      𝔻 [ H .func→ f ∘ (θ ∘nt η) A ]     ∎
      where
-        open IsCategory (𝔻 .isCategory)
+        open IsCategory (isCategory 𝔻)
+
    NatComp = _:⊕:_

  private
@ -86,31 +96,35 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
        × (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
      :ident: = ident-r , ident-l

-  instance
-    :isCategory: : IsCategory (Functor ℂ 𝔻) NaturalTransformation
-      (λ {F} → identityNat F) (λ {a} {b} {c} → _:⊕:_ {a} {b} {c})
-    :isCategory: = record
-      { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D}
-      ; ident = λ {A B} → :ident: {A} {B}
-      }
-
  -- Functor categories. Objects are functors, arrows are natural transformations.
-  Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
-  Fun = record
+  RawFun : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
+  RawFun = record
    { Object = Functor ℂ 𝔻
    ; Arrow = NaturalTransformation
    ; 𝟙 = λ {F} → identityNat F
-    ; _⊕_ = λ {F G H} → _:⊕:_ {F} {G} {H}
+    ; _∘_ = λ {F G H} → _:⊕:_ {F} {G} {H}
    }

+  instance
+    :isCategory: : IsCategory RawFun
+    :isCategory: = record
+      { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D}
+      ; ident = λ {A B} → :ident: {A} {B}
+      ; arrow-is-set = ?
+      ; univalent = ?
+      }
+
+  Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
+  Fun = RawFun , :isCategory:
+
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
  open import Cat.Categories.Sets

  -- Restrict the functors to Presheafs.
-  Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
-  Presh = record
+  RawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
+  RawPresh = record
    { Object = Presheaf ℂ
    ; Arrow = NaturalTransformation
    ; 𝟙 = λ {F} → identityNat F
-    ; _⊕_ = λ {F G H} → NatComp {F = F} {G = G} {H = H}
+    ; _∘_ = λ {F G H} → NatComp {F = F} {G = G} {H = H}
    }
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@ -1,4 +1,4 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
 module Cat.Categories.Rel where

 open import Cubical
@ -154,11 +154,18 @@ 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 (lsuc lzero) (lsuc lzero)
-Rel = record
+RawRel : RawCategory (lsuc lzero) (lsuc lzero)
+RawRel = 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 )}
-  ; isCategory = record { assoc = funExt is-assoc ; ident = funExt ident-l , funExt ident-r }
+  ; _∘_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
+  }
+
+RawIsCategoryRel : IsCategory RawRel
+RawIsCategoryRel = record
+  { assoc = funExt is-assoc
+  ; ident = funExt ident-l , funExt ident-r
+  ; arrow-is-set = {!!}
+  ; univalent = {!!}
  }
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@ -1,41 +1,49 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Categories.Sets where

 open import Cubical
 open import Agda.Primitive
 open import Data.Product
-open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
+import Function

 open import Cat.Category
 open import Cat.Functor
 open Category

 module _ {ℓ : Level} where
-  Sets : Category (lsuc ℓ) ℓ
-  Sets = record
-    { Object = Set ℓ
-    ; Arrow = λ T U → T → U
-    ; 𝟙 = id
-    ; _⊕_ = _∘′_
-    ; isCategory = record { assoc = refl ; ident = funExt (λ _ → refl) , funExt (λ _ → refl) }
+  SetsRaw : RawCategory (lsuc ℓ) ℓ
+  SetsRaw = record
+       { Object = Set ℓ
+       ; Arrow = λ T U → T → U
+       ; 𝟙 = Function.id
+       ; _∘_ = Function._∘′_
+       }
+
+  SetsIsCategory : IsCategory SetsRaw
+  SetsIsCategory = record
+    { assoc = refl
+    ; ident = funExt (λ _ → refl) , funExt (λ _ → refl)
+    ; arrow-is-set = {!!}
+    ; univalent = {!!}
    }
-    where
-      open import Function
+
+  Sets : Category (lsuc ℓ) ℓ
+  Sets = SetsRaw , 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
-      _S⊕_ = Sets ._⊕_
-      lem : proj₁ S⊕ (f &&& g) ≡ f × snd S⊕ (f &&& g) ≡ g
+      lem : Sets [ proj₁ ∘ (f &&& g)] ≡ f × Sets [ proj₂ ∘ (f &&& g)] ≡ g
      proj₁ lem = refl
      proj₂ lem = refl
    instance
-      isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} fst snd
+      isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} proj₁ proj₂
      isProduct f g = f &&& g , lem f g

    product : (A B : Sets .Object) → Product {ℂ = Sets} A B
-    product A B = record { obj = A × B ; proj₁ = fst ; proj₂ = snd ; isProduct = isProduct }
+    product A B = record { obj = A × B ; proj₁ = proj₁ ; proj₂ = proj₂ ; isProduct = isProduct }

  instance
    SetsHasProducts : HasProducts Sets
@ -49,12 +57,14 @@ Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
 representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
 representable {ℂ = ℂ} A = record
  { func* = λ B → ℂ .Arrow A B
-  ; func→ = ℂ ._⊕_
-  ; ident = funExt λ _ → snd ident
-  ; distrib = funExt λ x → sym assoc
+  ; func→ = ℂ ._∘_
+  ; isFunctor = record
+    { ident = funExt λ _ → proj₂ ident
+    ; distrib = funExt λ x → sym assoc
+    }
  }
  where
-    open IsCategory (ℂ .isCategory)
+    open IsCategory (isCategory ℂ)

 -- Contravariant Presheaf
 Presheaf : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
@ -64,9 +74,11 @@ Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
 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→ = λ f g → ℂ ._∘_ g f
+  ; isFunctor = record
+    { ident = funExt λ x → proj₁ ident
+    ; distrib = funExt λ x → assoc
+    }
  }
  where
-    open IsCategory (ℂ .isCategory)
+    open IsCategory (isCategory ℂ)
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@ -1,4 +1,4 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --allow-unsolved-metas --cubical #-}

 module Cat.Category where

@ -10,8 +10,9 @@ open import Data.Product renaming
  ; ∃! to ∃!≈
  )
 open import Data.Empty
-open import Function
+import Function
 open import Cubical
+open import Cubical.GradLemma using ( propIsEquiv )

 ∃! : ∀ {a b} {A : Set a}
  → (A → Set b) → Set (a ⊔ b)
@ -22,57 +23,119 @@ open import Cubical

 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
+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
-    {{isCategory}} : IsCategory Object Arrow 𝟙 _⊕_
-  infixl 45 _⊕_
+    _∘_    : {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

-open Category
+-- Thierry: All projections must be `isProp`'s

-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 ≡ ℂ .𝟙
+-- 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 ℂ
+  -- (Object : Set ℓ)
+  -- (Arrow  : Object → Object → Set ℓ')
+  -- (𝟙      : {o : Object} → Arrow o o)
+  -- (_∘_    : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c)
+  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
+    arrow-is-set : ∀ {A B : Object} → isSet (Arrow A B)

-    Epimorphism : {X : ℂ .Object } → (f : ℂ .Arrow A B) → Set ℓ'
-    Epimorphism {X} f = ( g₀ g₁ : ℂ .Arrow B X ) → ℂ ._⊕_ g₀ f ≡ ℂ ._⊕_ g₁ f → g₀ ≡ g₁
+  Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
+  Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙

-    Monomorphism : {X : ℂ .Object} → (f : ℂ .Arrow A B) → Set ℓ'
-    Monomorphism {X} f = ( g₀ g₁ : ℂ .Arrow X A ) → ℂ ._⊕_ f g₀ ≡ ℂ ._⊕_ f g₁ → g₀ ≡ g₁
+  _≅_ : (A B : Object) → Set ℓb
+  _≅_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f)

-  -- Isomorphism of objects
-  _≅_ : (A B : Object ℂ) → Set ℓ'
-  _≅_ A B = Σ[ f ∈ ℂ .Arrow A B ] (Isomorphism f)
+  idIso : (A : Object) → A ≅ A
+  idIso A = 𝟙 , (𝟙 , ident)

-module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} where
-  IsProduct : (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
+  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.
+  field
+    univalent : {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
+
+  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} {ℂ : 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
+    { assoc = x.arrow-is-set _ _ x.assoc y.assoc i
+    ; ident =
+      ( x.arrow-is-set _ _ (fst x.ident) (fst y.ident) i
+      , x.arrow-is-set _ _ (snd x.ident) (snd y.ident) i
+      )
+    -- ; arrow-is-set = {!λ x₁ y₁ p q → x.arrow-is-set _ _ p q!}
+    ; arrow-is-set = λ _ _ p q →
+      let
+        golden : x.arrow-is-set _ _ p q ≡ y.arrow-is-set _ _ p q
+        golden = λ j k l → {!!}
+      in
+        golden i
+      ; univalent = λ y₁ → {!!}
+    }
+    where
+      module x = IsCategory x
+      module y = IsCategory y
+
+Category : (ℓa ℓb : Level) → Set (lsuc (ℓa ⊔ ℓb))
+Category ℓa ℓb = Σ (RawCategory ℓa ℓb) IsCategory
+
+module Category {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  raw = fst ℂ
+  open RawCategory raw public
+  isCategory = snd ℂ
+
+open RawCategory
+
+-- _∈_ : ∀ {ℓa ℓb} (ℂ : Category ℓa ℓb) → (ℂ .fst .Object → Set ℓb) → Set (ℓa ⊔ ℓb)
+-- A ∈ ℂ =
+
+Obj : ∀ {ℓa ℓb} → Category ℓa ℓb → Set ℓa
+Obj ℂ = ℂ .fst .Object
+
+_[_,_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → (A : Obj ℂ) → (B : Obj ℂ) → Set ℓ'
+ℂ [ A , B ] = ℂ .fst .Arrow A B
+
+_[_∘_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → {A B C : Obj ℂ} → (g : ℂ [ B , C ]) → (f : ℂ [ A , B ]) → ℂ [ A , C ]
+ℂ [ g ∘ f ] = ℂ .fst ._∘_ g f
+
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Obj ℂ} where
+  IsProduct : (π₁ : ℂ [ obj , A ]) (π₂ : ℂ [ obj , B ]) → Set (ℓ ⊔ ℓ')
  IsProduct π₁ π₂
-    = ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B)
-    → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ ._⊕_ π₂ x ≡ x₂)
+    = ∀ {X : Obj ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
+    → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ × ℂ [ π₂ ∘ x ] ≡ x₂)

 -- Tip from Andrea; Consider this style for efficiency:
 -- record IsProduct {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'})
@ -81,46 +144,55 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} whe
 --      isProduct : ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B)
 --        → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ. _⊕_ π₂ x ≡ x₂)

-record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : ℂ .Object) : Set (ℓ ⊔ ℓ') where
+record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Obj ℂ) : Set (ℓ ⊔ ℓ') where
  no-eta-equality
  field
-    obj : ℂ .Object
-    proj₁ : ℂ .Arrow obj A
-    proj₂ : ℂ .Arrow obj B
+    obj : Obj ℂ
+    proj₁ : ℂ [ obj , A ]
+    proj₂ : ℂ [ obj , B ]
    {{isProduct}} : IsProduct ℂ proj₁ proj₂

-  arrowProduct : ∀ {X} → (π₁ : Arrow ℂ X A) (π₂ : Arrow ℂ X B)
-    → Arrow ℂ X obj
+  arrowProduct : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
+    → ℂ [ X , obj ]
  arrowProduct π₁ π₂ = fst (isProduct π₁ π₂)

 record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
  field
-    product : ∀ (A B : ℂ .Object) → Product {ℂ = ℂ} A B
+    product : ∀ (A B : Obj ℂ) → Product {ℂ = ℂ} A B

  open Product

-  objectProduct : (A B : ℂ .Object) → ℂ .Object
+  objectProduct : (A B : Obj ℂ) → Obj ℂ
  objectProduct A B = Product.obj (product A B)
  -- The product mentioned in awodey in Def 6.1 is not the regular product of arrows.
  -- It's a "parallel" product
-  parallelProduct : {A A' B B' : ℂ .Object} → ℂ .Arrow A A' → ℂ .Arrow B B'
-    → ℂ .Arrow (objectProduct A B) (objectProduct A' B')
+  parallelProduct : {A A' B B' : Obj ℂ} → ℂ [ A , A' ] → ℂ [ B , B' ]
+    → ℂ [ objectProduct A B , objectProduct A' B' ]
  parallelProduct {A = A} {A' = A'} {B = B} {B' = B'} a b = arrowProduct (product A' B')
-    (ℂ ._⊕_ a ((product A B) .proj₁))
-    (ℂ ._⊕_ b ((product A B) .proj₂))
+    (ℂ [ a ∘ (product A B) .proj₁ ])
+    (ℂ [ b ∘ (product A B) .proj₂ ])

-module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-  Opposite : Category ℓ ℓ'
-  Opposite =
-    record
-      { Object = ℂ .Object
-      ; Arrow = flip (ℂ .Arrow)
-      ; 𝟙 = ℂ .𝟙
-      ; _⊕_ = flip (ℂ ._⊕_)
-      ; isCategory = record { assoc = sym assoc ; ident = swap ident }
+module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  private
+    open Category ℂ
+    module ℂ = RawCategory (ℂ .fst)
+    OpRaw : RawCategory ℓa ℓb
+    OpRaw = record
+      { Object = ℂ.Object
+      ; Arrow = Function.flip ℂ.Arrow
+      ; 𝟙 = ℂ.𝟙
+      ; _∘_ = Function.flip (ℂ._∘_)
      }
-      where
-        open IsCategory (ℂ .isCategory)
+    open IsCategory isCategory
+    OpIsCategory : IsCategory OpRaw
+    OpIsCategory = record
+      { assoc = sym assoc
+      ; ident = swap ident
+      ; arrow-is-set = {!!}
+      ; univalent = {!!}
+      }
+  Opposite : Category ℓa ℓb
+  Opposite = OpRaw , OpIsCategory

 -- A consequence of no-eta-equality; `Opposite-is-involution` is no longer
 -- definitional - i.e.; you must match on the fields:
@ -133,44 +205,52 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
 -- 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
-  HomFromArrow : (A : ℂ .Object) → {B B' : ℂ .Object} → (g : ℂ .Arrow B B')
-    → Hom ℂ A B → Hom ℂ A B'
-  HomFromArrow _A = _⊕_ ℂ
-
 module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} where
  open HasProducts hasProducts
  open Product hiding (obj)
  private
-    _×p_ : (A B : ℂ .Object) → ℂ .Object
+    _×p_ : (A B : Obj ℂ) → Obj ℂ
    _×p_ A B = Product.obj (product A B)

-  module _ (B C : ℂ .Category.Object) where
-    IsExponential : (Cᴮ : ℂ .Object) → ℂ .Arrow (Cᴮ ×p B) C → Set (ℓ ⊔ ℓ')
-    IsExponential Cᴮ eval = ∀ (A : ℂ .Object) (f : ℂ .Arrow (A ×p B) C)
-      → ∃![ f~ ] (ℂ ._⊕_ eval (parallelProduct f~ (ℂ .𝟙)) ≡ f)
+  module _ (B C : Obj ℂ) where
+    IsExponential : (Cᴮ : Obj ℂ) → ℂ [ Cᴮ ×p B , C ] → Set (ℓ ⊔ ℓ')
+    IsExponential Cᴮ eval = ∀ (A : Obj ℂ) (f : ℂ [ A ×p B , C ])
+      → ∃![ f~ ] (ℂ [ eval ∘ parallelProduct f~ (Category.raw ℂ .𝟙)] ≡ f)

    record Exponential : Set (ℓ ⊔ ℓ') where
      field
        -- obj ≡ Cᴮ
-        obj : ℂ .Object
-        eval : ℂ .Arrow ( obj ×p B ) C
+        obj : Obj ℂ
+        eval : ℂ [ obj ×p B , C ]
        {{isExponential}} : IsExponential obj eval
      -- If I make this an instance-argument then the instance resolution
      -- algorithm goes into an infinite loop. Why?
      exponentialsHaveProducts : HasProducts ℂ
      exponentialsHaveProducts = hasProducts
-      transpose : (A : ℂ .Object) → ℂ .Arrow (A ×p B) C → ℂ .Arrow A obj
+      transpose : (A : Obj ℂ) → ℂ [ A ×p B , C ] → ℂ [ A , obj ]
      transpose A f = fst (isExponential A f)

 record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where
  field
-    exponent : (A B : ℂ .Object) → Exponential ℂ A B
+    exponent : (A B : Obj ℂ) → Exponential ℂ A B

 record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
  field
    {{hasProducts}}     : HasProducts ℂ
    {{hasExponentials}} : HasExponentials ℂ
+
+module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  unique = isContr
+
+  IsInitial : Obj ℂ → Set (ℓa ⊔ ℓb)
+  IsInitial I = {X : Obj ℂ} → unique (ℂ [ I , X ])
+
+  IsTerminal : Obj ℂ → Set (ℓa ⊔ ℓb)
+  -- ∃![ ? ] ?
+  IsTerminal T = {X : Obj ℂ} → unique (ℂ [ X , T ])
+
+  Initial : Set (ℓa ⊔ ℓb)
+  Initial = Σ (Obj ℂ) IsInitial
+
+  Terminal : Set (ℓa ⊔ ℓb)
+  Terminal = Σ (Obj ℂ) IsTerminal
--- a/src/Cat/Category/Free.agda
+++ b/src/Cat/Category/Free.agda
@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Category.Free where

 open import Agda.Primitive
@ -9,28 +10,33 @@ open import Cat.Category as C
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
  private
    open module ℂ = Category ℂ
-    Obj = ℂ.Object

  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
+    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
+    module _ {A B C D : Obj ℂ} {r : Path A B} {q : Path B C} {p : Path C D} where
      postulate
        p-assoc : concatenate {A} {C} {D} p (concatenate {A} {B} {C} q r)
          ≡ concatenate {A} {B} {D} (concatenate {B} {C} {D} p q) r
-    module _ {A B : Obj} {p : Path A B} where
+    module _ {A B : Obj ℂ} {p : Path A B} where
      postulate
        ident-r : concatenate {A} {A} {B} p (emptyPath A) ≡ p
        ident-l : concatenate {A} {B} {B} (emptyPath B) p ≡ p

-  Free : Category ℓ ℓ'
-  Free = record
-    { Object = Obj
+  RawFree : RawCategory ℓ ℓ'
+  RawFree = record
+    { Object = Obj ℂ
    ; Arrow = Path
    ; 𝟙 = λ {o} → emptyPath o
-    ; _⊕_ = λ {a b c} → concatenate {a} {b} {c}
-    ; isCategory = record { assoc = p-assoc ; ident = ident-r , ident-l }
+    ; _∘_ = λ {a b c} → concatenate {a} {b} {c}
+    }
+  RawIsCategoryFree : IsCategory RawFree
+  RawIsCategoryFree = record
+    { assoc = p-assoc
+    ; ident = ident-r , ident-l
+    ; arrow-is-set = {!!}
+    ; univalent = {!!}
    }
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@ -9,36 +9,37 @@ open import Cubical
 open import Cat.Category
 open import Cat.Functor
 open import Cat.Categories.Sets
+open import Cat.Equality
+open Equality.Data.Product

 module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Category.Object } {X : ℂ .Category.Object} (f : ℂ .Category.Arrow A B) where
  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
+  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₀ ∘ 𝟙          ≡⟨ 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 : 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₀        ≡⟨ 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 : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
  iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso

 {-
@ -48,45 +49,76 @@ epi-mono-is-not-iso f =
  in {!!}
 -}

-module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
-  open import Cat.Category
-  open Category
-  open import Cat.Categories.Cat using (Cat)
-  open import Cat.Categories.Fun
-  open import Cat.Categories.Sets
-  module Cat = Cat.Categories.Cat
-  open Exponential
-  private
-    Catℓ = Cat ℓ ℓ
-    prshf = presheaf {ℂ = ℂ}
+open import Cat.Category
+open Category
+open import Cat.Functor
+open Functor

-    -- Exp : Set (lsuc (lsuc ℓ))
-    -- Exp = Exponential (Cat (lsuc ℓ) ℓ)
-    --   Sets (Opposite ℂ)
+-- module _ {ℓ : Level} {ℂ : Category ℓ ℓ}
+--   {isSObj : isSet (ℂ .Object)}
+--   {isz2 : ∀ {ℓ} → {A B : Set ℓ} → isSet (Sets [ A , B ])} where
+--   -- open import Cat.Categories.Cat using (Cat)
+--   open import Cat.Categories.Fun
+--   open import Cat.Categories.Sets
+--   -- module Cat = Cat.Categories.Cat
+--   open Exponential
+--   private
+--     Catℓ = Cat ℓ ℓ
+--     prshf = presheaf {ℂ = ℂ}
+--     module ℂ = IsCategory (ℂ .isCategory)

-    _⇑_ : (A B : Catℓ .Object) → Catℓ .Object
-    A ⇑ B = (exponent A B) .obj
-      where
-        open HasExponentials (Cat.hasExponentials ℓ)
+--     -- Exp : Set (lsuc (lsuc ℓ))
+--     -- Exp = Exponential (Cat (lsuc ℓ) ℓ)
+--     --   Sets (Opposite ℂ)

-    module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where
-      :func→: : NaturalTransformation (prshf A) (prshf B)
-      :func→: = (λ C x → (ℂ ._⊕_ f x)) , λ f₁ → funExt λ x → lem
-        where
-          lem = (ℂ .isCategory) .IsCategory.assoc
-    module _ {c : ℂ .Object} where
-      eqTrans : (:func→: (ℂ .𝟙 {c})) .proj₁ ≡ (Fun .𝟙 {o = prshf c}) .proj₁
-      eqTrans = funExt λ x → funExt λ x → ℂ .isCategory .IsCategory.ident .proj₂
-      eqNat : (i : I) → Natural (prshf c) (prshf c) (eqTrans i)
-      eqNat i f = {!!}
+--     _⇑_ : (A B : Catℓ .Object) → Catℓ .Object
+--     A ⇑ B = (exponent A B) .obj
+--       where
+--         open HasExponentials (Cat.hasExponentials ℓ)

-      :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c})
-      :ident: i = eqTrans i , eqNat i
+--     module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where
+--       :func→: : NaturalTransformation (prshf A) (prshf B)
+--       :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.assoc

-  yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}})
-  yoneda = record
-    { func* = prshf
-    ; func→ = :func→:
-    ; ident = :ident:
-    ; distrib = {!!}
-    }
+--     module _ {c : ℂ .Object} where
+--       eqTrans : (λ _ → Transformation (prshf c) (prshf c))
+--         [ (λ _ x → ℂ [ ℂ .𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
+--       eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂
+
+--       eqNat : (λ i → Natural (prshf c) (prshf c) (eqTrans i))
+--         [(λ _ → funExt (λ _ → ℂ.assoc)) ≡ identityNatural (prshf c)]
+--       eqNat = λ i {A} {B} f →
+--         let
+--          open IsCategory (Sets .isCategory)
+--          lemm : (Sets [ eqTrans i B ∘ prshf c .func→ f ]) ≡
+--            (Sets [ prshf c .func→ f ∘ eqTrans i A ])
+--          lemm = {!!}
+--          lem : (λ _ → Sets [ Functor.func* (prshf c) A , prshf c .func* B ])
+--                 [ Sets [ eqTrans i B ∘ prshf c .func→ f ]
+--                 ≡ Sets [ prshf c .func→ f ∘ eqTrans i A ] ]
+--          lem
+--           = isz2 _ _ lemm _ i
+--             -- (Sets [ eqTrans i B ∘ prshf c .func→ f ])
+--             -- (Sets [ prshf c .func→ f ∘ eqTrans i A ])
+--             -- lemm
+--             -- _ i
+--         in
+--           lem
+--       -- eqNat = λ {A} {B} i ℂ[B,A] i' ℂ[A,c] →
+--       --   let
+--       --     k : ℂ [ {!!} , {!!} ]
+--       --     k = ℂ[A,c]
+--       --   in {!ℂ [ ? ∘ ? ]!}
+
+--       :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c})
+--       :ident: = Σ≡ eqTrans eqNat
+
+--   yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}})
+--   yoneda = record
+--     { func* = prshf
+--     ; func→ = :func→:
+--     ; isFunctor = record
+--       { ident = :ident:
+--       ; distrib = {!!}
+--       }
+--     }
--- a/src/Cat/Cubical.agda
+++ b/src/Cat/Cubical.agda
@ -1,101 +0,0 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-module Cat.Cubical where
-
-open import Agda.Primitive
-open import Data.Bool
-open import Data.Product
-open import Data.Sum
-open import Data.Unit
-open import Data.Empty
-open import Data.Product
-
-open import Cat.Category
-open import Cat.Functor
-
-- 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 CwF {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-  open Category
-  open Functor
-  open import Function
-  open import Cubical
-
-  module _ {ℓa ℓb : Level} where
-    private
-      Obj = Σ[ A ∈ Set ℓa ] (A → Set ℓb)
-      Arr : Obj → Obj → Set (ℓa ⊔ ℓb)
-      Arr (A , B) (A' , B') = Σ[ f ∈ (A → A') ] ({x : A} → B x → B' (f x))
-      one : {o : Obj} → Arr o o
-      proj₁ one = λ x → x
-      proj₂ one = λ b → b
-      _:⊕:_ : {a b c : Obj} → Arr b c → Arr a b → Arr a c
-      (g , g') :⊕: (f , f') = g ∘ f , g' ∘ f'
-
-      module _ {A B C D : Obj} {f : Arr A B} {g : Arr B C} {h : Arr C D} where
-        :assoc: : (_:⊕:_ {A} {C} {D} h (_:⊕:_ {A} {B} {C} g f)) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} h g) f)
-        :assoc: = {!!}
-
-      module _ {A B : Obj} {f : Arr A B} where
-        :ident: : (_:⊕:_ {A} {A} {B} f one) ≡ f × (_:⊕:_ {A} {B} {B} one f) ≡ f
-        :ident: = {!!}
-
-      instance
-        :isCategory: : IsCategory Obj Arr one (λ {a b c} → _:⊕:_ {a} {b} {c})
-        :isCategory: = record
-          { assoc = λ {A} {B} {C} {D} {f} {g} {h} → :assoc: {A} {B} {C} {D} {f} {g} {h}
-          ; ident = {!!}
-          }
-    Fam : Category (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
-    Fam = record
-      { Object = Obj
-      ; Arrow = Arr
-      ; 𝟙 = one
-      ; _⊕_ = λ {a b c} → _:⊕:_ {a} {b} {c}
-      }
-
-  Contexts = ℂ .Object
-  Substitutions = ℂ .Arrow
-
-  record CwF : Set {!ℓa ⊔ ℓb!} where
-    field
-      Terms : Functor (Opposite ℂ) Fam
-
-module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
-  -- Ns is the "namespace"
-  ℓo = (lsuc lzero ⊔ ℓ)
-
-  FiniteDecidableSubset : Set ℓ
-  FiniteDecidableSubset = Ns → Bool
-
-  isTrue : Bool → Set
-  isTrue false = ⊥
-  isTrue true = ⊤
-
-  elmsof : (Ns → Bool) → Set ℓ
-  elmsof P = (σ : Ns) → isTrue (P σ)
-
-  𝟚 : Set
-  𝟚 = Bool
-
-  module _ (I J : FiniteDecidableSubset) where
-    private
-      themap : Set {!!}
-      themap = elmsof I → elmsof J ⊎ 𝟚
-      rules : (elmsof I → elmsof J ⊎ 𝟚) → Set
-      rules f = (i j : elmsof I) → {!!}
-
-    Mor = Σ themap rules
-
-  -- The category of names and substitutions
-  ℂ : Category ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
-  ℂ = record
-    -- { Object = FiniteDecidableSubset
-    { Object = Ns → Bool
-    ; Arrow = Mor
-    ; 𝟙 = {!!}
-    ; _⊕_ = {!!}
-    ; isCategory = {!!}
-    }
--- a/src/Cat/CwF.agda
+++ b/src/Cat/CwF.agda
@ -0,0 +1,55 @@
+module Cat.CwF where
+
+open import Agda.Primitive
+open import Data.Product
+
+open import Cat.Category
+open import Cat.Functor
+open import Cat.Categories.Fam
+
+open Category
+open Functor
+
+module _ {ℓa ℓb : Level} where
+  record CwF : Set (lsuc (ℓa ⊔ ℓb)) where
+    -- "A category with families consists of"
+    field
+      -- "A base category"
+      ℂ : Category ℓa ℓb
+    -- It's objects are called contexts
+    Contexts = ℂ .Object
+    -- It's arrows are called substitutions
+    Substitutions = ℂ .Arrow
+    field
+      -- A functor T
+      T : Functor (Opposite ℂ) (Fam ℓa ℓb)
+      -- Empty context
+      [] : Terminal ℂ
+    Type : (Γ : ℂ .Object) → Set ℓa
+    Type Γ = proj₁ (T .func* Γ)
+
+    module _ {Γ : ℂ .Object} {A : Type Γ} where
+
+      module _ {A B : ℂ .Object} {γ : ℂ [ A , B ]} where
+        k : Σ (proj₁ (func* T B) → proj₁ (func* T A))
+          (λ f →
+          {x : proj₁ (func* T B)} →
+          proj₂ (func* T B) x → proj₂ (func* T A) (f x))
+        k = T .func→ γ
+        k₁ : proj₁ (func* T B) → proj₁ (func* T A)
+        k₁ = proj₁ k
+        k₂ : ({x : proj₁ (func* T B)} →
+          proj₂ (func* T B) x → proj₂ (func* T A) (k₁ x))
+        k₂ = proj₂ k
+
+      record ContextComprehension : Set (ℓa ⊔ ℓb) where
+        field
+          Γ&A : ℂ .Object
+          proj1 : ℂ .Arrow Γ&A Γ
+          -- proj2 : ????
+
+        -- if γ : ℂ [ A , B ]
+        -- then T .func→ γ (written T[γ]) interpret substitutions in types and terms respectively.
+        -- field
+        --   ump : {Δ : ℂ .Object} → (γ : ℂ [ Δ , Γ ])
+        --     → (a : {!!}) → {!!}
--- a/src/Cat/Equality.agda
+++ b/src/Cat/Equality.agda
@ -0,0 +1,21 @@
+-- Defines equality-principles for data-types from the standard library.
+
+module Cat.Equality where
+
+open import Level
+open import Cubical
+
+-- _[_≡_] = PathP
+
+module Equality where
+  module Data where
+    module Product where
+      open import Data.Product
+
+      module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B}
+        (proj₁≡ : (λ _ → A)            [ proj₁ a ≡ proj₁ b ])
+        (proj₂≡ : (λ i → B (proj₁≡ i)) [ proj₂ a ≡ proj₂ b ]) where
+
+        Σ≡ : a ≡ b
+        proj₁ (Σ≡ i) = proj₁≡ i
+        proj₂ (Σ≡ i) = proj₂≡ i
--- a/src/Cat/Functor.agda
+++ b/src/Cat/Functor.agda
@ -6,36 +6,54 @@ open import Function

 open import Cat.Category

-record Functor {ℓc ℓc' ℓd ℓd'} (C : Category ℓc ℓc') (D : Category ℓd ℓd')
-  : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
-  open Category
-  field
-    func* : C .Object → D .Object
-    func→ : {dom cod : C .Object} → C .Arrow dom cod → D .Arrow (func* dom) (func* cod)
-    ident   : { c : C .Object } → func→ (C .𝟙 {c}) ≡ D .𝟙 {func* c}
-    -- TODO: Avoid use of ugly explicit arguments somehow.
-    -- This guy managed to do it:
-    --    https://github.com/copumpkin/categories/blob/master/Categories/Functor/Core.agda
-    distrib : { c c' c'' : C .Object} {a : C .Arrow c c'} {a' : C .Arrow c' c''}
-      → func→ (C ._⊕_ a' a) ≡ D ._⊕_ (func→ a') (func→ a)
+open Category hiding (_∘_)

+module _ {ℓc ℓc' ℓd ℓd'} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
+  record IsFunctor
+    (func* : Obj ℂ → Obj 𝔻)
+    (func→ : {A B : Obj ℂ} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ])
+      : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
+    field
+      ident   : {c : Obj ℂ} → func→ (ℂ .𝟙 {c}) ≡ 𝔻 .𝟙 {func* c}
+      -- TODO: Avoid use of ugly explicit arguments somehow.
+      -- This guy managed to do it:
+      --    https://github.com/copumpkin/categories/blob/master/Categories/Functor/Core.agda
+      distrib : {A B C : ℂ .Object} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
+        → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ]
+
+  record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
+    field
+      func* : ℂ .Object → 𝔻 .Object
+      func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
+      {{isFunctor}} : IsFunctor func* func→
+
+open IsFunctor
 open Functor
-open Category

 module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
-  private
-    _ℂ⊕_ = ℂ ._⊕_
+
+  IsFunctor≡
+    : {func* : ℂ .Object → 𝔻 .Object}
+      {func→ : {A B : ℂ .Object} → ℂ .Arrow A B → 𝔻 .Arrow (func* A) (func* B)}
+      {F G : IsFunctor ℂ 𝔻 func* func→}
+    → (eqI
+      : (λ i → ∀ {A} → func→ (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {func* A})
+        [ F .ident ≡ G .ident ])
+    → (eqD :
+        (λ i → ∀ {A B C} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
+          → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ])
+        [ F .distrib ≡ G .distrib ])
+    → (λ _ → IsFunctor ℂ 𝔻 (λ i → func* i) func→) [ F ≡ G ]
+  IsFunctor≡ eqI eqD i = record { ident = eqI i ; distrib = eqD i }
+
  Functor≡ : {F G : Functor ℂ 𝔻}
    → (eq* : F .func* ≡ G .func*)
-    → (eq→ : PathP (λ i → ∀ {x y} → ℂ .Arrow x y → 𝔻 .Arrow (eq* i x) (eq* i y))
-      (F .func→) (G .func→))
-    → (eqI : PathP (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A})
-      (ident F) (ident G))
-    → (eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C}
-      → eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f))
-      (distrib F) (distrib G))
+    → (eq→ : (λ i → ∀ {x y} → ℂ [ x , y ] → 𝔻 [ eq* i x , eq* i y ])
+        [ F .func→ ≡ G .func→ ])
+    -- → (eqIsF : PathP (λ i → IsFunctor ℂ 𝔻 (eq* i) (eq→ i)) (F .isFunctor) (G .isFunctor))
+    → (eqIsFunctor : (λ i → IsFunctor ℂ 𝔻 (eq* i) (eq→ i)) [ F .isFunctor ≡ G .isFunctor ])
    → F ≡ G
-  Functor≡ eq* eq→ eqI eqD i = record { func* = eq* i ; func→ = eq→ i ; ident = eqI i ; distrib = eqD i }
+  Functor≡ eq* eq→ eqIsFunctor i = record { func* = eq* i ; func→ = eq→ i ; isFunctor = eqIsFunctor i }

 module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
  private
@ -43,29 +61,28 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
    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
+    module _ {a0 a1 a2 : A .Object} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where

-      dist : (F→ ∘ G→) (α1 A⊕ α0) ≡ (F→ ∘ G→) α1 C⊕ (F→ ∘ G→) α0
+      dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (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→) (A [ α1 ∘ α0 ])         ≡⟨ refl ⟩
+        F→ (G→ (A [ α1 ∘ α0 ]))           ≡⟨ cong F→ (G .isFunctor .distrib)⟩
+        F→ (B [ G→ α1 ∘ G→ α0 ])          ≡⟨ F .isFunctor .distrib ⟩
+        C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎

  _∘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 .𝟙             ∎
-      ; distrib = dist
+      ; isFunctor = record
+        { ident = begin
+          (F→ ∘ G→) (A .𝟙) ≡⟨ refl ⟩
+          F→ (G→ (A .𝟙))   ≡⟨ cong F→ (G .isFunctor .ident)⟩
+          F→ (B .𝟙)        ≡⟨ F .isFunctor .ident ⟩
+          C .𝟙             ∎
+        ; distrib = dist
+        }
      }

 -- The identity functor
@ -73,6 +90,8 @@ identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C
 identity = record
  { func* = λ x → x
  ; func→ = λ x → x
-  ; ident = refl
-  ; distrib = refl
+  ; isFunctor = record
+    { ident = refl
+    ; distrib = refl
+    }
  }