Make properties of a category an instance argument

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}
+      ; isCategory = {!!}
-      ; ident = ident-r , ident-l
+--      ; 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
+    :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₂
     }

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
+  ; isCategory = record { assoc = funExt is-assoc ; ident = funExt ident-l , funExt ident-r }
-  ; ident = funExt ident-l , funExt ident-r
   }

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
-
+open Category
--- Sets are built-in to Agda. The set of all small sets is called Set.
-
-Fun : {ℓ : Level} → ( T U : Set ℓ ) → Set ℓ
-Fun T U = T → U
 
 Sets : {ℓ : Level} → Category (lsuc ℓ) ℓ
 Sets {ℓ} = record
   { Object = Set ℓ
-  ; Arrow = λ T U → Fun {ℓ} T U
+  ; Arrow = λ T U → T → U
-  ; 𝟙 = λ x → x
+  ; 𝟙 = id
-  ; _⊕_  = λ g f x → g ( f x )
+  ; _⊕_ = _∘′_
-  ; assoc = refl
+  ; isCategory = record { assoc = refl ; ident = funExt (λ _ → refl) , funExt (λ _ → refl) }
-  ; ident = funExt (λ x → refl) , funExt (λ x → 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* = λ B → ℂ .Arrow A B
-  ; func→ = λ f g → f ℂ.⊕ g
+  ; func→ = ℂ ._⊕_
-  ; ident = funExt λ _ → snd ℂ.ident
+  ; ident = funExt λ _ → snd ident
-  ; distrib = funExt λ x → sym ℂ.assoc
+  ; 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* = λ A → ℂ .Arrow A B
-  ; func→ = λ f g → g ℂ.⊕ f
+  ; func→ = λ f g → ℂ ._⊕_ g f
-  ; ident = funExt λ x → fst ℂ.ident
+  ; ident = funExt λ x → fst ident
-  ; distrib = funExt λ x → ℂ.assoc
+  ; distrib = funExt λ x → assoc
   }
   where
-    open module ℂ = Category ℂ
+    open IsCategory (ℂ .isCategory)

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 }
+    {{isCategory}} : IsCategory Object Arrow 𝟙 _⊕_
-      → h ⊕ (g ⊕ f) ≡ (h ⊕ g) ⊕ f
-    ident  : { A B : Object } { f : Arrow A B }
-      → f ⊕ 𝟙 ≡ f × 𝟙 ⊕ f ≡ f
   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
+-- Two pairs are equal if their components are equal.
-  catProduct : ∀ {ℓ} (C D : Category ℓ ℓ) → Category ℓ ℓ
+eqpair : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} {a a' : A} {b b' : B}
-  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 : ∀ {ℓ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
+eqpair eqa eqb i = eqa i , eqb i
 
-
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-  -- arrowProduct : ∀ {ℓ} {C D : Category {ℓ} {ℓ}} → (Object C) × (Object D) → (Object C) × (Object D) → Set ℓ
+  private
-  -- arrowProduct = {!!}
+    instance
-
+      _ : IsCategory (ℂ .Object) (flip (ℂ .Arrow)) (ℂ .𝟙) (flip (ℂ ._⊕_))
-  -- Arrows in the product-category
+      _ = record { assoc = sym assoc ; ident = swap ident }
-  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 ℂ
+          open IsCategory (ℂ .isCategory)
+
+  Opposite : Category ℓ ℓ'
+  Opposite =
+    record
+      { Object = ℂ .Object
+      ; Arrow = flip (ℂ .Arrow)
+      ; 𝟙 = ℂ .𝟙
+      ; _⊕_ = flip (ℂ ._⊕_)
+      }
 
 -- A consequence of no-eta-equality; `Opposite-is-involution` is no longer
 -- definitional - i.e.; you must match on the fields:

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
+    ; isCategory = record { assoc = p-assoc ; ident = ident-r , ident-l }
-    ; ident = ident-r , ident-l
     }

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 = {!!}
+    ; isCategory = ?
-    ; ident = {!!}
     }
 
 _⇑_ = Exponential

src/Cat/Cubical.agda

@@ -49,6 +49,5 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
     ; Arrow = Mor
     ; 𝟙 = {!!}
     ; _⊕_ = {!!}
-    ; assoc = {!!}
+    ; isCategory = ?
-    ; ident = {!!}
     }