Merge branch 'dev'

2018-02-06 14:31:28 +01:00 · 2018-02-06 14:31:28 +01:00 · 4df4231906
parent 36d10b0556 9349b37550
commit 4df4231906
17 changed files with 615 additions and 441 deletions
--- a/src/Cat.agda
+++ b/src/Cat.agda
@ -1,14 +1,19 @@
 module Cat where

 import Cat.Category
-import Cat.Functor
 import Cat.CwF
+
+import Cat.Category.Functor
+import Cat.Category.Product
+import Cat.Category.Exponential
+import Cat.Category.CartesianClosed
 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.Rel
+import Cat.Categories.Free
 import Cat.Categories.Fun
 import Cat.Categories.Cube
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@ -9,7 +9,9 @@ open import Function
 open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)

 open import Cat.Category
-open import Cat.Functor
+open import Cat.Category.Functor
+open import Cat.Category.Product
+open import Cat.Category.Exponential

 open import Cat.Equality
 open Equality.Data.Product
@ -26,12 +28,12 @@ module _ (ℓ ℓ' : Level) where
        eq* : func* (H ∘f (G ∘f F)) ≡ func* ((H ∘f G) ∘f F)
        eq* = refl
        eq→ : PathP
-          (λ i → {A B : 𝔸 .Object} → 𝔸 [ A , B ] → 𝔻 [ eq* i A , eq* i B ])
+          (λ 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
-            : (λ i → ∀ {A : 𝔸 .Object} → eq→ i (𝔸 .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A})
+            : (λ i → ∀ {A : Object 𝔸} → eq→ i (𝟙 𝔸 {A}) ≡ 𝟙 𝔻 {eq* i A})
            [ (H ∘f (G ∘f F)) .isFunctor .ident
            ≡ ((H ∘f G) ∘f F) .isFunctor .ident
            ]
@ -58,12 +60,12 @@ module _ (ℓ ℓ' : Level) where
          eq→ = refl
          postulate
            eqI-r
-              : (λ i → {c : ℂ .Object} → (λ _ → 𝔻 [ func* F c , func* F c ])
-                [ func→ F (ℂ .𝟙) ≡ 𝔻 .𝟙 ])
+              : (λ 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} →
+                        {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} →
                        eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
                        ((F ∘f identity) .isFunctor .distrib) (F .isFunctor .distrib)
        ident-r : F ∘f identity ≡ F
@ -73,40 +75,50 @@ module _ (ℓ ℓ' : Level) where
          postulate
            eq* : (identity ∘f F) .func* ≡ F .func*
            eq→ : PathP
-              (λ i → {x y : Object ℂ} → ℂ .Arrow x y → 𝔻 .Arrow (eq* i x) (eq* i y))
+              (λ i → {x y : Object ℂ} → ℂ [ x , y ] → 𝔻 [ eq* i x , eq* i y ])
              ((identity ∘f F) .func→) (F .func→)
-            eqI : (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A})
+            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}
+            eqD : PathP (λ i → {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
                 → 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→ λ i → record { ident = eqI i ; distrib = eqD i }

-  Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
-  Cat =
-    record
-      { Object = Category ℓ ℓ'
-      ; Arrow = Functor
-      ; 𝟙 = identity
-      ; _∘_ = _∘f_
-      -- What gives here? Why can I not name the variables directly?
-      ; isCategory = record
-        { assoc = λ {_ _ _ _ F G H} → assc {F = F} {G = G} {H = H}
-        ; ident = ident-r , ident-l
+    RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
+    RawCat =
+      record
+        { Object = Category ℓ ℓ'
+        ; Arrow = Functor
+        ; 𝟙 = identity
+        ; _∘_ = _∘f_
+        -- What gives here? Why can I not name the variables directly?
+        -- ; isCategory = record
+        --   { assoc = λ {_ _ _ _ F G H} → assc {F = F} {G = G} {H = H}
+        --   ; ident = ident-r , ident-l
+        --   }
        }
-      }
+    open IsCategory
+    instance
+      :isCategory: : IsCategory RawCat
+      assoc :isCategory: {f = F} {G} {H} = assc {F = F} {G = G} {H = H}
+      ident :isCategory: = ident-r , ident-l
+      arrow-is-set :isCategory: = {!!}
+      univalent :isCategory: = {!!}
+
+  Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
+  raw Cat = RawCat

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

+      :rawProduct: : RawCategory ℓ ℓ'
+      RawCategory.Object :rawProduct: = :Object:
+      RawCategory.Arrow :rawProduct: = :Arrow:
+      RawCategory.𝟙 :rawProduct: = :𝟙:
+      RawCategory._∘_ :rawProduct: = _:⊕:_
+
+      module C = IsCategory (ℂ .isCategory)
+      module D = IsCategory (𝔻 .isCategory)
+      postulate
+        issSet : {A B : RawCategory.Object :rawProduct:} → isSet (RawCategory.Arrow :rawProduct: A B)
      instance
-        :isCategory: : IsCategory :Object: :Arrow: :𝟙: _:⊕:_
-        :isCategory: = record
-          { assoc = Σ≡ C.assoc D.assoc
-          ; ident
+        :isCategory: : IsCategory :rawProduct:
+        -- :isCategory: = record
+        --   { assoc = Σ≡ C.assoc D.assoc
+        --   ; ident
+        --     = Σ≡ (fst C.ident) (fst D.ident)
+        --     , Σ≡ (snd C.ident) (snd D.ident)
+        --   ; arrow-is-set = issSet
+        --   ; univalent = {!!}
+        --   }
+        IsCategory.assoc :isCategory: = Σ≡ C.assoc D.assoc
+        IsCategory.ident :isCategory:
          = Σ≡ (fst C.ident) (fst D.ident)
          , Σ≡ (snd C.ident) (snd D.ident)
-          }
-          where
-            open module C = IsCategory (ℂ .isCategory)
-            open module D = IsCategory (𝔻 .isCategory)
+        IsCategory.arrow-is-set :isCategory: = issSet
+        IsCategory.univalent :isCategory: = {!!}

      :product: : Category ℓ ℓ'
-      :product: = record
-        { Object = :Object:
-        ; Arrow = :Arrow:
-        ; 𝟙 = :𝟙:
-        ; _∘_ = _:⊕:_
-        }
+      raw :product: = :rawProduct:

      proj₁ : Catt [ :product: , ℂ ]
      proj₁ = record { func* = fst ; func→ = fst ; isFunctor = record { ident = refl ; distrib = refl } }
@ -143,28 +165,32 @@ module _ {ℓ ℓ' : Level} where
      module _ {X : Object Catt} (x₁ : Catt [ X , ℂ ]) (x₂ : Catt [ X , 𝔻 ]) where
        open Functor

-        x : Functor X :product:
-        x = record
-          { func* = λ x → x₁ .func* x , x₂ .func* x
-          ; func→ = λ x → func→ x₁ x , func→ x₂ 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)
+        postulate x : Functor X :product:
+        -- x = record
+        --   { func* = λ x → x₁ .func* x , x₂ .func* x
+        --   ; func→ = λ x → func→ x₁ x , func→ x₂ 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)

-        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
+        -- Turned into postulate after:
+        -- > commit e8215b2c051062c6301abc9b3f6ec67106259758 (HEAD -> dev, github/dev)
+        -- > Author: Frederik Hanghøj Iversen <fhi.1990@gmail.com>
+        -- > Date:   Mon Feb 5 14:59:53 2018 +0100
+        postulate isUniqL : Catt [ proj₁ ∘ x ] ≡ x₁
+        -- isUniqL = Functor≡ eq* eq→ {!!}
+        --   where
+        --     eq* : (Catt [ proj₁ ∘ x ]) .func* ≡ x₁ .func*
+        --     eq* = {!refl!}
+        --     eq→ : (λ i → {A : Object X} {B : Object X} → 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₂
@ -202,55 +228,55 @@ module _ (ℓ : Level) where
    Catℓ = Cat ℓ ℓ
    module _ (ℂ 𝔻 : Category ℓ ℓ) where
      private
-        :obj: : Cat ℓ ℓ .Object
+        :obj: : Object (Cat ℓ ℓ)
        :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻}

-        :func*: : Functor ℂ 𝔻 × ℂ .Object → 𝔻 .Object
+        :func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻
        :func*: (F , A) = F .func* A

-      module _ {dom cod : Functor ℂ 𝔻 × ℂ .Object} where
+      module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where
        private
          F : Functor ℂ 𝔻
          F = proj₁ dom
-          A : ℂ .Object
+          A : Object ℂ
          A = proj₂ dom

          G : Functor ℂ 𝔻
          G = proj₁ cod
-          B : ℂ .Object
+          B : Object ℂ
          B = proj₂ cod

-        :func→: : (pobj : NaturalTransformation F G × ℂ .Arrow A B)
-          → 𝔻 .Arrow (F .func* A) (G .func* B)
+        :func→: : (pobj : NaturalTransformation F G × ℂ [ A , B ])
+          → 𝔻 [ F .func* A , G .func* B ]
        :func→: ((θ , θNat) , f) = result
          where
-            θA : 𝔻 .Arrow (F .func* A) (G .func* A)
+            θA : 𝔻 [ F .func* A , G .func* A ]
            θA = θ A
-            θB : 𝔻 .Arrow (F .func* B) (G .func* B)
+            θB : 𝔻 [ F .func* B , G .func* B ]
            θB = θ B
-            F→f : 𝔻 .Arrow (F .func* A) (F .func* B)
+            F→f : 𝔻 [ F .func* A , F .func* B ]
            F→f = F .func→ f
-            G→f : 𝔻 .Arrow (G .func* A) (G .func* B)
+            G→f : 𝔻 [ G .func* A , G .func* B ]
            G→f = G .func→ f
-            l : 𝔻 .Arrow (F .func* A) (G .func* B)
+            l : 𝔻 [ F .func* A , G .func* B ]
            l = 𝔻 [ θB ∘ F→f ]
-            r : 𝔻 .Arrow (F .func* A) (G .func* B)
+            r : 𝔻 [ 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 : 𝔻 [ F .func* A , G .func* B ]
            result = l

      _×p_ = product

-      module _ {c : Functor ℂ 𝔻 × ℂ .Object} where
+      module _ {c : Functor ℂ 𝔻 × Object ℂ} where
        private
          F : Functor ℂ 𝔻
          F = proj₁ c
-          C : ℂ .Object
+          C : Object ℂ
          C = proj₂ c

        -- NaturalTransformation F G × ℂ .Arrow A B
@ -259,19 +285,19 @@ module _ (ℓ : Level) where
        --   where
        --     open module 𝔻 = IsCategory (𝔻 .isCategory)
        -- Unfortunately the equational version has some ambigous arguments.
-        :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙 {o = proj₂ c}) ≡ 𝔻 .𝟙
+        :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 ⟩
-          𝔻 .𝟙                                               ∎
+          :func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩
+          :func→: {c} {c} (identityNat F , 𝟙 ℂ)             ≡⟨⟩
+          𝔻 [ 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
+      module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where
        F = F×A .proj₁
        A = F×A .proj₂
        G = G×B .proj₁
@ -279,27 +305,27 @@ 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 .Category._∘_ {F×A} {G×B} {H×C}
+        _P⊕_ = Category._∘_ (Product.obj (:obj: ×p ℂ)) {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
+          {θ×f : NaturalTransformation F G × ℂ [ A , B ]}
+          {η×g : NaturalTransformation G H × ℂ [ B , C ]} where
          private
            θ : Transformation F G
            θ = proj₁ (proj₁ θ×f)
            θNat : Natural F G θ
            θNat = proj₂ (proj₁ θ×f)
-            f : ℂ .Arrow A B
+            f : ℂ [ A , B ]
            f = proj₂ θ×f
            η : Transformation G H
            η = proj₁ (proj₁ η×g)
            ηNat : Natural G H η
            ηNat = proj₂ (proj₁ η×g)
-            g : ℂ .Arrow B C
+            g : ℂ [ B , C ]
            g = proj₂ η×g

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

            ηθ = proj₁ ηθNT
            ηθNat = proj₂ ηθNT
@ -341,17 +367,28 @@ module _ (ℓ : Level) where
        }

      module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where
-        open HasProducts (hasProducts {ℓ} {ℓ}) using (parallelProduct)
+        open HasProducts (hasProducts {ℓ} {ℓ}) renaming (_|×|_ to parallelProduct)

        postulate
          transpose : Functor 𝔸 :obj:
-          eq : Catℓ [ :eval: ∘ (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ] ≡ F
+          eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F
+          -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F
+          -- eq' : (Catℓ [ :eval: ∘
+          --   (record { product = product } HasProducts.|×| transpose)
+          --   (𝟙 Catℓ)
+          --   ])
+          --   ≡ F

-        catTranspose : ∃![ F~ ] (Catℓ [ :eval: ∘ (parallelProduct F~ (Catℓ .𝟙 {o = ℂ}))] ≡ F )
-        catTranspose = transpose , eq
+        -- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758`
+        -- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [
+        -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose =
+        -- transpose , eq

      :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
-      :isExponential: = catTranspose
+      :isExponential: = {!catTranspose!}
+        where
+          open HasProducts (hasProducts {ℓ} {ℓ}) using (_|×|_)
+      -- :isExponential: = λ 𝔸 F → transpose 𝔸 F , eq' 𝔸 F

      -- :exponent: : Exponential (Cat ℓ ℓ) A B
      :exponent: : Exponential Catℓ ℂ 𝔻
--- a/src/Cat/Categories/Cube.agda
+++ b/src/Cat/Categories/Cube.agda
@ -13,7 +13,7 @@ open import Relation.Nullary
 open import Relation.Nullary.Decidable

 open import Cat.Category
-open import Cat.Functor
+open import Cat.Category.Functor
 open import Cat.Equality
 open Equality.Data.Product

@ -65,15 +65,16 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where

    Hom = Σ Hom' rules

+  module Raw = RawCategory
  -- 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ℂ
+  Raw.Object Rawℂ = FiniteDecidableSubset
+  Raw.Arrow Rawℂ = Hom
+  Raw.𝟙 Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} }
+  Raw._∘_ Rawℂ = {!!}
+
+  postulate IsCategoryℂ : IsCategory Rawℂ
+
  ℂ : Category ℓ ℓ
-  ℂ = Rawℂ , RawIsCategoryℂ
+  raw ℂ = Rawℂ
+  isCategory ℂ = IsCategoryℂ
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@ -46,9 +46,9 @@ module _ (ℓa ℓb : Level) where
      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 = ?
+        ; arrowIsSet = {!!}
+        ; univalent = {!!}
        }

  Fam : Category (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
-  Fam = RawFam , isCategory
+  Category.raw Fam = RawFam
--- a/src/Cat/Categories/Free.agda
+++ b/src/Cat/Categories/Free.agda
@ -0,0 +1,62 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module Cat.Categories.Free where
+
+open import Agda.Primitive
+open import Cubical hiding (Path ; isSet ; empty)
+open import Data.Product
+
+open import Cat.Category
+
+open IsCategory
+open Category
+
+-- data Path {ℓ : Level} {A : Set ℓ} : (a b : A) → Set ℓ where
+--   emptyPath : {a : A} → Path a a
+--   concatenate : {a b c : A} → Path a b → Path b c → Path a b
+
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
+  module ℂ = Category ℂ
+
+  -- import Data.List
+  -- P : (a b : Object ℂ) → Set (ℓ ⊔ ℓ')
+  -- P = {!Data.List.List ?!}
+  -- Generalized paths:
+  -- data P {ℓ : Level} {A : Set ℓ} (R : A → A → Set ℓ) : (a b : A) → Set ℓ where
+  --   e : {a : A} → P R a a
+  --   c : {a b c : A} → R a b → P R b c → P R a c
+
+  -- Path's are like lists with directions.
+  -- This implementation is specialized to categories.
+  data Path : (a b : Object ℂ) → Set (ℓ ⊔ ℓ') where
+    empty : {A : Object ℂ} → Path A A
+    cons : ∀ {A B C} → ℂ [ B , C ] → Path A B → Path A C
+
+  concatenate : ∀ {A B C : Object ℂ}  → Path B C → Path A B → Path A C
+  concatenate empty p = p
+  concatenate (cons x q) p = cons x (concatenate q p)
+
+  private
+    module _ {A B C D : Object ℂ} where
+      p-assoc : {r : Path A B} {q : Path B C} {p : Path C D} → concatenate p (concatenate q r) ≡ concatenate (concatenate p q) r
+      p-assoc {r} {q} {p} = {!!}
+    module _ {A B : Object ℂ} {p : Path A B} where
+      -- postulate
+      --   ident-r : concatenate {A} {A} {B} p (lift 𝟙) ≡ p
+      --   ident-l : concatenate {A} {B} {B} (lift 𝟙) p ≡ p
+    module _ {A B : Object ℂ} where
+      isSet : IsSet (Path A B)
+      isSet = {!!}
+  RawFree : RawCategory ℓ (ℓ ⊔ ℓ')
+  RawFree = record
+    { Object = Object ℂ
+    ; Arrow = Path
+    ; 𝟙 = λ {o} → {!lift 𝟙!}
+    ; _∘_ = λ {a b c} → {!concatenate {a} {b} {c}!}
+    }
+  RawIsCategoryFree : IsCategory RawFree
+  RawIsCategoryFree = record
+    { assoc = {!p-assoc!}
+    ; ident = {!ident-r , ident-l!}
+    ; arrowIsSet = {!!}
+    ; univalent = {!!}
+    }
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@ -7,22 +7,25 @@ open import Function
 open import Data.Product

 open import Cat.Category
-open import Cat.Functor
+open import Cat.Category.Functor

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

  module _ (F G : Functor ℂ 𝔻) where
+    private
+      module F = Functor F
+      module G = Functor G
    -- What do you call a non-natural tranformation?
    Transformation : Set (ℓc ⊔ ℓd')
-    Transformation = (C : ℂ .Object) → 𝔻 [ 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}
+      = {A B : Object ℂ}
      → (f : ℂ [ A , B ])
-      → 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
+      → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]

    NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
    NaturalTransformation = Σ Transformation Natural
@ -30,29 +33,29 @@ 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}
+    NaturalTransformation≡ : {α β : NaturalTransformation}
      → (eq₁ : α .proj₁ ≡ β .proj₁)
      → (eq₂ : PathP
-          (λ i → {A B : ℂ .Object} (f : ℂ [ A , B ])
-            → 𝔻 [ eq₁ i B ∘ F .func→ f ]
-            ≡ 𝔻 [ G .func→ f ∘ eq₁ i A ])
+          (λ 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 = 𝔻 .𝟙
+  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 ]              ≡⟨ proj₂ 𝔻.ident ⟩
    F→ f                            ≡⟨ sym (proj₁ 𝔻.ident) ⟩
-    𝔻 [ F→ f ∘ 𝔻 .𝟙 ]               ≡⟨⟩
+    𝔻 [ F→ f ∘ 𝟙 𝔻 ]               ≡⟨⟩
    𝔻 [ F→ f ∘ identityTrans F A ]  ∎
    where
-      F→ = F .func→
+      module F = Functor F
+      F→ = F.func→
      module 𝔻 = IsCategory (isCategory 𝔻)

  identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F
@ -60,20 +63,23 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat

  module _ {F G H : Functor ℂ 𝔻} where
    private
+      module F = Functor F
+      module G = Functor G
+      module H = Functor H
      _∘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 ]     ∎
+      𝔻 [ (θ ∘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 𝔻)

@ -110,12 +116,12 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
    :isCategory: = record
      { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D}
      ; ident = λ {A B} → :ident: {A} {B}
-      ; arrow-is-set = ?
-      ; univalent = ?
+      ; arrowIsSet = {!!}
+      ; univalent = {!!}
      }

  Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
-  Fun = RawFun , :isCategory:
+  raw Fun = RawFun

 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
  open import Cat.Categories.Sets
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@ -166,6 +166,6 @@ RawIsCategoryRel : IsCategory RawRel
 RawIsCategoryRel = record
  { assoc = funExt is-assoc
  ; ident = funExt ident-l , funExt ident-r
-  ; arrow-is-set = {!!}
+  ; arrowIsSet = {!!}
  ; univalent = {!!}
  }
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --allow-unsolved-metas --cubical #-}
 module Cat.Categories.Sets where

 open import Cubical
@ -7,28 +7,28 @@ open import Data.Product
 import Function

 open import Cat.Category
-open import Cat.Functor
+open import Cat.Category.Functor
+open import Cat.Category.Product
 open Category

 module _ {ℓ : Level} where
  SetsRaw : RawCategory (lsuc ℓ) ℓ
-  SetsRaw = record
-       { Object = Set ℓ
-       ; Arrow = λ T U → T → U
-       ; 𝟙 = Function.id
-       ; _∘_ = Function._∘′_
-       }
+  RawCategory.Object SetsRaw = Set ℓ
+  RawCategory.Arrow SetsRaw = λ T U → T → U
+  RawCategory.𝟙 SetsRaw = Function.id
+  RawCategory._∘_ SetsRaw = Function._∘′_

+  open IsCategory
  SetsIsCategory : IsCategory SetsRaw
-  SetsIsCategory = record
-    { assoc = refl
-    ; ident = funExt (λ _ → refl) , funExt (λ _ → refl)
-    ; arrow-is-set = {!!}
-    ; univalent = {!!}
-    }
+  assoc SetsIsCategory = refl
+  proj₁ (ident SetsIsCategory) = funExt λ _ → refl
+  proj₂ (ident SetsIsCategory) = funExt λ _ → refl
+  arrowIsSet SetsIsCategory = {!!}
+  univalent SetsIsCategory = {!!}

  Sets : Category (lsuc ℓ) ℓ
-  Sets = SetsRaw , SetsIsCategory
+  raw Sets = SetsRaw
+  isCategory Sets = SetsIsCategory

  private
    module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
@ -39,10 +39,10 @@ module _ {ℓ : Level} where
      proj₁ lem = refl
      proj₂ lem = refl
    instance
-      isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} proj₁ proj₂
+      isProduct : {A B : Object Sets} → 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 : Object Sets) → Product {ℂ = Sets} A B
    product A B = record { obj = A × B ; proj₁ = proj₁ ; proj₂ = proj₂ ; isProduct = isProduct }

  instance
@ -56,8 +56,10 @@ Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
 -- The "co-yoneda" embedding.
 representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
 representable {ℂ = ℂ} A = record
-  { func* = λ B → ℂ .Arrow A B
-  ; func→ = ℂ ._∘_
+  { raw = record
+    { func* = λ B → ℂ [ A , B ]
+    ; func→ = ℂ [_∘_]
+    }
  ; isFunctor = record
    { ident = funExt λ _ → proj₂ ident
    ; distrib = funExt λ x → sym assoc
@ -73,8 +75,10 @@ Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
 -- Alternate name: `yoneda`
 presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ
 presheaf {ℂ = ℂ} B = record
-  { func* = λ A → ℂ .Arrow A B
-  ; func→ = λ f g → ℂ ._∘_ g f
+  { raw = record
+    { func* = λ A → ℂ [ A , B ]
+    ; func→ = λ f g → ℂ [ g ∘ f ]
+  }
  ; isFunctor = record
    { ident = funExt λ x → proj₁ ident
    ; distrib = funExt λ x → assoc
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@ -11,7 +11,7 @@ open import Data.Product renaming
  )
 open import Data.Empty
 import Function
-open import Cubical
+open import Cubical hiding (isSet)
 open import Cubical.GradLemma using ( propIsEquiv )

 ∃! : ∀ {a b} {A : Set a}
@ -23,6 +23,9 @@ open import Cubical.GradLemma using ( propIsEquiv )

 syntax ∃!-syntax (λ x → B) = ∃![ x ] B

+IsSet   : {ℓ : Level} (A : Set ℓ) → Set ℓ
+IsSet A = {x y : A} → (p q : x ≡ y) → p ≡ q
+
 record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
  -- adding no-eta-equality can speed up type-checking.
  -- ONLY IF you define your categories with copatterns though.
@ -50,16 +53,12 @@ record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
 -- (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)
+    arrowIsSet : ∀ {A B : Object} → IsSet (Arrow A B)

  Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
  Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
@ -73,11 +72,12 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
  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.
+  Univalent : Set (ℓa ⊔ ℓb)
+  Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
  field
-    univalent : {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
+    univalent : Univalent

  module _ {A B : Object} where
    Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓb
@ -91,16 +91,15 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
  -- This lemma will be useful to prove the equality of two categories.
  IsCategory-is-prop : isProp (IsCategory ℂ)
  IsCategory-is-prop x y i = record
-    { assoc = x.arrow-is-set _ _ x.assoc y.assoc i
+    { assoc = x.arrowIsSet 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
+      ( x.arrowIsSet (fst x.ident) (fst y.ident) i
+      , x.arrowIsSet (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 →
+    ; arrowIsSet = λ p q →
      let
-        golden : x.arrow-is-set _ _ p q ≡ y.arrow-is-set _ _ p q
-        golden = λ j k l → {!!}
+        golden : x.arrowIsSet p q ≡ y.arrowIsSet p q
+        golden = {!!}
      in
        golden i
      ; univalent = λ y₁ → {!!}
@ -109,148 +108,91 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} 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 : Obj ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
-    → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ × ℂ [ π₂ ∘ x ] ≡ x₂)
-
-- Tip from Andrea; Consider this style for efficiency:
-- record IsProduct {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'})
--   {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) : Set (ℓ ⊔ ℓ') where
--   field
--      isProduct : ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B)
--        → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ. _⊕_ π₂ x ≡ x₂)
-
-record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Obj ℂ) : Set (ℓ ⊔ ℓ') where
-  no-eta-equality
+record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
  field
-    obj : Obj ℂ
-    proj₁ : ℂ [ obj , A ]
-    proj₂ : ℂ [ obj , B ]
-    {{isProduct}} : IsProduct ℂ proj₁ proj₂
+    raw : RawCategory ℓa ℓb
+    {{isCategory}} : IsCategory raw

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

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

-  open Product
+  Arrow = ℂ.Arrow
+
+  𝟙 = ℂ.𝟙
+
+  _∘_ = ℂ._∘_
+
+  _[_,_] : (A : Object) → (B : Object) → Set ℓb
+  _[_,_] = ℂ.Arrow
+
+  _[_∘_] : {A B C : Object} → (g : ℂ.Arrow B C) → (f : ℂ.Arrow A B) → ℂ.Arrow A C
+  _[_∘_] = ℂ._∘_

-  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' : 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₂ ])

 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 (ℂ._∘_)
-      }
+    RawCategory.Object OpRaw = Object
+    RawCategory.Arrow OpRaw = Function.flip Arrow
+    RawCategory.𝟙 OpRaw = 𝟙
+    RawCategory._∘_ OpRaw = Function.flip _∘_
+
    open IsCategory isCategory
+
    OpIsCategory : IsCategory OpRaw
-    OpIsCategory = record
-      { assoc = sym assoc
-      ; ident = swap ident
-      ; arrow-is-set = {!!}
-      ; univalent = {!!}
-      }
+    IsCategory.assoc OpIsCategory = sym assoc
+    IsCategory.ident OpIsCategory = swap ident
+    IsCategory.arrowIsSet OpIsCategory = arrowIsSet
+    IsCategory.univalent OpIsCategory = {!!}
+
  Opposite : Category ℓa ℓb
-  Opposite = OpRaw , OpIsCategory
+  raw Opposite = OpRaw
+  Category.isCategory Opposite = OpIsCategory

-- A consequence of no-eta-equality; `Opposite-is-involution` is no longer
-- definitional - i.e.; you must match on the fields:
--
-- Opposite-is-involution : ∀ {ℓ ℓ'} → {C : Category {ℓ} {ℓ'}} → Opposite (Opposite C) ≡ C
-- Object (Opposite-is-involution {C = C} i) = Object C
-- Arrow (Opposite-is-involution i) = {!!}
-- 𝟙 (Opposite-is-involution i) = {!!}
-- _⊕_ (Opposite-is-involution i) = {!!}
-- assoc (Opposite-is-involution i) = {!!}
-- ident (Opposite-is-involution i) = {!!}
-
-module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} where
-  open HasProducts hasProducts
-  open Product hiding (obj)
+-- As demonstrated here a side-effect of having no-eta-equality on constructors
+-- means that we need to pick things apart to show that things are indeed
+-- definitionally equal. I.e; a thing that would normally be provable in one
+-- line now takes more than 20!!
+module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
  private
-    _×p_ : (A B : Obj ℂ) → Obj ℂ
-    _×p_ A B = Product.obj (product A B)
+    open RawCategory
+    module C = Category ℂ
+    rawOp : Category.raw (Opposite (Opposite ℂ)) ≡ Category.raw ℂ
+    Object (rawOp _) = C.Object
+    Arrow (rawOp _) = C.Arrow
+    𝟙 (rawOp _) = C.𝟙
+    _∘_ (rawOp _) = C._∘_
+    open Category
+    open IsCategory
+    module IsCat = IsCategory (ℂ .isCategory)
+    rawIsCat : (i : I) → IsCategory (rawOp i)
+    assoc (rawIsCat i) = IsCat.assoc
+    ident (rawIsCat i) = IsCat.ident
+    arrowIsSet (rawIsCat i) = IsCat.arrowIsSet
+    univalent (rawIsCat i) = IsCat.univalent

-  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 : 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 : 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 : Obj ℂ) → Exponential ℂ A B
-
-record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
-  field
-    {{hasProducts}}     : HasProducts ℂ
-    {{hasExponentials}} : HasExponentials ℂ
+  Opposite-is-involution : Opposite (Opposite ℂ) ≡ ℂ
+  raw (Opposite-is-involution i) = rawOp i
+  isCategory (Opposite-is-involution i) = rawIsCat i

 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  open Category
  unique = isContr

-  IsInitial : Obj ℂ → Set (ℓa ⊔ ℓb)
-  IsInitial I = {X : Obj ℂ} → unique (ℂ [ I , X ])
+  IsInitial : Object ℂ → Set (ℓa ⊔ ℓb)
+  IsInitial I = {X : Object ℂ} → unique (ℂ [ I , X ])

-  IsTerminal : Obj ℂ → Set (ℓa ⊔ ℓb)
+  IsTerminal : Object ℂ → Set (ℓa ⊔ ℓb)
  -- ∃![ ? ] ?
-  IsTerminal T = {X : Obj ℂ} → unique (ℂ [ X , T ])
+  IsTerminal T = {X : Object ℂ} → unique (ℂ [ X , T ])

  Initial : Set (ℓa ⊔ ℓb)
-  Initial = Σ (Obj ℂ) IsInitial
+  Initial = Σ (Object ℂ) IsInitial

  Terminal : Set (ℓa ⊔ ℓb)
-  Terminal = Σ (Obj ℂ) IsTerminal
+  Terminal = Σ (Object ℂ) IsTerminal
--- a/src/Cat/Category/CartesianClosed.agda
+++ b/src/Cat/Category/CartesianClosed.agda
@ -0,0 +1,12 @@
+module Cat.Category.CartesianClosed where
+
+open import Agda.Primitive
+
+open import Cat.Category
+open import Cat.Category.Product
+open import Cat.Category.Exponential
+
+record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
+  field
+    {{hasProducts}}     : HasProducts ℂ
+    {{hasExponentials}} : HasExponentials ℂ
--- a/src/Cat/Category/Exponential.agda
+++ b/src/Cat/Category/Exponential.agda
@ -0,0 +1,39 @@
+module Cat.Category.Exponential where
+
+open import Agda.Primitive
+open import Data.Product
+open import Cubical
+
+open import Cat.Category
+open import Cat.Category.Product
+
+open Category
+
+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 : Object ℂ) where
+    IsExponential : (Cᴮ : Object ℂ) → ℂ [ Cᴮ ×p B , C ] → Set (ℓ ⊔ ℓ')
+    IsExponential Cᴮ eval = ∀ (A : Object ℂ) (f : ℂ [ A ×p B , C ])
+      → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f)
+
+    record Exponential : Set (ℓ ⊔ ℓ') where
+      field
+        -- obj ≡ Cᴮ
+        obj : Object ℂ
+        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 ℂ) → ℂ [ A ×p B , C ] → ℂ [ A , obj ]
+      transpose A f = proj₁ (isExponential A f)
+
+record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where
+  field
+    exponent : (A B : Object ℂ) → Exponential ℂ A B
--- a/src/Cat/Category/Free.agda
+++ b/src/Cat/Category/Free.agda
@ -1,42 +0,0 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-module Cat.Category.Free where
-
-open import Agda.Primitive
-open import Cubical hiding (Path)
-open import Data.Product
-
-open import Cat.Category as C
-
-module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-  private
-    open module ℂ = Category ℂ
-
-  postulate
-    Path : ( a b : Obj ℂ ) → Set ℓ'
-    emptyPath : (o : Obj ℂ) → Path o o
-    concatenate : {a b c : Obj ℂ} → Path b c → Path a b → Path a c
-
-  private
-    module _ {A B C D : Obj ℂ} {r : Path A B} {q : Path B C} {p : Path C D} where
-      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
-      postulate
-        ident-r : concatenate {A} {A} {B} p (emptyPath A) ≡ p
-        ident-l : concatenate {A} {B} {B} (emptyPath B) p ≡ p
-
-  RawFree : RawCategory ℓ ℓ'
-  RawFree = record
-    { Object = Obj ℂ
-    ; Arrow = Path
-    ; 𝟙 = λ {o} → emptyPath o
-    ; _∘_ = λ {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/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@ -0,0 +1,150 @@
+module Cat.Category.Functor where
+
+open import Agda.Primitive
+open import Cubical
+open import Function
+
+open import Cat.Category
+
+open Category hiding (_∘_ ; raw)
+
+module _ {ℓc ℓc' ℓd ℓd'}
+    (ℂ : Category ℓc ℓc')
+    (𝔻 : Category ℓd ℓd')
+    where
+
+  private
+    ℓ = ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd'
+    𝓤 = Set ℓ
+
+  record RawFunctor : 𝓤 where
+    field
+      func* : Object ℂ → Object 𝔻
+      func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
+
+  record IsFunctor (F : RawFunctor) : 𝓤 where
+    open RawFunctor F
+    field
+      ident   : {c : Object ℂ} → func→ (𝟙 ℂ {c}) ≡ 𝟙 𝔻 {func* c}
+      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
+      raw : RawFunctor
+      {{isFunctor}} : IsFunctor raw
+
+    private
+      module R = RawFunctor raw
+
+    func* : Object ℂ → Object 𝔻
+    func* = R.func*
+
+    func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
+    func→ = R.func→
+
+open IsFunctor
+open Functor
+
+-- TODO: Is `IsFunctor` a proposition?
+module _
+    {ℓa ℓb : Level}
+    {ℂ 𝔻 : Category ℓa ℓb}
+    {F : RawFunctor ℂ 𝔻}
+    where
+  private
+    module 𝔻 = IsCategory (isCategory 𝔻)
+
+  -- isProp  : Set ℓ
+  -- isProp  = (x y : A) → x ≡ y
+
+  IsFunctorIsProp : isProp (IsFunctor _ _ F)
+  IsFunctorIsProp isF0 isF1 i = record
+    { ident = 𝔻.arrowIsSet isF0.ident isF1.ident i
+    ; distrib = 𝔻.arrowIsSet isF0.distrib isF1.distrib i
+    }
+    where
+      module isF0 = IsFunctor isF0
+      module isF1 = IsFunctor isF1
+
+-- Alternate version of above where `F` is a path in 
+module _
+    {ℓa ℓb : Level}
+    {ℂ 𝔻 : Category ℓa ℓb}
+    {F : I → RawFunctor ℂ 𝔻}
+    where
+  private
+    module 𝔻 = IsCategory (isCategory 𝔻)
+  IsProp' : {ℓ : Level} (A : I → Set ℓ) → Set ℓ
+  IsProp' A = (a0 : A i0) (a1 : A i1) → A [ a0 ≡ a1 ]
+
+  postulate IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
+  -- IsFunctorIsProp' isF0 isF1 i = record
+  --   { ident = {!𝔻.arrowIsSet {!isF0.ident!} {!isF1.ident!} i!}
+  --   ; distrib = {!𝔻.arrowIsSet {!isF0.distrib!} {!isF1.distrib!} i!}
+  --   }
+  --   where
+  --     module isF0 = IsFunctor isF0
+  --     module isF1 = IsFunctor isF1
+
+module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
+  Functor≡ : {F G : Functor ℂ 𝔻}
+    → (eq* : func* F ≡ func* G)
+    → (eq→ : (λ i → ∀ {x y} → ℂ [ x , y ] → 𝔻 [ eq* i x , eq* i y ])
+        [ func→ F ≡ func→ G ])
+    → F ≡ G
+  Functor≡ {F} {G} eq* eq→ i = record
+    { raw = eqR i
+    ; isFunctor = f i
+    }
+    where
+      eqR : raw F ≡ raw G
+      eqR i = record { func* = eq* i ; func→ = eq→ i }
+      postulate T : isSet (IsFunctor _ _ (raw F))
+      f : (λ i →  IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ]
+      f = IsFunctorIsProp' (isFunctor F) (isFunctor G)
+
+module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
+  private
+    F* = func* F
+    F→ = func→ F
+    G* = func* G
+    G→ = func→ G
+    module _ {a0 a1 a2 : Object A} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where
+
+      dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ]
+      dist = begin
+        (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 ] ∎
+
+    _∘fr_ : RawFunctor A C
+    RawFunctor.func* _∘fr_ = F* ∘ G*
+    RawFunctor.func→ _∘fr_ = F→ ∘ G→
+    instance
+      isFunctor' : IsFunctor A C _∘fr_
+      isFunctor' = record
+        { ident = begin
+          (F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩
+          F→ (G→ (𝟙 A))   ≡⟨ cong F→ (G .isFunctor .ident)⟩
+          F→ (𝟙 B)        ≡⟨ F .isFunctor .ident ⟩
+          𝟙 C             ∎
+        ; distrib = dist
+        }
+
+  _∘f_ : Functor A C
+  raw _∘f_ = _∘fr_
+
+-- The identity functor
+identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C
+identity = record
+  { raw = record
+    { func* = λ x → x
+    ; func→ = λ x → x
+    }
+  ; isFunctor = record
+    { ident = refl
+    ; distrib = refl
+    }
+  }
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@ -0,0 +1,54 @@
+module Cat.Category.Product where
+
+open import Agda.Primitive
+open import Cubical
+open import Data.Product as P hiding (_×_)
+
+open import Cat.Category
+
+open Category
+
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} where
+  IsProduct : (π₁ : ℂ [ obj , A ]) (π₂ : ℂ [ obj , B ]) → Set (ℓ ⊔ ℓ')
+  IsProduct π₁ π₂
+    = ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
+    → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ P.× ℂ [ π₂ ∘ x ] ≡ x₂)
+
+-- Tip from Andrea; Consider this style for efficiency:
+-- record IsProduct {ℓa ℓb : Level} (ℂ : Category ℓa ℓb)
+--   {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) : Set (ℓa ⊔ ℓb) where
+--   field
+--      issProduct : ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
+--        → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ P.× ℂ [ π₂ ∘ x ] ≡ x₂)
+
+-- open IsProduct
+
+record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Object ℂ) : Set (ℓ ⊔ ℓ') where
+  no-eta-equality
+  field
+    obj : Object ℂ
+    proj₁ : ℂ [ obj , A ]
+    proj₂ : ℂ [ obj , B ]
+    {{isProduct}} : IsProduct ℂ proj₁ proj₂
+
+  _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
+    → ℂ [ X , obj ]
+  _P[_×_] π₁ π₂ = proj₁ (isProduct π₁ π₂)
+
+record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
+  field
+    product : ∀ (A B : Object ℂ) → Product {ℂ = ℂ} A B
+
+  open Product
+
+  _×_ : (A B : Object ℂ) → Object ℂ
+  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
+  _|×|_ : {A A' B B' : Object ℂ} → ℂ [ A , A' ] → ℂ [ B , B' ]
+    → ℂ [ A × B , A' × B' ]
+  _|×|_ {A = A} {A' = A'} {B = B} {B' = B'} a b
+    = product A' B'
+      P[ ℂ [ a ∘ (product A B) .proj₁ ]
+      ×  ℂ [ b ∘ (product A B) .proj₂ ]
+      ]
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@ -7,12 +7,12 @@ open import Data.Product
 open import Cubical

 open import Cat.Category
-open import Cat.Functor
+open import Cat.Category.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
+module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where
  open Category ℂ
  open IsCategory (isCategory)

@ -51,7 +51,6 @@ epi-mono-is-not-iso f =

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

 -- module _ {ℓ : Level} {ℂ : Category ℓ ℓ}
@ -61,7 +60,7 @@ open Functor
 --   open import Cat.Categories.Fun
 --   open import Cat.Categories.Sets
 --   -- module Cat = Cat.Categories.Cat
--   open Exponential
+--   open import Cat.Category.Exponential
 --   private
 --     Catℓ = Cat ℓ ℓ
 --     prshf = presheaf {ℂ = ℂ}
--- a/src/Cat/CwF.agda
+++ b/src/Cat/CwF.agda
@ -4,7 +4,7 @@ open import Agda.Primitive
 open import Data.Product

 open import Cat.Category
-open import Cat.Functor
+open import Cat.Category.Functor
 open import Cat.Categories.Fam

 open Category
@ -17,25 +17,27 @@ module _ {ℓa ℓb : Level} where
      -- "A base category"
      ℂ : Category ℓa ℓb
    -- It's objects are called contexts
-    Contexts = ℂ .Object
+    Contexts = Object ℂ
    -- It's arrows are called substitutions
-    Substitutions = ℂ .Arrow
+    Substitutions = Arrow ℂ
    field
      -- A functor T
      T : Functor (Opposite ℂ) (Fam ℓa ℓb)
      -- Empty context
      [] : Terminal ℂ
-    Type : (Γ : ℂ .Object) → Set ℓa
-    Type Γ = proj₁ (T .func* Γ)
+    private
+      module T = Functor T
+    Type : (Γ : Object ℂ) → Set ℓa
+    Type Γ = proj₁ (T.func* Γ)

-    module _ {Γ : ℂ .Object} {A : Type Γ} where
+    module _ {Γ : Object ℂ} {A : Type Γ} where

-      module _ {A B : ℂ .Object} {γ : ℂ [ A , B ]} 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 = T.func→ γ
        k₁ : proj₁ (func* T B) → proj₁ (func* T A)
        k₁ = proj₁ k
        k₂ : ({x : proj₁ (func* T B)} →
@ -44,8 +46,8 @@ module _ {ℓa ℓb : Level} where

      record ContextComprehension : Set (ℓa ⊔ ℓb) where
        field
-          Γ&A : ℂ .Object
-          proj1 : ℂ .Arrow Γ&A Γ
+          Γ&A : Object ℂ
+          proj1 : ℂ [ Γ&A , Γ ]
          -- proj2 : ????

        -- if γ : ℂ [ A , B ]
--- a/src/Cat/Functor.agda
+++ b/src/Cat/Functor.agda
@ -1,97 +0,0 @@
-module Cat.Functor where
-
-open import Agda.Primitive
-open import Cubical
-open import Function
-
-open import Cat.Category
-
-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
-
-module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
-
-  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→ : (λ 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→ 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
-    F* = F .func*
-    F→ = F .func→
-    G* = G .func*
-    G→ = G .func→
-    module _ {a0 a1 a2 : A .Object} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where
-
-      dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ]
-      dist = begin
-        (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→
-      ; 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
-identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C
-identity = record
-  { func* = λ x → x
-  ; func→ = λ x → x
-  ; isFunctor = record
-    { ident = refl
-    ; distrib = refl
-    }
-  }