From da10e63cc8f3aeaefdefe5c56bdbb88557e3469c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 17 Jan 2018 23:00:27 +0100
Subject: [PATCH 01/14] Fix import-statements. Make file that checks everything

---
 src/Cat/Categories/Cat.agda | 12 +++++-------
 src/Cat/Category/Bij.agda   |  7 +++++--
 src/Cat/Category/Free.agda  |  5 +++--
 src/Cat/Category/Pathy.agda |  3 ++-
 src/Cat/Cubical.agda        |  1 +
 5 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 79efc49..1133eee 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -1,13 +1,14 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
 
-module Category.Categories.Cat where
+module Cat.Categories.Cat where
 
 open import Agda.Primitive
 open import Cubical
 open import Function
 open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
 
-open import Category
+open import Cat.Category
+open import Cat.Functor
 
 -- The category of categories
 module _ {ℓ ℓ' : Level} where
@@ -29,10 +30,7 @@ module _ {ℓ ℓ' : Level} where
   --      → Functor.ident f ≡ Functor.ident g
   --       → Functor.distrib f ≡ Functor.distrib g
         → f ≡ g
-      lift-eq
-        (functor func* func→ idnt distrib)
-        (functor func*₁ func→₁ idnt₁ distrib₁)
-        eq-func* = {!!}
+      lift-eq f g eq* x = {!!}
 
     module _ {A B : Category {ℓ} {ℓ'}} {f : Functor A B} where
       idHere = identity {ℓ} {ℓ'} {A}
diff --git a/src/Cat/Category/Bij.agda b/src/Cat/Category/Bij.agda
index 217c329..0d55500 100644
--- a/src/Cat/Category/Bij.agda
+++ b/src/Cat/Category/Bij.agda
@@ -1,6 +1,9 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
+
+module Cat.Category.Bij where
 
 open import Cubical.PathPrelude hiding ( Id )
+open import Cubical.FromStdLib
 
 module _ {A : Set} {a : A} {P : A → Set} where
   Q : A → Set
@@ -20,7 +23,7 @@ module _ {A : Set} {a : A} {P : A → Set} where
   w x = {!!}
 
   vw-bij : (a : P a) → (w ∘ v) a ≡ a
-  vw-bij a = refl
+  vw-bij a = ?
   -- tubij a with (t ∘ u) a
   -- ... | q = {!!}
 
diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda
index c67f25a..57aadc6 100644
--- a/src/Cat/Category/Free.agda
+++ b/src/Cat/Category/Free.agda
@@ -1,9 +1,10 @@
-module Category.Free where
+module Cat.Category.Free where
 
 open import Agda.Primitive
 open import Cubical.PathPrelude hiding (Path)
+open import Data.Product
 
-open import Category as C
+open import Cat.Category as C
 
 module _ {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'}) where
   private
diff --git a/src/Cat/Category/Pathy.agda b/src/Cat/Category/Pathy.agda
index 7738726..e33a2ca 100644
--- a/src/Cat/Category/Pathy.agda
+++ b/src/Cat/Category/Pathy.agda
@@ -1,7 +1,8 @@
 {-# OPTIONS --cubical #-}
 
-module Category.Pathy where
+module Cat.Category.Pathy where
 
+open import Level
 open import Cubical.PathPrelude
 
 {-
diff --git a/src/Cat/Cubical.agda b/src/Cat/Cubical.agda
index cba1c41..f5abda3 100644
--- a/src/Cat/Cubical.agda
+++ b/src/Cat/Cubical.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Cubical where
 
 open import Agda.Primitive

From 5fd7dcae9dbec409bbd3c2c16f653fb202e87261 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 00:21:25 +0100
Subject: [PATCH 02/14] Notes from Andrea and some stuff about products

---
 src/Cat/Categories/Cat.agda  | 115 ++++++++++++++++++++++++++++-------
 src/Cat/Categories/Sets.agda |   4 ++
 src/Cat/Category.agda        | 109 +++++++++++++++++++++++----------
 src/Cat/Category/Bij.agda    |   2 +-
 src/Cat/Cubical.agda         |   7 ++-
 5 files changed, 181 insertions(+), 56 deletions(-)

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

From 40816eb17a621278958a420efcf59a43c160e828 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 00:21:51 +0100
Subject: [PATCH 03/14] Dummy file to compile everything

---
 src/Cat.agda | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 src/Cat.agda

diff --git a/src/Cat.agda b/src/Cat.agda
new file mode 100644
index 0000000..6cb8e32
--- /dev/null
+++ b/src/Cat.agda
@@ -0,0 +1,12 @@
+module Cat where
+
+import Cat.Categories.Sets
+import Cat.Categories.Cat
+import Cat.Categories.Rel
+import Cat.Category.Pathy
+import Cat.Category.Bij
+import Cat.Category.Free
+import Cat.Category.Properties
+import Cat.Category
+import Cat.Cubical
+import Cat.Functor

From b379c3fed05a4fdc614c0154a666025fd98a89b6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 00:22:52 +0100
Subject: [PATCH 04/14] Add Makefile

---
 Makefile | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 Makefile

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..051f9ce
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,2 @@
+build: src/**.agda
+	agda src/Cat.agda

From 0990a3778ffb05a989a2798e7981414e73d9cb9a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 01:03:40 +0100
Subject: [PATCH 05/14] Use EqReasoning and clean up some stuff

---
 src/Cat/Category.agda | 73 +++++++++++++++++++------------------------
 1 file changed, 33 insertions(+), 40 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 7d84df8..ba1ec7f 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -44,7 +44,7 @@ record Category {ℓ ℓ'} : Set (lsuc (ℓ' ⊔ ℓ)) where
 
 open Category public
 
-module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } where
+module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : ℂ .Object } where
   private
     open module ℂ = Category ℂ
     _+_ = ℂ._⊕_
@@ -59,36 +59,28 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } w
   Monomorphism {X} f = ( g₀ g₁ : ℂ.Arrow X A ) → f + g₀ ≡ f + g₁ → g₀ ≡ g₁
 
   iso-is-epi : ∀ {X} (f : ℂ.Arrow A B) → Isomorphism f → Epimorphism {X = X} f
-  -- Idea: Pre-compose with f- on both sides of the equality of eq to get
-  -- g₀ + f + f- ≡ g₁ + f + f-
-  -- which by left-inv reduces to the goal.
   iso-is-epi f (f- , left-inv , right-inv) g₀ g₁ eq =
-     trans (sym (fst ℂ.ident))
-       ( trans (cong (_+_ g₀) (sym right-inv))
-         ( trans ℂ.assoc
-           ( trans (cong (λ x → x + f-) eq)
-             ( trans (sym ℂ.assoc)
-               ( trans (cong (_+_ g₁) right-inv) (fst ℂ.ident))
-             )
-           )
-         )
-       )
+    begin
+    g₀              ≡⟨ sym (fst ℂ.ident) ⟩
+    g₀ + ℂ.𝟙        ≡⟨ cong (_+_ g₀) (sym right-inv) ⟩
+    g₀ + (f + f-)   ≡⟨ ℂ.assoc ⟩
+    (g₀ + f) + f-   ≡⟨ cong (λ x → x + f-) eq ⟩
+    (g₁ + f) + f-   ≡⟨ sym ℂ.assoc ⟩
+    g₁ + (f + f-)   ≡⟨ cong (_+_ g₁) right-inv ⟩
+    g₁ + ℂ.𝟙        ≡⟨ fst ℂ.ident ⟩
+    g₁              ∎
 
   iso-is-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Monomorphism {X = X} f
-  -- For the next goal we do something similar: Post-compose with f- and use
-  -- right-inv to get the goal.
   iso-is-mono f (f- , (left-inv , right-inv)) g₀ g₁ eq =
-    trans (sym (snd ℂ.ident))
-      ( trans (cong (λ x → x + g₀) (sym left-inv))
-        ( trans (sym ℂ.assoc)
-          ( trans (cong (_+_ f-) eq)
-            ( trans ℂ.assoc
-              ( trans (cong (λ x → x + g₁) left-inv) (snd ℂ.ident)
-              )
-            )
-          )
-        )
-      )
+    begin
+    g₀            ≡⟨ sym (snd ℂ.ident) ⟩
+    ℂ.𝟙 + g₀      ≡⟨ cong (λ x → x + g₀) (sym left-inv) ⟩
+    (f- + f) + g₀ ≡⟨ sym ℂ.assoc ⟩
+    f- + (f + g₀) ≡⟨ cong (_+_ f-) eq ⟩
+    f- + (f + g₁) ≡⟨ ℂ.assoc ⟩
+    (f- + f) + g₁ ≡⟨ cong (λ x → x + g₁) left-inv ⟩
+    ℂ.𝟙 + g₁      ≡⟨ snd ℂ.ident ⟩
+    g₁            ∎
 
   iso-is-epi-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
   iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso
@@ -102,9 +94,7 @@ epi-mono-is-not-iso f =
 
 -- Isomorphism of objects
 _≅_ : { ℓ ℓ' : Level } → { ℂ : Category {ℓ} {ℓ'} } → ( A B : Object ℂ ) → Set ℓ'
-_≅_ {ℂ = ℂ} A B = Σ[ f ∈ ℂ.Arrow A B ] (Isomorphism {ℂ = ℂ} f)
-  where
-    open module ℂ = Category ℂ
+_≅_ {ℂ = ℂ} A B = Σ[ f ∈ ℂ .Arrow A B ] (Isomorphism {ℂ = ℂ} f)
 
 IsProduct : ∀ {ℓ ℓ'} (ℂ : Category {ℓ} {ℓ'}) {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
 IsProduct ℂ {A = A} {B = B} π₁ π₂
@@ -113,21 +103,23 @@ IsProduct ℂ {A = A} {B = B} π₁ π₂
   where
     open module ℂ = Category ℂ
 
--- Consider this style for efficiency:
--- record R : Set where
+-- 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
---     isP : IsProduct {!!} {!!} {!!}
+--      isProduct : ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B)
+--        → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ. _⊕_ π₂ x ≡ x₂)
 
-record Product {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} (A B : Category.Object ℂ) : Set (ℓ ⊔ ℓ') where
+record Product {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} (A B : ℂ .Object) : Set (ℓ ⊔ ℓ') where
   no-eta-equality
   field
-    obj : Category.Object ℂ
-    proj₁ : Category.Arrow ℂ obj A
-    proj₂ : Category.Arrow ℂ obj B
+    obj : ℂ .Object
+    proj₁ : ℂ .Arrow obj A
+    proj₂ : ℂ .Arrow obj B
     {{isProduct}} : IsProduct ℂ proj₁ proj₂
 
 mutual
-  catProduct : {ℓ : Level} → ( C D : Category {ℓ} {ℓ} ) → Category {ℓ} {ℓ}
+  catProduct : {ℓ : Level} → (C D : Category {ℓ} {ℓ}) → Category {ℓ} {ℓ}
   catProduct C D =
     record
       { Object = C.Object × D.Object
@@ -145,8 +137,9 @@ mutual
       open module C = Category C
       open module D = Category D
       -- Two pairs are equal if their components are equal.
-      eqpair : {ℓ : Level} → { A : Set ℓ } → { B : Set ℓ } → { a a' : A } → { b b' : B } → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
-      eqpair {a = a} {b = b} eqa eqb = subst eqa (subst eqb (refl {x = (a , b)}))
+      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
 
 
   -- arrowProduct : ∀ {ℓ} {C D : Category {ℓ} {ℓ}} → (Object C) × (Object D) → (Object C) × (Object D) → Set ℓ

From 07e4269399361567106cd711265c1ad145adbe2b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 01:11:08 +0100
Subject: [PATCH 06/14] Make level-parameters to Category explicit

---
 src/Cat/Categories/Cat.agda      | 12 ++++++------
 src/Cat/Categories/Rel.agda      |  2 +-
 src/Cat/Categories/Sets.agda     | 10 +++++-----
 src/Cat/Category.agda            | 20 ++++++++++----------
 src/Cat/Category/Free.agda       |  6 +++---
 src/Cat/Category/Properties.agda |  4 ++--
 src/Cat/Cubical.agda             |  2 +-
 src/Cat/Functor.agda             |  6 +++---
 8 files changed, 31 insertions(+), 31 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 79aeb58..916ca9a 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -20,7 +20,7 @@ snd (lift-eq a b i) = b i
 
 open Functor
 open Category
-module _ {ℓ ℓ' : Level} {A B : Category {ℓ} {ℓ'}} where
+module _ {ℓ ℓ' : Level} {A B : Category ℓ ℓ'} where
   lift-eq-functors : {f g : Functor A B}
     → (eq* : Functor.func* f ≡ Functor.func* g)
     → (eq→ : PathP (λ i → ∀ {x y} → Arrow A x y → Arrow B (eq* i x) (eq* i y))
@@ -41,11 +41,11 @@ module _ {ℓ ℓ' : Level} {A B : Category {ℓ} {ℓ'}} where
 module _ {ℓ ℓ' : Level} where
   private
     _⊛_ = functor-comp
-    module _ {A B C D : Category {ℓ} {ℓ'}} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
+    module _ {A B C D : Category ℓ ℓ'} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
       postulate assc : h ⊛ (g ⊛ f) ≡ (h ⊛ g) ⊛ f
       -- assc = lift-eq-functors refl refl {!refl!} λ i j → {!!}
 
-    module _ {A B : Category {ℓ} {ℓ'}} {f : Functor A B} where
+    module _ {A B : Category ℓ ℓ'} {f : Functor A B} where
       lem : (func* f) ∘ (func* (identity {C = A})) ≡ func* f
       lem = refl
       -- lemmm : func→ {C = A} {D = B} (f ⊛ identity) ≡ func→ f
@@ -62,10 +62,10 @@ module _ {ℓ ℓ' : Level} where
       postulate ident-l : identity ⊛ f ≡ f
       -- ident-l = lift-eq-functors lem lemmm {!refl!} {!!}
 
-  CatCat : Category {lsuc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'}
+  CatCat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
   CatCat =
     record
-      { Object = Category {ℓ} {ℓ'}
+      { Object = Category ℓ ℓ'
       ; Arrow = Functor
       ; 𝟙 = identity
       ; _⊕_ = functor-comp
@@ -74,7 +74,7 @@ module _ {ℓ ℓ' : Level} where
       ; ident = ident-r , ident-l
       }
 
-module _  {ℓ : Level} (C D : Category {ℓ} {ℓ}) where
+module _  {ℓ : Level} (C D : Category ℓ ℓ) where
   private
     proj₁ : Arrow CatCat (catProduct C D) C
     proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl }
diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index 32e07f4..0f2fce9 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -154,7 +154,7 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset
          ≡ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
   is-assoc = equivToPath equi
 
-Rel : Category
+Rel : Category (lsuc lzero) (lsuc lzero)
 Rel = record
   { Object = Set
   ; Arrow = λ S R → Subset (S × R)
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 62c463e..5993b4b 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -15,7 +15,7 @@ open import Cat.Functor
 Fun : {ℓ : Level} → ( T U : Set ℓ ) → Set ℓ
 Fun T U = T → U
 
-Sets : {ℓ : Level} → Category {lsuc ℓ} {ℓ}
+Sets : {ℓ : Level} → Category (lsuc ℓ) ℓ
 Sets {ℓ} = record
   { Object = Set ℓ
   ; Arrow = λ T U → Fun {ℓ} T U
@@ -26,11 +26,11 @@ Sets {ℓ} = record
   }
 
 -- Covariant Presheaf
-Representable : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → Set (ℓ ⊔ lsuc ℓ')
+Representable : {ℓ ℓ' : Level} → (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
 Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
 
 -- The "co-yoneda" embedding.
-representable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Representable ℂ
+representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
 representable {ℂ = ℂ} A = record
   { func* = λ B → ℂ.Arrow A B
   ; func→ = λ f g → f ℂ.⊕ g
@@ -41,11 +41,11 @@ representable {ℂ = ℂ} A = record
     open module ℂ = Category ℂ
 
 -- Contravariant Presheaf
-Presheaf : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → Set (ℓ ⊔ lsuc ℓ')
+Presheaf : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
 Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
 
 -- Alternate name: `yoneda`
-presheaf : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object (Opposite ℂ) → Presheaf ℂ
+presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ
 presheaf {ℂ = ℂ} B = record
   { func* = λ A → ℂ.Arrow A B
   ; func→ = λ f g → g ℂ.⊕ f
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index ba1ec7f..c388f77 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -24,7 +24,7 @@ syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
 postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
 
-record Category {ℓ ℓ'} : Set (lsuc (ℓ' ⊔ ℓ)) where
+record Category (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
   -- adding no-eta-equality can speed up type-checking.
   no-eta-equality
   field
@@ -44,7 +44,7 @@ record Category {ℓ ℓ'} : Set (lsuc (ℓ' ⊔ ℓ)) where
 
 open Category public
 
-module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : ℂ .Object } where
+module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Object } where
   private
     open module ℂ = Category ℂ
     _+_ = ℂ._⊕_
@@ -93,10 +93,10 @@ epi-mono-is-not-iso f =
 -}
 
 -- Isomorphism of objects
-_≅_ : { ℓ ℓ' : Level } → { ℂ : Category {ℓ} {ℓ'} } → ( A B : Object ℂ ) → Set ℓ'
+_≅_ : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} (A B : Object ℂ) → Set ℓ'
 _≅_ {ℂ = ℂ} A B = Σ[ f ∈ ℂ .Arrow A B ] (Isomorphism {ℂ = ℂ} f)
 
-IsProduct : ∀ {ℓ ℓ'} (ℂ : Category {ℓ} {ℓ'}) {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
+IsProduct : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
 IsProduct ℂ {A = A} {B = B} π₁ π₂
   = ∀ {X : ℂ.Object} (x₁ : ℂ.Arrow X A) (x₂ : ℂ.Arrow X B)
   → ∃![ x ] (π₁ ℂ.⊕ x ≡ x₁ × π₂ ℂ.⊕ x ≡ x₂)
@@ -110,7 +110,7 @@ IsProduct ℂ {A = A} {B = B} π₁ π₂
 --      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 : ℂ .Object) : Set (ℓ ⊔ ℓ') where
   no-eta-equality
   field
     obj : ℂ .Object
@@ -119,7 +119,7 @@ record Product {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} (A B : ℂ .Obje
     {{isProduct}} : IsProduct ℂ proj₁ proj₂
 
 mutual
-  catProduct : {ℓ : Level} → (C D : Category {ℓ} {ℓ}) → Category {ℓ} {ℓ}
+  catProduct : ∀ {ℓ} (C D : Category ℓ ℓ) → Category ℓ ℓ
   catProduct C D =
     record
       { Object = C.Object × D.Object
@@ -146,10 +146,10 @@ mutual
   -- arrowProduct = {!!}
 
   -- Arrows in the product-category
-  arrowProduct : ∀ {ℓ} {C D : Category {ℓ} {ℓ}} (c d : Object (catProduct C D)) → Set ℓ
+  arrowProduct : ∀ {ℓ} {C D : Category ℓ ℓ} (c d : Object (catProduct C D)) → Set ℓ
   arrowProduct {C = C} {D = D} (c , d) (c' , d') = Arrow C c c' × Arrow D d d'
 
-Opposite : ∀ {ℓ ℓ'} → Category {ℓ} {ℓ'} → Category {ℓ} {ℓ'}
+Opposite : ∀ {ℓ ℓ'} → Category ℓ ℓ' → Category ℓ ℓ'
 Opposite ℂ =
   record
     { Object = ℂ.Object
@@ -173,10 +173,10 @@ Opposite ℂ =
 -- assoc (Opposite-is-involution i) = {!!}
 -- ident (Opposite-is-involution i) = {!!}
 
-Hom : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → (A B : Object ℂ) → Set ℓ'
+Hom : {ℓ ℓ' : Level} → (ℂ : Category ℓ ℓ') → (A B : Object ℂ) → Set ℓ'
 Hom ℂ A B = Arrow ℂ A B
 
-module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} where
+module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where
   HomFromArrow : (A : ℂ .Object) → {B B' : ℂ .Object} → (g : ℂ .Arrow B B')
     → Hom ℂ A B → Hom ℂ A B'
   HomFromArrow _A = _⊕_ ℂ
diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda
index 57aadc6..d6ca6ac 100644
--- a/src/Cat/Category/Free.agda
+++ b/src/Cat/Category/Free.agda
@@ -6,12 +6,12 @@ open import Data.Product
 
 open import Cat.Category as C
 
-module _ {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'}) where
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   private
     open module ℂ = Category ℂ
     Obj = ℂ.Object
 
-  Path : ( a b : Obj ) → Set
+  Path : ( a b : Obj ) → Set ℓ'
   Path a b = undefined
 
   postulate emptyPath : (o : Obj) → Path o o
@@ -28,7 +28,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'}) where
         ident-r : concatenate {A} {A} {B} p (emptyPath A) ≡ p
         ident-l : concatenate {A} {B} {B} (emptyPath B) p ≡ p
 
-  Free : Category
+  Free : Category ℓ ℓ'
   Free = record
     { Object = Obj
     ; Arrow = Path
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index d8bd40c..adfec58 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -7,7 +7,7 @@ open import Cat.Functor
 open import Cat.Categories.Sets
 
 module _ {ℓa ℓa' ℓb ℓb'} where
-  Exponential : Category {ℓa} {ℓa'} → Category {ℓb} {ℓb'} → Category {{!!}} {{!!}}
+  Exponential : Category ℓa ℓa' → Category ℓb ℓb' → Category ? ?
   Exponential A B = record
     { Object = {!!}
     ; Arrow = {!!}
@@ -19,5 +19,5 @@ module _ {ℓa ℓa' ℓb ℓb'} where
 
 _⇑_ = Exponential
 
-yoneda : ∀ {ℓ ℓ'} → {ℂ : Category {ℓ} {ℓ'}} → Functor ℂ (Sets ⇑ (Opposite ℂ))
+yoneda : ∀ {ℓ ℓ'} → {ℂ : Category ℓ ℓ'} → Functor ℂ (Sets ⇑ (Opposite ℂ))
 yoneda = {!!}
diff --git a/src/Cat/Cubical.agda b/src/Cat/Cubical.agda
index 92f3d12..025e202 100644
--- a/src/Cat/Cubical.agda
+++ b/src/Cat/Cubical.agda
@@ -42,7 +42,7 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
     Mor = Σ themap rules
 
   -- The category of names and substitutions
-  ℂ : Category -- {ℓo} {lsuc lzero ⊔ ℓo}
+  ℂ : Category ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
   ℂ = record
     -- { Object = FiniteDecidableSubset
     { Object = Ns → Bool
diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda
index 4daaef3..f4e0bba 100644
--- a/src/Cat/Functor.agda
+++ b/src/Cat/Functor.agda
@@ -6,7 +6,7 @@ open import Function
 
 open import Cat.Category
 
-record Functor {ℓc ℓc' ℓd ℓd'} (C : Category {ℓc} {ℓc'}) (D : Category {ℓd} {ℓd'})
+record Functor {ℓc ℓc' ℓd ℓd'} (C : Category ℓc ℓc') (D : Category ℓd ℓd')
   : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
   private
     open module C = Category C
@@ -21,7 +21,7 @@ record Functor {ℓc ℓc' ℓd ℓd'} (C : Category {ℓc} {ℓc'}) (D : Catego
     distrib : { c c' c'' : C.Object} {a : C.Arrow c c'} {a' : C.Arrow c' c''}
       → func→ (a' C.⊕ a) ≡ func→ a' D.⊕ func→ a
 
-module _ {ℓ ℓ' : Level} {A B C : Category {ℓ} {ℓ'}} (F : Functor B C) (G : Functor A B) where
+module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
   private
     open module F = Functor F
     open module G = Functor G
@@ -56,7 +56,7 @@ module _ {ℓ ℓ' : Level} {A B C : Category {ℓ} {ℓ'}} (F : Functor B C) (G
       }
 
 -- The identity functor
-identity : {ℓ ℓ' : Level} → {C : Category {ℓ} {ℓ'}} → Functor C C
+identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C
 -- Identity = record { F* = λ x → x ; F→ = λ x → x ; ident = refl ; distrib = refl }
 identity = record
   { func* = λ x → x

From 4c13334277cc5750e01959773cbf9b528dceba5a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 14:31:37 +0100
Subject: [PATCH 07/14] Make properties of a category an instance argument

---
 src/Cat/Categories/Cat.agda      |  47 +++++++++++---
 src/Cat/Categories/Rel.agda      |   3 +-
 src/Cat/Categories/Sets.agda     |  37 ++++++-----
 src/Cat/Category.agda            | 101 ++++++++++++++-----------------
 src/Cat/Category/Free.agda       |   3 +-
 src/Cat/Category/Properties.agda |   5 +-
 src/Cat/Cubical.agda             |   3 +-
 7 files changed, 109 insertions(+), 90 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 916ca9a..c57e183 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -70,16 +70,49 @@ module _ {ℓ ℓ' : Level} where
       ; 𝟙 = identity
       ; _⊕_ = functor-comp
       -- What gives here? Why can I not name the variables directly?
-      ; assoc = λ {_ _ _ _ f g h} → assc {f = f} {g = g} {h = h}
-      ; ident = ident-r , ident-l
+      ; isCategory = {!!}
+--      ; assoc = λ {_ _ _ _ f g h} → assc {f = f} {g = g} {h = h}
+--      ; ident = ident-r , ident-l
       }
 
-module _  {ℓ : Level} (C D : Category ℓ ℓ) where
+module _ {ℓ : Level} (C D : Category ℓ ℓ) where
   private
-    proj₁ : Arrow CatCat (catProduct C D) C
+    :Object: = C .Object × D .Object
+    :Arrow:  : :Object: → :Object: → Set ℓ
+    :Arrow: (c , d) (c' , d') = Arrow C c c' × Arrow D d d'
+    :𝟙: : {o : :Object:} → :Arrow: o o
+    :𝟙: = C .𝟙 , D .𝟙
+    _:⊕:_ :
+      {a b c : :Object:} →
+      :Arrow: b c →
+      :Arrow: a b →
+      :Arrow: a c
+    _:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → (C ._⊕_) bc∈C ab∈C , D ._⊕_ bc∈D ab∈D}
+
+    instance
+      :isCategory: : IsCategory :Object: :Arrow: :𝟙: _:⊕:_
+      :isCategory: = record
+        { assoc = eqpair C.assoc D.assoc
+        ; ident
+        = eqpair (fst C.ident) (fst D.ident)
+        , eqpair (snd C.ident) (snd D.ident)
+        }
+        where
+          open module C = IsCategory (C .isCategory)
+          open module D = IsCategory (D .isCategory)
+
+    :product: : Category ℓ ℓ
+    :product: = record
+      { Object = :Object:
+      ; Arrow = :Arrow:
+      ; 𝟙 = :𝟙:
+      ; _⊕_ = _:⊕:_
+      }
+
+    proj₁ : Arrow CatCat :product: C
     proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl }
 
-    proj₂ : Arrow CatCat (catProduct C D) D
+    proj₂ : Arrow CatCat :product: D
     proj₂ = record { func* = snd ; func→ = snd ; ident = refl ; distrib = refl }
 
     module _ {X : Object (CatCat {ℓ} {ℓ})} (x₁ : Arrow CatCat X C) (x₂ : Arrow CatCat X D) where
@@ -88,7 +121,7 @@ module _  {ℓ : Level} (C D : Category ℓ ℓ) where
       -- ident' : {c : Object X} → ((func→ x₁) {dom = c} (𝟙 X) , (func→ x₂) {dom = c} (𝟙 X)) ≡ 𝟙 (catProduct C D)
       -- ident' {c = c} = lift-eq (ident x₁) (ident x₂)
 
-      x : Functor X (catProduct C D)
+      x : Functor X :product:
       x = record
         { func* = λ x → (func* x₁) x , (func* x₂) x
         ; func→ = λ x → func→ x₁ x , func→ x₂ x
@@ -116,7 +149,7 @@ module _  {ℓ : Level} (C D : Category ℓ ℓ) where
 
   product : Product {ℂ = CatCat} C D
   product = record
-    { obj = catProduct C D
+    { obj = :product:
     ; proj₁ = proj₁
     ; proj₂ = proj₂
     }
diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index 0f2fce9..b398aa9 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -160,6 +160,5 @@ Rel = record
   ; Arrow = λ S R → Subset (S × R)
   ; 𝟙 = λ {S} → Diag S
   ; _⊕_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
-  ; assoc = funExt is-assoc
-  ; ident = funExt ident-l , funExt ident-r
+  ; isCategory = record { assoc = funExt is-assoc ; ident = funExt ident-l , funExt ident-r }
   }
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 5993b4b..3579b52 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -9,21 +9,18 @@ open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
 
 open import Cat.Category
 open import Cat.Functor
-
--- Sets are built-in to Agda. The set of all small sets is called Set.
-
-Fun : {ℓ : Level} → ( T U : Set ℓ ) → Set ℓ
-Fun T U = T → U
+open Category
 
 Sets : {ℓ : Level} → Category (lsuc ℓ) ℓ
 Sets {ℓ} = record
   { Object = Set ℓ
-  ; Arrow = λ T U → Fun {ℓ} T U
-  ; 𝟙 = λ x → x
-  ; _⊕_  = λ g f x → g ( f x )
-  ; assoc = refl
-  ; ident = funExt (λ x → refl) , funExt (λ x → refl)
+  ; Arrow = λ T U → T → U
+  ; 𝟙 = id
+  ; _⊕_ = _∘′_
+  ; isCategory = record { assoc = refl ; ident = funExt (λ _ → refl) , funExt (λ _ → refl) }
   }
+  where
+    open import Function
 
 -- Covariant Presheaf
 Representable : {ℓ ℓ' : Level} → (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
@@ -32,13 +29,13 @@ Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
 -- The "co-yoneda" embedding.
 representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
 representable {ℂ = ℂ} A = record
-  { func* = λ B → ℂ.Arrow A B
-  ; func→ = λ f g → f ℂ.⊕ g
-  ; ident = funExt λ _ → snd ℂ.ident
-  ; distrib = funExt λ x → sym ℂ.assoc
+  { func* = λ B → ℂ .Arrow A B
+  ; func→ = ℂ ._⊕_
+  ; ident = funExt λ _ → snd ident
+  ; distrib = funExt λ x → sym assoc
   }
   where
-    open module ℂ = Category ℂ
+    open IsCategory (ℂ .isCategory)
 
 -- Contravariant Presheaf
 Presheaf : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
@@ -47,10 +44,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
-  ; ident = funExt λ x → fst ℂ.ident
-  ; distrib = funExt λ x → ℂ.assoc
+  { func* = λ A → ℂ .Arrow A B
+  ; func→ = λ f g → ℂ ._⊕_ g f
+  ; ident = funExt λ x → fst ident
+  ; distrib = funExt λ x → assoc
   }
   where
-    open module ℂ = Category ℂ
+    open IsCategory (ℂ .isCategory)
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index c388f77..a881c71 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -24,6 +24,20 @@ syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
 postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
 
+record IsCategory {ℓ ℓ' : Level}
+  (Object : Set ℓ)
+  (Arrow  : Object → Object → Set ℓ')
+  (𝟙      : {o : Object} → Arrow o o)
+  (_⊕_    : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c)
+  : Set (lsuc (ℓ' ⊔ ℓ)) where
+  field
+    assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
+      → h ⊕ (g ⊕ f) ≡ (h ⊕ g) ⊕ f
+    ident : {A B : Object} {f : Arrow A B}
+      → f ⊕ 𝟙 ≡ f × 𝟙 ⊕ f ≡ f
+
+-- open IsCategory public
+
 record Category (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
   -- adding no-eta-equality can speed up type-checking.
   no-eta-equality
@@ -32,17 +46,14 @@ record Category (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
     Arrow  : Object → Object → Set ℓ'
     𝟙      : {o : Object} → Arrow o o
     _⊕_    : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c
-    assoc : { A B C D : Object } { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
-      → h ⊕ (g ⊕ f) ≡ (h ⊕ g) ⊕ f
-    ident  : { A B : Object } { f : Arrow A B }
-      → f ⊕ 𝟙 ≡ f × 𝟙 ⊕ f ≡ f
+    {{isCategory}} : IsCategory Object Arrow 𝟙 _⊕_
   infixl 45 _⊕_
   domain : { a b : Object } → Arrow a b → Object
   domain {a = a} _ = a
   codomain : { a b : Object } → Arrow a b → Object
   codomain {b = b} _ = b
 
-open Category public
+open Category
 
 module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Object } where
   private
@@ -61,26 +72,30 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Object } wher
   iso-is-epi : ∀ {X} (f : ℂ.Arrow A B) → Isomorphism f → Epimorphism {X = X} f
   iso-is-epi f (f- , left-inv , right-inv) g₀ g₁ eq =
     begin
-    g₀              ≡⟨ sym (fst ℂ.ident) ⟩
+    g₀              ≡⟨ sym (fst ident) ⟩
     g₀ + ℂ.𝟙        ≡⟨ cong (_+_ g₀) (sym right-inv) ⟩
-    g₀ + (f + f-)   ≡⟨ ℂ.assoc ⟩
+    g₀ + (f + f-)   ≡⟨ assoc ⟩
     (g₀ + f) + f-   ≡⟨ cong (λ x → x + f-) eq ⟩
-    (g₁ + f) + f-   ≡⟨ sym ℂ.assoc ⟩
+    (g₁ + f) + f-   ≡⟨ sym assoc ⟩
     g₁ + (f + f-)   ≡⟨ cong (_+_ g₁) right-inv ⟩
-    g₁ + ℂ.𝟙        ≡⟨ fst ℂ.ident ⟩
+    g₁ + ℂ.𝟙        ≡⟨ fst ident ⟩
     g₁              ∎
+    where
+      open IsCategory ℂ.isCategory
 
   iso-is-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Monomorphism {X = X} f
   iso-is-mono f (f- , (left-inv , right-inv)) g₀ g₁ eq =
     begin
-    g₀            ≡⟨ sym (snd ℂ.ident) ⟩
+    g₀            ≡⟨ sym (snd ident) ⟩
     ℂ.𝟙 + g₀      ≡⟨ cong (λ x → x + g₀) (sym left-inv) ⟩
-    (f- + f) + g₀ ≡⟨ sym ℂ.assoc ⟩
+    (f- + f) + g₀ ≡⟨ sym assoc ⟩
     f- + (f + g₀) ≡⟨ cong (_+_ f-) eq ⟩
-    f- + (f + g₁) ≡⟨ ℂ.assoc ⟩
+    f- + (f + g₁) ≡⟨ assoc ⟩
     (f- + f) + g₁ ≡⟨ cong (λ x → x + g₁) left-inv ⟩
-    ℂ.𝟙 + g₁      ≡⟨ snd ℂ.ident ⟩
+    ℂ.𝟙 + g₁      ≡⟨ snd ident ⟩
     g₁            ∎
+    where
+      open IsCategory ℂ.isCategory
 
   iso-is-epi-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
   iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso
@@ -118,49 +133,27 @@ record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : ℂ .Object)
     proj₂ : ℂ .Arrow obj B
     {{isProduct}} : IsProduct ℂ proj₁ proj₂
 
-mutual
-  catProduct : ∀ {ℓ} (C D : Category ℓ ℓ) → Category ℓ ℓ
-  catProduct C D =
+-- Two pairs are equal if their components are equal.
+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
+
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
+  private
+    instance
+      _ : IsCategory (ℂ .Object) (flip (ℂ .Arrow)) (ℂ .𝟙) (flip (ℂ ._⊕_))
+      _ = record { assoc = sym assoc ; ident = swap ident }
+        where
+          open IsCategory (ℂ .isCategory)
+
+  Opposite : Category ℓ ℓ'
+  Opposite =
     record
-      { Object = C.Object × D.Object
-      -- Why does "outlining   with `arrowProduct` not work?
-      ; Arrow = λ {(c , d) (c' , d') → Arrow C c c' × Arrow D d d'}
-      ; 𝟙 = C.𝟙 , D.𝟙
-      ; _⊕_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → bc∈C C.⊕ ab∈C , bc∈D D.⊕ ab∈D}
-      ; assoc = eqpair C.assoc D.assoc
-      ; ident =
-        let (Cl , Cr) = C.ident
-            (Dl , Dr) = D.ident
-        in eqpair Cl Dl , eqpair Cr Dr
+      { Object = ℂ .Object
+      ; Arrow = flip (ℂ .Arrow)
+      ; 𝟙 = ℂ .𝟙
+      ; _⊕_ = flip (ℂ ._⊕_)
       }
-    where
-      open module C = Category C
-      open module D = Category D
-      -- Two pairs are equal if their components are equal.
-      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
-
-
-  -- arrowProduct : ∀ {ℓ} {C D : Category {ℓ} {ℓ}} → (Object C) × (Object D) → (Object C) × (Object D) → Set ℓ
-  -- arrowProduct = {!!}
-
-  -- Arrows in the product-category
-  arrowProduct : ∀ {ℓ} {C D : Category ℓ ℓ} (c d : Object (catProduct C D)) → Set ℓ
-  arrowProduct {C = C} {D = D} (c , d) (c' , d') = Arrow C c c' × Arrow D d d'
-
-Opposite : ∀ {ℓ ℓ'} → Category ℓ ℓ' → Category ℓ ℓ'
-Opposite ℂ =
-  record
-    { Object = ℂ.Object
-    ; Arrow = λ A B → ℂ.Arrow B A
-    ; 𝟙 = ℂ.𝟙
-    ; _⊕_ = λ g f → f ℂ.⊕ g
-    ; assoc = sym ℂ.assoc
-    ; ident = swap ℂ.ident
-    }
-  where
-    open module ℂ = Category ℂ
 
 -- A consequence of no-eta-equality; `Opposite-is-involution` is no longer
 -- definitional - i.e.; you must match on the fields:
diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda
index d6ca6ac..98305a6 100644
--- a/src/Cat/Category/Free.agda
+++ b/src/Cat/Category/Free.agda
@@ -34,6 +34,5 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
     ; Arrow = Path
     ; 𝟙 = λ {o} → emptyPath o
     ; _⊕_ = λ {a b c} → concatenate {a} {b} {c}
-    ; assoc = p-assoc
-    ; ident = ident-r , ident-l
+    ; isCategory = record { assoc = p-assoc ; ident = ident-r , ident-l }
     }
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index adfec58..f415fc1 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -7,14 +7,13 @@ open import Cat.Functor
 open import Cat.Categories.Sets
 
 module _ {ℓa ℓa' ℓb ℓb'} where
-  Exponential : Category ℓa ℓa' → Category ℓb ℓb' → Category ? ?
+  Exponential : Category ℓa ℓa' → Category ℓb ℓb' → Category {!!} {!!}
   Exponential A B = record
     { Object = {!!}
     ; Arrow = {!!}
     ; 𝟙 = {!!}
     ; _⊕_ = {!!}
-    ; assoc = {!!}
-    ; ident = {!!}
+    ; isCategory = ?
     }
 
 _⇑_ = Exponential
diff --git a/src/Cat/Cubical.agda b/src/Cat/Cubical.agda
index 025e202..b10afba 100644
--- a/src/Cat/Cubical.agda
+++ b/src/Cat/Cubical.agda
@@ -49,6 +49,5 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
     ; Arrow = Mor
     ; 𝟙 = {!!}
     ; _⊕_ = {!!}
-    ; assoc = {!!}
-    ; ident = {!!}
+    ; isCategory = ?
     }

From 316de7e4f9a6a88963dd09dcaa71a3c79af9ce96 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 14:32:27 +0100
Subject: [PATCH 08/14] Remove `undefined`

---
 src/Cat/Category.agda | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index a881c71..8ccad7e 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -22,8 +22,6 @@ open import Cubical
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
-postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
-
 record IsCategory {ℓ ℓ' : Level}
   (Object : Set ℓ)
   (Arrow  : Object → Object → Set ℓ')

From 793fc305348c9c6efa44fdc0e54c5647f6ad6998 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 15:01:01 +0100
Subject: [PATCH 09/14] Move properties of categories to
 Cat.Category.Properties

---
 src/Cat/Category.agda            | 89 +++++++-------------------------
 src/Cat/Category/Properties.agda | 45 +++++++++++++++-
 2 files changed, 63 insertions(+), 71 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 8ccad7e..91e25f3 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -53,68 +53,26 @@ record Category (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
 
 open Category
 
-module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Object } where
-  private
-    open module ℂ = Category ℂ
-    _+_ = ℂ._⊕_
+module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where
+  module _ { A B : ℂ .Object } where
+    Isomorphism : (f : ℂ .Arrow A B) → Set ℓ'
+    Isomorphism f = Σ[ g ∈ ℂ .Arrow B A ] ℂ ._⊕_ g f ≡ ℂ .𝟙 × ℂ ._⊕_ f g ≡ ℂ .𝟙
 
-  Isomorphism : (f : ℂ.Arrow A B) → Set ℓ'
-  Isomorphism f = Σ[ g ∈ ℂ.Arrow B A ] g ℂ.⊕ f ≡ ℂ.𝟙 × f + g ≡ ℂ.𝟙
+    Epimorphism : {X : ℂ .Object } → (f : ℂ .Arrow A B) → Set ℓ'
+    Epimorphism {X} f = ( g₀ g₁ : ℂ .Arrow B X ) → ℂ ._⊕_ g₀ f ≡ ℂ ._⊕_ g₁ f → g₀ ≡ g₁
 
-  Epimorphism : {X : ℂ.Object } → (f : ℂ.Arrow A B) → Set ℓ'
-  Epimorphism {X} f = ( g₀ g₁ : ℂ.Arrow B X ) → g₀ + f ≡ g₁ + f → g₀ ≡ g₁
+    Monomorphism : {X : ℂ .Object} → (f : ℂ .Arrow A B) → Set ℓ'
+    Monomorphism {X} f = ( g₀ g₁ : ℂ .Arrow X A ) → ℂ ._⊕_ f g₀ ≡ ℂ ._⊕_ f g₁ → g₀ ≡ g₁
 
-  Monomorphism : {X : ℂ.Object} → (f : ℂ.Arrow A B) → Set ℓ'
-  Monomorphism {X} f = ( g₀ g₁ : ℂ.Arrow X A ) → f + g₀ ≡ f + g₁ → g₀ ≡ g₁
+  -- Isomorphism of objects
+  _≅_ : (A B : Object ℂ) → Set ℓ'
+  _≅_ A B = Σ[ f ∈ ℂ .Arrow A B ] (Isomorphism f)
 
-  iso-is-epi : ∀ {X} (f : ℂ.Arrow A B) → Isomorphism f → Epimorphism {X = X} f
-  iso-is-epi f (f- , left-inv , right-inv) g₀ g₁ eq =
-    begin
-    g₀              ≡⟨ sym (fst ident) ⟩
-    g₀ + ℂ.𝟙        ≡⟨ cong (_+_ g₀) (sym right-inv) ⟩
-    g₀ + (f + f-)   ≡⟨ assoc ⟩
-    (g₀ + f) + f-   ≡⟨ cong (λ x → x + f-) eq ⟩
-    (g₁ + f) + f-   ≡⟨ sym assoc ⟩
-    g₁ + (f + f-)   ≡⟨ cong (_+_ g₁) right-inv ⟩
-    g₁ + ℂ.𝟙        ≡⟨ fst ident ⟩
-    g₁              ∎
-    where
-      open IsCategory ℂ.isCategory
-
-  iso-is-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Monomorphism {X = X} f
-  iso-is-mono f (f- , (left-inv , right-inv)) g₀ g₁ eq =
-    begin
-    g₀            ≡⟨ sym (snd ident) ⟩
-    ℂ.𝟙 + g₀      ≡⟨ cong (λ x → x + g₀) (sym left-inv) ⟩
-    (f- + f) + g₀ ≡⟨ sym assoc ⟩
-    f- + (f + g₀) ≡⟨ cong (_+_ f-) eq ⟩
-    f- + (f + g₁) ≡⟨ assoc ⟩
-    (f- + f) + g₁ ≡⟨ cong (λ x → x + g₁) left-inv ⟩
-    ℂ.𝟙 + g₁      ≡⟨ snd ident ⟩
-    g₁            ∎
-    where
-      open IsCategory ℂ.isCategory
-
-  iso-is-epi-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
-  iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso
-
-{-
-epi-mono-is-not-iso : ∀ {ℓ ℓ'} → ¬ ((ℂ : Category {ℓ} {ℓ'}) {A B X : Object ℂ} (f : Arrow ℂ A B ) → Epimorphism {ℂ = ℂ} {X = X} f → Monomorphism {ℂ = ℂ} {X = X} f → Isomorphism {ℂ = ℂ} f)
-epi-mono-is-not-iso f =
-  let k = f {!!} {!!} {!!} {!!}
-  in {!!}
--}
-
--- Isomorphism of objects
-_≅_ : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} (A B : Object ℂ) → Set ℓ'
-_≅_ {ℂ = ℂ} A B = Σ[ f ∈ ℂ .Arrow A B ] (Isomorphism {ℂ = ℂ} f)
-
-IsProduct : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
-IsProduct ℂ {A = A} {B = B} π₁ π₂
-  = ∀ {X : ℂ.Object} (x₁ : ℂ.Arrow X A) (x₂ : ℂ.Arrow X B)
-  → ∃![ x ] (π₁ ℂ.⊕ x ≡ x₁ × π₂ ℂ.⊕ x ≡ x₂)
-  where
-    open module ℂ = Category ℂ
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} where
+  IsProduct : (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
+  IsProduct π₁ π₂
+    = ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B)
+    → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ ._⊕_ π₂ x ≡ x₂)
 
 -- Tip from Andrea; Consider this style for efficiency:
 -- record IsProduct {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'})
@@ -131,19 +89,7 @@ record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : ℂ .Object)
     proj₂ : ℂ .Arrow obj B
     {{isProduct}} : IsProduct ℂ proj₁ proj₂
 
--- Two pairs are equal if their components are equal.
-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
-
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-  private
-    instance
-      _ : IsCategory (ℂ .Object) (flip (ℂ .Arrow)) (ℂ .𝟙) (flip (ℂ ._⊕_))
-      _ = record { assoc = sym assoc ; ident = swap ident }
-        where
-          open IsCategory (ℂ .isCategory)
-
   Opposite : Category ℓ ℓ'
   Opposite =
     record
@@ -151,7 +97,10 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
       ; Arrow = flip (ℂ .Arrow)
       ; 𝟙 = ℂ .𝟙
       ; _⊕_ = flip (ℂ ._⊕_)
+      ; isCategory = record { assoc = sym assoc ; ident = swap ident }
       }
+      where
+        open IsCategory (ℂ .isCategory)
 
 -- A consequence of no-eta-equality; `Opposite-is-involution` is no longer
 -- definitional - i.e.; you must match on the fields:
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index f415fc1..4ff4376 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -2,10 +2,53 @@
 
 module Cat.Category.Properties where
 
+open import Agda.Primitive
+open import Data.Product
+open import Cubical.PathPrelude
+
 open import Cat.Category
 open import Cat.Functor
 open import Cat.Categories.Sets
 
+module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Category.Object } {X : ℂ .Category.Object} (f : ℂ .Category.Arrow A B) where
+  open Category ℂ
+  open IsCategory (isCategory)
+
+  iso-is-epi : Isomorphism {ℂ = ℂ} f → Epimorphism {ℂ = ℂ} {X = X} f
+  iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq =
+    begin
+    g₀              ≡⟨ sym (proj₁ ident) ⟩
+    g₀ ⊕ 𝟙          ≡⟨ cong (_⊕_ g₀) (sym right-inv) ⟩
+    g₀ ⊕ (f ⊕ f-)   ≡⟨ assoc ⟩
+    (g₀ ⊕ f) ⊕ f-   ≡⟨ cong (λ φ → φ ⊕ f-) eq ⟩
+    (g₁ ⊕ f) ⊕ f-   ≡⟨ sym assoc ⟩
+    g₁ ⊕ (f ⊕ f-)   ≡⟨ cong (_⊕_ g₁) right-inv ⟩
+    g₁ ⊕ 𝟙          ≡⟨ proj₁ ident ⟩
+    g₁              ∎
+
+  iso-is-mono : Isomorphism {ℂ = ℂ} f → Monomorphism {ℂ = ℂ} {X = X} f
+  iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq =
+    begin
+    g₀            ≡⟨ sym (proj₂ ident) ⟩
+    𝟙 ⊕ g₀        ≡⟨ cong (λ φ → φ ⊕ g₀) (sym left-inv) ⟩
+    (f- ⊕ f) ⊕ g₀ ≡⟨ sym assoc ⟩
+    f- ⊕ (f ⊕ g₀) ≡⟨ cong (_⊕_ f-) eq ⟩
+    f- ⊕ (f ⊕ g₁) ≡⟨ assoc ⟩
+    (f- ⊕ f) ⊕ g₁ ≡⟨ cong (λ φ → φ ⊕ g₁) left-inv ⟩
+    𝟙 ⊕ g₁        ≡⟨ proj₂ ident ⟩
+    g₁            ∎
+
+  iso-is-epi-mono : Isomorphism {ℂ = ℂ} f → Epimorphism {ℂ = ℂ} {X = X} f × Monomorphism {ℂ = ℂ} {X = X} f
+  iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso
+
+{-
+epi-mono-is-not-iso : ∀ {ℓ ℓ'} → ¬ ((ℂ : Category {ℓ} {ℓ'}) {A B X : Object ℂ} (f : Arrow ℂ A B ) → Epimorphism {ℂ = ℂ} {X = X} f → Monomorphism {ℂ = ℂ} {X = X} f → Isomorphism {ℂ = ℂ} f)
+epi-mono-is-not-iso f =
+  let k = f {!!} {!!} {!!} {!!}
+  in {!!}
+-}
+
+
 module _ {ℓa ℓa' ℓb ℓb'} where
   Exponential : Category ℓa ℓa' → Category ℓb ℓb' → Category {!!} {!!}
   Exponential A B = record
@@ -13,7 +56,7 @@ module _ {ℓa ℓa' ℓb ℓb'} where
     ; Arrow = {!!}
     ; 𝟙 = {!!}
     ; _⊕_ = {!!}
-    ; isCategory = ?
+    ; isCategory = {!!}
     }
 
 _⇑_ = Exponential

From ea3e14af962a4e241c33831234e2debc34b89327 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 15:03:00 +0100
Subject: [PATCH 10/14] Re-add eqpair

---
 src/Cat/Categories/Cat.agda |  6 ++++--
 src/Cat/Category/Free.agda  | 10 ++++------
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index c57e183..37c760f 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -10,13 +10,15 @@ 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
---lift-eq a b = λ i → a i , b i
-
 
+eqpair : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} {a a' : A} {b b' : B}
+  → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
+eqpair eqa eqb i = eqa i , eqb i
 
 open Functor
 open Category
diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda
index 98305a6..ff06743 100644
--- a/src/Cat/Category/Free.agda
+++ b/src/Cat/Category/Free.agda
@@ -11,12 +11,10 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
     open module ℂ = Category ℂ
     Obj = ℂ.Object
 
-  Path : ( a b : Obj ) → Set ℓ'
-  Path a b = undefined
-
-  postulate emptyPath : (o : Obj) → Path o o
-
-  postulate concatenate : {a b c : Obj} → Path b c → Path a b → Path a c
+  postulate
+    Path : ( a b : Obj ) → Set ℓ'
+    emptyPath : (o : Obj) → Path o o
+    concatenate : {a b c : Obj} → Path b c → Path a b → Path a c
 
   private
     module _ {A B C D : Obj} {r : Path A B} {q : Path B C} {p : Path C D} where

From b158b1d420e76b0998c0b8c47a1f93fe0c5396e4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 15:19:15 +0100
Subject: [PATCH 11/14] Use TDNR

---
 src/Cat/Functor.agda | 39 +++++++++++++++++++--------------------
 1 file changed, 19 insertions(+), 20 deletions(-)

diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda
index f4e0bba..4bdd2c0 100644
--- a/src/Cat/Functor.agda
+++ b/src/Cat/Functor.agda
@@ -22,25 +22,24 @@ record Functor {ℓc ℓc' ℓd ℓd'} (C : Category ℓc ℓc') (D : Category 
       → func→ (a' C.⊕ a) ≡ func→ a' D.⊕ func→ a
 
 module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
+  open Functor
+  open Category
   private
-    open module F = Functor F
-    open module G = Functor G
-    open module A = Category A
-    open module B = Category B
-    open module C = Category C
+    F* = F .func*
+    F→ = F .func→
+    G* = G .func*
+    G→ = G .func→
+    _A⊕_ = A ._⊕_
+    _B⊕_ = B ._⊕_
+    _C⊕_ = C ._⊕_
+    module _ {a0 a1 a2 : A .Object} {α0 : A .Arrow a0 a1} {α1 : A .Arrow a1 a2} where
 
-    F* = F.func*
-    F→ = F.func→
-    G* = G.func*
-    G→ = G.func→
-    module _ {a0 a1 a2 : A.Object} {α0 : A.Arrow a0 a1} {α1 : A.Arrow a1 a2} where
-
-      dist : (F→ ∘ G→) (α1 A.⊕ α0) ≡ (F→ ∘ G→) α1 C.⊕ (F→ ∘ G→) α0
+      dist : (F→ ∘ G→) (α1 A⊕ α0) ≡ (F→ ∘ G→) α1 C⊕ (F→ ∘ G→) α0
       dist = begin
-        (F→ ∘ G→) (α1 A.⊕ α0)         ≡⟨ refl ⟩
-        F→ (G→ (α1 A.⊕ α0))           ≡⟨ cong F→ G.distrib ⟩
-        F→ ((G→ α1) B.⊕ (G→ α0))      ≡⟨ F.distrib ⟩
-        (F→ ∘ G→) α1 C.⊕ (F→ ∘ G→) α0 ∎
+        (F→ ∘ G→) (α1 A⊕ α0)         ≡⟨ refl ⟩
+        F→ (G→ (α1 A⊕ α0))           ≡⟨ cong F→ (G .distrib)⟩
+        F→ ((G→ α1) B⊕ (G→ α0))      ≡⟨ F .distrib ⟩
+        (F→ ∘ G→) α1 C⊕ (F→ ∘ G→) α0 ∎
 
   functor-comp : Functor A C
   functor-comp =
@@ -48,10 +47,10 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
       { func* = F* ∘ G*
       ; func→ = F→ ∘ G→
       ; ident = begin
-        (F→ ∘ G→) (A.𝟙) ≡⟨ refl ⟩
-        F→ (G→ (A.𝟙))   ≡⟨ cong F→ G.ident ⟩
-        F→ (B.𝟙)        ≡⟨ F.ident ⟩
-        C.𝟙             ∎
+        (F→ ∘ G→) (A .𝟙) ≡⟨ refl ⟩
+        F→ (G→ (A .𝟙))   ≡⟨ cong F→ (G .ident)⟩
+        F→ (B .𝟙)        ≡⟨ F .ident ⟩
+        C .𝟙             ∎
       ; distrib = dist
       }
 

From b21c9b7a895e459db5cd385489ed771684398e50 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 15:21:50 +0100
Subject: [PATCH 12/14] Choose new name for functor composition

---
 src/Cat/Categories/Cat.agda | 15 +++++++--------
 src/Cat/Functor.agda        |  5 ++---
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 37c760f..ae4b247 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -42,26 +42,25 @@ module _ {ℓ ℓ' : Level} {A B : Category ℓ ℓ'} where
 -- The category of categories
 module _ {ℓ ℓ' : Level} where
   private
-    _⊛_ = functor-comp
     module _ {A B C D : Category ℓ ℓ'} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
-      postulate assc : h ⊛ (g ⊛ f) ≡ (h ⊛ g) ⊛ f
+      postulate assc : h ∘f (g ∘f f) ≡ (h ∘f g) ∘f f
       -- assc = lift-eq-functors refl refl {!refl!} λ i j → {!!}
 
     module _ {A B : Category ℓ ℓ'} {f : Functor A B} where
       lem : (func* f) ∘ (func* (identity {C = A})) ≡ func* f
       lem = refl
-      -- lemmm : func→ {C = A} {D = B} (f ⊛ identity) ≡ func→ f
+      -- lemmm : func→ {C = A} {D = B} (f ∘f identity) ≡ func→ f
       lemmm : PathP
         (λ i →
         {x y : Object A} → Arrow A x y → Arrow B (func* f x) (func* f y))
-        (func→ (f ⊛ identity)) (func→ f)
+        (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 ⊛ identity)) (ident f)
+                  (ident (f ∘f identity)) (ident f)
       -- lemz = {!!}
-      postulate ident-r : f ⊛ identity ≡ f
+      postulate ident-r : f ∘f identity ≡ f
       -- ident-r = lift-eq-functors lem lemmm {!lemz!} {!!}
-      postulate ident-l : identity ⊛ f ≡ f
+      postulate ident-l : identity ∘f f ≡ f
       -- ident-l = lift-eq-functors lem lemmm {!refl!} {!!}
 
   CatCat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
@@ -70,7 +69,7 @@ module _ {ℓ ℓ' : Level} where
       { Object = Category ℓ ℓ'
       ; Arrow = Functor
       ; 𝟙 = identity
-      ; _⊕_ = functor-comp
+      ; _⊕_ = _∘f_
       -- What gives here? Why can I not name the variables directly?
       ; isCategory = {!!}
 --      ; assoc = λ {_ _ _ _ f g h} → assc {f = f} {g = g} {h = h}
diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda
index 4bdd2c0..5965f72 100644
--- a/src/Cat/Functor.agda
+++ b/src/Cat/Functor.agda
@@ -41,8 +41,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
         F→ ((G→ α1) B⊕ (G→ α0))      ≡⟨ F .distrib ⟩
         (F→ ∘ G→) α1 C⊕ (F→ ∘ G→) α0 ∎
 
-  functor-comp : Functor A C
-  functor-comp =
+  _∘f_ : Functor A C
+  _∘f_ =
     record
       { func* = F* ∘ G*
       ; func→ = F→ ∘ G→
@@ -56,7 +56,6 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
 
 -- The identity functor
 identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C
--- Identity = record { F* = λ x → x ; F→ = λ x → x ; ident = refl ; distrib = refl }
 identity = record
   { func* = λ x → x
   ; func→ = λ x → x

From 26d210dcc312b106c4dcfc12a5a7345d04887e71 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 15:23:40 +0100
Subject: [PATCH 13/14] Rename the category of categories

---
 src/Cat/Categories/Cat.agda | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index ae4b247..b25eb54 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -63,8 +63,8 @@ module _ {ℓ ℓ' : Level} where
       postulate ident-l : identity ∘f f ≡ f
       -- ident-l = lift-eq-functors lem lemmm {!refl!} {!!}
 
-  CatCat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
-  CatCat =
+  Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
+  Cat =
     record
       { Object = Category ℓ ℓ'
       ; Arrow = Functor
@@ -110,13 +110,13 @@ module _ {ℓ : Level} (C D : Category ℓ ℓ) where
       ; _⊕_ = _:⊕:_
       }
 
-    proj₁ : Arrow CatCat :product: C
+    proj₁ : Arrow Cat :product: C
     proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl }
 
-    proj₂ : Arrow CatCat :product: D
+    proj₂ : Arrow Cat :product: D
     proj₂ = record { func* = snd ; func→ = snd ; ident = refl ; distrib = refl }
 
-    module _ {X : Object (CatCat {ℓ} {ℓ})} (x₁ : Arrow CatCat X C) (x₂ : Arrow CatCat X D) where
+    module _ {X : Object (Cat {ℓ} {ℓ})} (x₁ : Arrow Cat X C) (x₂ : Arrow Cat X D) where
       open Functor
 
       -- ident' : {c : Object X} → ((func→ x₁) {dom = c} (𝟙 X) , (func→ x₂) {dom = c} (𝟙 X)) ≡ 𝟙 (catProduct C D)
@@ -132,23 +132,23 @@ 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.
-      isUniqL : (CatCat ⊕ proj₁) x ≡ x₁
+      isUniqL : (Cat ⊕ proj₁) x ≡ x₁
       isUniqL = lift-eq-functors refl refl {!!} {!!}
 
-      isUniqR : (CatCat ⊕ proj₂) x ≡ x₂
+      isUniqR : (Cat ⊕ proj₂) x ≡ x₂
       isUniqR = lift-eq-functors refl refl {!!} {!!}
 
-      isUniq : (CatCat ⊕ proj₁) x ≡ x₁ × (CatCat ⊕ proj₂) x ≡ x₂
+      isUniq : (Cat ⊕ proj₁) x ≡ x₁ × (Cat ⊕ proj₂) x ≡ x₂
       isUniq = isUniqL , isUniqR
 
-      uniq : ∃![ x ] ((CatCat ⊕ proj₁) x ≡ x₁ × (CatCat ⊕ proj₂) x ≡ x₂)
+      uniq : ∃![ x ] ((Cat ⊕ proj₁) x ≡ x₁ × (Cat ⊕ proj₂) x ≡ x₂)
       uniq = x , isUniq
 
     instance
-      isProduct : IsProduct CatCat proj₁ proj₂
+      isProduct : IsProduct Cat proj₁ proj₂
       isProduct = uniq
 
-  product : Product {ℂ = CatCat} C D
+  product : Product {ℂ = Cat} C D
   product = record
     { obj = :product:
     ; proj₁ = proj₁

From 922570a5bdab972fbbb8e89ada6143d465284f50 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 21 Jan 2018 19:23:24 +0100
Subject: [PATCH 14/14] Make some names more explicit

---
 src/Cat/Categories/Cat.agda | 46 ++++++++++++++++++++++++++-----------
 1 file changed, 32 insertions(+), 14 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index b25eb54..796379b 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -24,9 +24,9 @@ open Functor
 open Category
 module _ {ℓ ℓ' : Level} {A B : Category ℓ ℓ'} where
   lift-eq-functors : {f g : Functor A B}
-    → (eq* : Functor.func* f ≡ Functor.func* g)
-    → (eq→ : PathP (λ i → ∀ {x y} → Arrow A x y → Arrow B (eq* i x) (eq* i y))
-    (func→ f) (func→ g))
+    → (eq* : 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
@@ -34,8 +34,8 @@ module _ {ℓ ℓ' : Level} {A B : Category ℓ ℓ'} where
     → (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))
+      → 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 }
 
@@ -43,8 +43,25 @@ module _ {ℓ ℓ' : Level} {A B : Category ℓ ℓ'} where
 module _ {ℓ ℓ' : Level} where
   private
     module _ {A B C D : Category ℓ ℓ'} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
-      postulate assc : h ∘f (g ∘f f) ≡ (h ∘f g) ∘f f
-      -- assc = lift-eq-functors refl refl {!refl!} λ i j → {!!}
+      eq* : func* (h ∘f (g ∘f f)) ≡ func* ((h ∘f g) ∘f f)
+      eq* = refl
+      eq→ : PathP
+        (λ i → {x y : A .Object} → A .Arrow x y → D .Arrow (eq* i x) (eq* i y))
+        (func→ (h ∘f (g ∘f f))) (func→ ((h ∘f g) ∘f f))
+      eq→ = refl
+      id-l = (h ∘f (g ∘f f)) .ident -- = func→ (h ∘f (g ∘f f)) (𝟙 A) ≡ 𝟙 D
+      id-r = ((h ∘f g) ∘f f) .ident -- = func→ ((h ∘f g) ∘f f) (𝟙 A) ≡ 𝟙 D
+      postulate eqI : PathP
+                 (λ i → ∀ {c : A .Object} → eq→ i (A .𝟙 {c}) ≡ D .𝟙 {eq* i c})
+                 (ident ((h ∘f (g ∘f f))))
+                 (ident ((h ∘f g) ∘f f))
+      postulate eqD : PathP (λ i → { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''}
+                        → eq→ i (A ._⊕_ a' a) ≡ D ._⊕_ (eq→ i a') (eq→ i a))
+                        (distrib (h ∘f (g ∘f f))) (distrib ((h ∘f g) ∘f f))
+      -- eqD = {!!}
+
+      assc : h ∘f (g ∘f f) ≡ (h ∘f g) ∘f f
+      assc = lift-eq-functors eq* eq→ eqI eqD
 
     module _ {A B : Category ℓ ℓ'} {f : Functor A B} where
       lem : (func* f) ∘ (func* (identity {C = A})) ≡ func* f
@@ -71,9 +88,10 @@ module _ {ℓ ℓ' : Level} where
       ; 𝟙 = identity
       ; _⊕_ = _∘f_
       -- What gives here? Why can I not name the variables directly?
-      ; isCategory = {!!}
---      ; assoc = λ {_ _ _ _ f g h} → assc {f = f} {g = g} {h = h}
---      ; ident = ident-r , ident-l
+      ; isCategory = record
+        { assoc = λ {_ _ _ _ f g h} → assc {f = f} {g = g} {h = h}
+        ; ident = ident-r , ident-l
+        }
       }
 
 module _ {ℓ : Level} (C D : Category ℓ ℓ) where
@@ -132,11 +150,11 @@ 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.
-      isUniqL : (Cat ⊕ proj₁) x ≡ x₁
-      isUniqL = lift-eq-functors refl refl {!!} {!!}
+      postulate isUniqL : (Cat ⊕ proj₁) x ≡ x₁
+      -- isUniqL = lift-eq-functors refl refl {!!} {!!}
 
-      isUniqR : (Cat ⊕ proj₂) x ≡ x₂
-      isUniqR = lift-eq-functors refl refl {!!} {!!}
+      postulate isUniqR : (Cat ⊕ proj₂) x ≡ x₂
+      -- isUniqR = lift-eq-functors refl refl {!!} {!!}
 
       isUniq : (Cat ⊕ proj₁) x ≡ x₁ × (Cat ⊕ proj₂) x ≡ x₂
       isUniq = isUniqL , isUniqR