Merge branch 'dev'

2018-01-25 12:52:39 +01:00 · 2018-01-25 12:52:39 +01:00 · e501f8152b
parent be4949180b 812662bda3
commit e501f8152b
9 changed files with 607 additions and 159 deletions
--- a/proposal/macros.tex
+++ b/proposal/macros.tex
@ -5,6 +5,7 @@
 \newcommand{\defeq}{\coloneqq}
 \newcommand{\bN}{\mathbb{N}}
 \newcommand{\bC}{\mathbb{C}}
+\newcommand{\bX}{\mathbb{X}}
 \newcommand{\to}{\rightarrow}}
 \newcommand{\mto}{\mapsto}}
 \newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace}
--- a/src/Cat.agda
+++ b/src/Cat.agda
@ -1,12 +1,13 @@
 module Cat where

-import Cat.Categories.Sets
-import Cat.Categories.Cat
-import Cat.Categories.Rel
+import Cat.Cubical
+import Cat.Category
+import Cat.Functor
 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
+import Cat.Categories.Sets
+import Cat.Categories.Cat
+import Cat.Categories.Rel
+import Cat.Categories.Fun
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@ -22,27 +22,12 @@ 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
+module _ (ℓ ℓ' : Level) where
  private
    module _ {A B C D : Category ℓ ℓ'} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
+      private
        eq* : func* (h ∘f (g ∘f f)) ≡ func* ((h ∘f g) ∘f f)
        eq* = refl
        eq→ : PathP
@ -58,27 +43,46 @@ module _ {ℓ ℓ' : Level} where
        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 = {!!}

      assc : h ∘f (g ∘f f) ≡ (h ∘f g) ∘f f
-      assc = lift-eq-functors eq* eq→ eqI eqD
+      assc = Functor≡ eq* eq→ eqI eqD

-    module _ {A B : Category ℓ ℓ'} {f : Functor A B} where
-      lem : (func* f) ∘ (func* (identity {C = A})) ≡ func* f
-      lem = refl
+    module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where
+      module _ where
+        private
+          eq* : (func* F) ∘ (func* (identity {C = ℂ})) ≡ func* F
+          eq* = refl
          -- lemmm : func→ {C = A} {D = B} (f ∘f identity) ≡ func→ f
-      lemmm : PathP
+          eq→ : 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!} {!!}
+            {x y : Object ℂ} → Arrow ℂ x y → Arrow 𝔻 (func* F x) (func* F y))
+            (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)
+            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)
+        ident-r : F ∘f identity ≡ F
+        ident-r = Functor≡ eq* eq→ eqI-r eqD-r
+      module _ where
+        private
+          postulate
+            eq* : (identity ∘f F) .func* ≡ F .func*
+            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)
+            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)
+        ident-l : identity ∘f F ≡ F
+        ident-l = Functor≡ eq* eq→ eqI eqD

  Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
  Cat =
@ -94,19 +98,22 @@ module _ {ℓ ℓ' : Level} where
        }
      }

-module _ {ℓ : Level} (C D : Category ℓ ℓ) where
+module _ {ℓ ℓ' : Level} where
+  Catt = Cat ℓ ℓ'
+
+  module _ (ℂ 𝔻 : 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'
+      :Object: = ℂ .Object × 𝔻 .Object
+      :Arrow:  : :Object: → :Object: → Set ℓ'
+      :Arrow: (c , d) (c' , d') = Arrow ℂ c c' × Arrow 𝔻 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}
+      _:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → (ℂ ._⊕_) bc∈C ab∈C , 𝔻 ._⊕_ bc∈D ab∈D}

      instance
        :isCategory: : IsCategory :Object: :Arrow: :𝟙: _:⊕:_
@ -117,10 +124,10 @@ module _ {ℓ : Level} (C D : Category ℓ ℓ) where
          , eqpair (snd C.ident) (snd D.ident)
          }
          where
-          open module C = IsCategory (C .isCategory)
-          open module D = IsCategory (D .isCategory)
+            open module C = IsCategory (ℂ .isCategory)
+            open module D = IsCategory (𝔻 .isCategory)

-    :product: : Category ℓ ℓ
+      :product: : Category ℓ ℓ'
      :product: = record
        { Object = :Object:
        ; Arrow = :Arrow:
@ -128,13 +135,13 @@ module _ {ℓ : Level} (C D : Category ℓ ℓ) where
        ; _⊕_ = _:⊕:_
        }

-    proj₁ : Arrow Cat :product: C
+      proj₁ : Arrow Catt :product: ℂ
      proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl }

-    proj₂ : Arrow Cat :product: D
+      proj₂ : Arrow Catt :product: 𝔻
      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
+      module _ {X : Object Catt} (x₁ : Arrow Catt X ℂ) (x₂ : Arrow Catt X 𝔻) where
        open Functor

        -- ident' : {c : Object X} → ((func→ x₁) {dom = c} (𝟙 X) , (func→ x₂) {dom = c} (𝟙 X)) ≡ 𝟙 (catProduct C D)
@ -150,25 +157,194 @@ module _ {ℓ : Level} (C D : Category ℓ ℓ) where

        -- 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 isUniqL : (Catt ⊕ proj₁) x ≡ x₁
+        -- isUniqL = Functor≡ refl refl {!!} {!!}

-      postulate isUniqR : (Cat ⊕ proj₂) x ≡ x₂
-      -- isUniqR = lift-eq-functors refl refl {!!} {!!}
+        postulate isUniqR : (Catt ⊕ proj₂) x ≡ x₂
+        -- isUniqR = Functor≡ refl refl {!!} {!!}

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

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

    instance
-      isProduct : IsProduct Cat proj₁ proj₂
+      isProduct : IsProduct (Cat ℓ ℓ') proj₁ proj₂
      isProduct = uniq

-  product : Product {ℂ = Cat} C D
+    product : Product {ℂ = (Cat ℓ ℓ')} ℂ 𝔻
    product = record
      { obj = :product:
      ; proj₁ = proj₁
      ; proj₂ = proj₂
      }
+
+module _ {ℓ ℓ' : Level} where
+  instance
+    hasProducts : HasProducts (Cat ℓ ℓ')
+    hasProducts = record { product = product }
+
+-- Basically proves that `Cat ℓ ℓ` is cartesian closed.
+module _ (ℓ : Level) where
+  private
+    open Data.Product
+    open import Cat.Categories.Fun
+
+    Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ)
+    Catℓ = Cat ℓ ℓ
+    module _ (ℂ 𝔻 : Category ℓ ℓ) where
+      private
+        _𝔻⊕_ = 𝔻 ._⊕_
+        _ℂ⊕_ = ℂ ._⊕_
+
+        :obj: : Cat ℓ ℓ .Object
+        :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻}
+
+        :func*: : Functor ℂ 𝔻 × ℂ .Object → 𝔻 .Object
+        :func*: (F , A) = F .func* A
+
+      module _ {dom cod : Functor ℂ 𝔻 × ℂ .Object} where
+        private
+          F : Functor ℂ 𝔻
+          F = proj₁ dom
+          A : ℂ .Object
+          A = proj₂ dom
+
+          G : Functor ℂ 𝔻
+          G = proj₁ cod
+          B : ℂ .Object
+          B = proj₂ cod
+
+        :func→: : (pobj : NaturalTransformation F G × ℂ .Arrow A B)
+          → 𝔻 .Arrow (F .func* A) (G .func* B)
+        :func→: ((θ , θNat) , f) = result
+          where
+            θA : 𝔻 .Arrow (F .func* A) (G .func* A)
+            θA = θ A
+            θB : 𝔻 .Arrow (F .func* B) (G .func* B)
+            θB = θ B
+            F→f : 𝔻 .Arrow (F .func* A) (F .func* B)
+            F→f = F .func→ f
+            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
+            r : 𝔻 .Arrow (F .func* A) (G .func* B)
+            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 = θNat f
+            result : 𝔻 .Arrow (F .func* A) (G .func* B)
+            result = l
+
+      _×p_ = product
+
+      module _ {c : Functor ℂ 𝔻 × ℂ .Object} where
+        private
+          F : Functor ℂ 𝔻
+          F = proj₁ c
+          C : ℂ .Object
+          C = proj₂ c
+
+        -- NaturalTransformation F G × ℂ .Arrow A B
+        -- :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 ⟩
+          𝔻 .𝟙 ∎
+          where
+            open module 𝔻 = IsCategory (𝔻 .isCategory)
+      module _ {F×A G×B H×C : Functor ℂ 𝔻 × ℂ .Object} where
+        F = F×A .proj₁
+        A = F×A .proj₂
+        G = G×B .proj₁
+        B = G×B .proj₂
+        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}
+        module _
+          -- NaturalTransformation F G × ℂ .Arrow A B
+          {θ×f : NaturalTransformation F G × ℂ .Arrow A B}
+          {η×g : NaturalTransformation G H × ℂ .Arrow B C} where
+          private
+            θ : Transformation F G
+            θ = proj₁ (proj₁ θ×f)
+            θNat : Natural F G θ
+            θNat = proj₂ (proj₁ θ×f)
+            f : ℂ .Arrow A B
+            f = proj₂ θ×f
+            η : Transformation G H
+            η = proj₁ (proj₁ η×g)
+            ηNat : Natural G H η
+            ηNat = proj₂ (proj₁ η×g)
+            g : ℂ .Arrow B C
+            g = proj₂ η×g
+
+            ηθNT : NaturalTransformation F H
+            ηθNT = Fun ._⊕_ {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)
+          :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) ∎
+            where
+              open IsCategory (𝔻 .isCategory)
+
+      :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}
+        }
+
+      module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where
+        open HasProducts (hasProducts {ℓ} {ℓ}) using (parallelProduct)
+
+        postulate
+          transpose : Functor 𝔸 :obj:
+          eq : Catℓ ._⊕_ :eval: (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ≡ F
+
+        catTranspose : ∃![ F~ ] (Catℓ ._⊕_ :eval: (parallelProduct F~ (Catℓ .𝟙 {o = ℂ})) ≡ F)
+        catTranspose = transpose , eq
+
+      :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
+      :isExponential: = catTranspose
+
+      -- :exponent: : Exponential (Cat ℓ ℓ) A B
+      :exponent: : Exponential Catℓ ℂ 𝔻
+      :exponent: = record
+        { obj = :obj:
+        ; eval = :eval:
+        ; isExponential = :isExponential:
+        }
+
+  hasExponentials : HasExponentials (Cat ℓ ℓ)
+  hasExponentials = record { exponent = :exponent: }
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@ -0,0 +1,116 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module Cat.Categories.Fun where
+
+open import Agda.Primitive
+open import Cubical
+open import Function
+open import Data.Product
+
+open import Cat.Category
+open import Cat.Functor
+
+module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
+  open Category
+  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)
+
+    Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
+    Natural θ
+      = {A B : ℂ .Object}
+      → (f : ℂ .Arrow A B)
+      → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A)
+
+    NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
+    NaturalTransformation = Σ Transformation Natural
+
+    -- NaturalTranformation : Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
+    -- NaturalTranformation = ∀ (θ : Transformation) {A B : ℂ .Object} → (f : ℂ .Arrow A B) → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A)
+
+  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     ∎
+    where
+      _𝔻⊕_ = 𝔻 ._⊕_
+      F→ = F .func→
+      open 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
+
+    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)) ∎
+      where
+        open IsCategory (𝔻 .isCategory)
+    NatComp = _:⊕:_
+
+  private
+    module _ {A B C D : Functor ℂ 𝔻} {f : NaturalTransformation A B}
+      {g : NaturalTransformation B C} {h : NaturalTransformation C D} where
+      _g⊕f_ = _:⊕:_ {A} {B} {C}
+      _h⊕g_ = _:⊕:_ {B} {C} {D}
+      :assoc: : (_:⊕:_ {A} {C} {D} h (_:⊕:_ {A} {B} {C} g f)) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} h g) f)
+      :assoc: = {!!}
+    module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
+      ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
+      ident-r = {!!}
+      ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
+      ident-l = {!!}
+      :ident:
+        : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
+        × (_:⊕:_ {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
+    { Object = Functor ℂ 𝔻
+    ; Arrow = NaturalTransformation
+    ; 𝟙 = λ {F} → identityNat F
+    ; _⊕_ = λ {F G H} → _:⊕:_ {F} {G} {H}
+    }
+
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
+  open import Cat.Categories.Sets
+
+  -- Restrict the functors to Presheafs.
+  Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
+  Presh = record
+    { Object = Presheaf ℂ
+    ; Arrow = NaturalTransformation
+    ; 𝟙 = λ {F} → identityNat F
+    ; _⊕_ = λ {F G H} → NatComp {F = F} {G = G} {H = H}
+    }
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@ -1,5 +1,3 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-
 module Cat.Categories.Sets where

 open import Cubical.PathPrelude
@ -11,8 +9,9 @@ open import Cat.Category
 open import Cat.Functor
 open Category

-Sets : {ℓ : Level} → Category (lsuc ℓ) ℓ
-Sets {ℓ} = record
+module _ {ℓ : Level} where
+  Sets : Category (lsuc ℓ) ℓ
+  Sets = record
    { Object = Set ℓ
    ; Arrow = λ T U → T → U
    ; 𝟙 = id
@ -22,6 +21,26 @@ Sets {ℓ} = record
    where
      open import Function

+  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
+      proj₁ lem = refl
+      proj₂ lem = refl
+    instance
+      isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} fst snd
+      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 }
+
+  instance
+    SetsHasProducts : HasProducts Sets
+    SetsHasProducts = record { product = product }
+
 -- Covariant Presheaf
 Representable : {ℓ ℓ' : Level} → (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
 Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@ -89,6 +89,26 @@ record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : ℂ .Object)
    proj₂ : ℂ .Arrow obj B
    {{isProduct}} : IsProduct ℂ proj₁ proj₂

+  arrowProduct : ∀ {X} → (π₁ : Arrow ℂ X A) (π₂ : Arrow ℂ X B)
+    → Arrow ℂ X obj
+  arrowProduct π₁ π₂ = fst (isProduct π₁ π₂)
+
+record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
+  field
+    product : ∀ (A B : ℂ .Object) → Product {ℂ = ℂ} A B
+
+  open Product
+
+  objectProduct : (A B : ℂ .Object) → ℂ .Object
+  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} {A' = A'} {B = B} {B' = B'} a b = arrowProduct (product A' B')
+    (ℂ ._⊕_ a ((product A B) .proj₁))
+    (ℂ ._⊕_ b ((product A B) .proj₂))
+
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
  Opposite : Category ℓ ℓ'
  Opposite =
@ -120,3 +140,37 @@ 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 = 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)
+
+    record Exponential : Set (ℓ ⊔ ℓ') where
+      field
+        -- obj ≡ Cᴮ
+        obj : ℂ .Object
+        eval : ℂ .Arrow ( 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 f = fst (isExponential A f)
+
+record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where
+  field
+    exponent : (A B : ℂ .Object) → Exponential ℂ A B
+
+record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
+  field
+    {{hasProducts}}     : HasProducts ℂ
+    {{hasExponentials}} : HasExponentials ℂ
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --allow-unsolved-metas --cubical #-}

 module Cat.Category.Properties where

@ -48,18 +48,37 @@ epi-mono-is-not-iso f =
  in {!!}
 -}

+module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
+  open import Cat.Category
+  open Category
+  open import Cat.Categories.Cat using (Cat)
+  module Cat = Cat.Categories.Cat
+  open Exponential
+  private
+    Catℓ = Cat ℓ ℓ
+    CatHasExponentials : HasExponentials Catℓ
+    CatHasExponentials = Cat.hasExponentials ℓ

-module _ {ℓa ℓa' ℓb ℓb'} where
-  Exponential : Category ℓa ℓa' → Category ℓb ℓb' → Category {!!} {!!}
-  Exponential A B = record
-    { Object = {!!}
-    ; Arrow = {!!}
-    ; 𝟙 = {!!}
-    ; _⊕_ = {!!}
-    ; isCategory = {!!}
+  -- Exp : Set (lsuc (lsuc ℓ))
+  -- Exp = Exponential (Cat (lsuc ℓ) ℓ)
+  --   Sets (Opposite ℂ)
+
+  _⇑_ : (A B : Catℓ .Object) → Catℓ .Object
+  A ⇑ B = (exponent A B) .obj
+    where
+      open HasExponentials CatHasExponentials
+
+  private
+    -- I need `Sets` to be a `Category ℓ ℓ` but it simlpy isn't.
+    Setz : Category ℓ ℓ
+    Setz = {!Sets!}
+    :func*: : ℂ .Object → (Setz ⇑ Opposite ℂ) .Object
+    :func*: A = {!!}
+
+  yoneda : Functor ℂ (Setz ⇑ (Opposite ℂ))
+  yoneda = record
+    { func* = :func*:
+    ; func→ = {!!}
+    ; ident = {!!}
+    ; distrib = {!!}
    }
-
-_⇑_ = Exponential
-
-yoneda : ∀ {ℓ ℓ'} → {ℂ : Category ℓ ℓ'} → Functor ℂ (Sets ⇑ (Opposite ℂ))
-yoneda = {!!}
--- a/src/Cat/Cubical.agda
+++ b/src/Cat/Cubical.agda
@ -7,14 +7,62 @@ 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 ⊔ ℓ)
@ -49,5 +97,5 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
    ; Arrow = Mor
    ; 𝟙 = {!!}
    ; _⊕_ = {!!}
-    ; isCategory = ?
+    ; isCategory = {!!}
    }
--- a/src/Cat/Functor.agda
+++ b/src/Cat/Functor.agda
@ -8,22 +8,36 @@ open import Cat.Category

 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
-    open module D = Category D
+  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}
+    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→ (a' C.⊕ a) ≡ func→ a' D.⊕ func→ a
+    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 Functor
+open Category
+
+module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
+  private
+    _ℂ⊕_ = ℂ ._⊕_
+  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))
+    → F ≡ G
+  Functor≡ eq* eq→ eqI eqD i = record { func* = eq* i ; func→ = eq→ i ; ident = eqI i ; distrib = eqD i }

 module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
-  open Functor
-  open Category
  private
    F* = F .func*
    F→ = F .func→