initial commit

.gitignore

@@ -0,0 +1,5 @@
+.DS_Store
+.idea
+*.log
+tmp/
+_build/

README.org

@@ -0,0 +1,9 @@
+#+title: Category-Theory
+
+This is an attempt at formalizing basic category theory in Agda by myself as practice to better understand both Agda and category theory.
+
+My main category theory reference is /Category Theory/ by Steve Awodey (supplemented by MacLane and /Categories in Context/ by Emily Riehl).
+
+My main reference for Agda is [[https://plfa.github.io/][Programming Languages Foundations in Agda]] and browsing [[https://agda.github.io/agda-stdlib/v2.1.1/][the standard library]].
+
+Use [[https://github.com/agda/agda-categories][this excellent library]] for any real category theory work.

category.agda-lib

@@ -0,0 +1,3 @@
+name: category
+depend: standard-library-2.1
+include: src/

src/Category/Category.agda

@@ -0,0 +1,3 @@
+module Category where
+
+open import Category.Core public

src/Category/Constructions/Arrow.agda

@@ -0,0 +1,42 @@
+open import Category.Core
+open import Level using (Level)
+open import Data.Product using (_,_; Σ-syntax; _×_)
+open import Relation.Binary using (IsEquivalence)
+open IsEquivalence
+
+module Category.Constructions.Arrow.Category {ℓ₁ ℓ₂ ℓ₃ : Level} (𝐂 : Category {ℓ₁} {ℓ₂} {ℓ₃}) where
+
+open Category 𝐂
+
+_⃑ : Category
+_⃑ .Obj = Σ[ A ∈ Obj ] Σ[ B ∈ Obj ] Hom A B
+_⃑ .Hom (A , B , f) (A′ , B′ , f′)
+    = Σ[ g₁ ∈ Hom A A′ ] Σ[ g₂ ∈ Hom B B′ ] g₂ ∘ f ≈ f′ ∘ g₁
+_⃑ ._≈_ ( g₁ , g₂ , _) ( h₁ , h₂ , _) = g₁ ≈ h₁ × g₂ ≈ h₂
+_⃑ .equiv = record
+    { refl = refl equiv , refl equiv
+    ; sym = λ (g₁ , g₂) → sym equiv g₁ , sym equiv g₂
+    ; trans = λ (g₁ , g₂) (h₁ , h₂) → trans equiv g₁ h₁ , trans equiv g₂ h₂
+    }
+_⃑ ._∘_ {A , A′ , a} {B , B′ , b} {C , C′ , c} (g₁ , g₂ , g₂∘b≈c∘g₁) (h₁ , h₂ , h₂∘a≈b∘h₁)
+    = g₁ ∘ h₁ , g₂ ∘ h₂ , (
+        begin
+          (g₂ ∘ h₂) ∘ a
+        ≈⟨ sym equiv (assoc g₂ h₂ a) ⟩
+          g₂ ∘ (h₂ ∘ a)
+        ≈⟨ ≈-resp-∘ (refl equiv) h₂∘a≈b∘h₁ ⟩
+          g₂ ∘ (b ∘ h₁)
+        ≈⟨ assoc g₂ b h₁ ⟩
+          (g₂ ∘ b) ∘ h₁
+        ≈⟨ ≈-resp-∘ g₂∘b≈c∘g₁ (refl equiv) ⟩
+          (c ∘ g₁) ∘ h₁
+        ≈⟨ sym equiv (assoc c g₁ h₁) ⟩
+          c ∘ (g₁ ∘ h₁)
+        ∎)
+    where open import Relation.Binary.Reasoning.Setoid
+                (record { Carrier = Hom A C′ ; _≈_ = _≈_ ; isEquivalence = equiv })
+_⃑ .𝟙 {A , B , f} = (𝟙 , 𝟙 , trans equiv (identity-ˡ f) (sym equiv (identity-ʳ f)))
+_⃑ .assoc (f , f′ , _) (g , g′ , _) (h , h′ , _) = assoc f g h , assoc f′ g′ h′
+_⃑ .identity-ˡ (f , f′ , _) = identity-ˡ f , identity-ˡ f′
+_⃑ .identity-ʳ (f , f′ , _) = identity-ʳ f , identity-ʳ f′
+_⃑ .≈-resp-∘ (f₁≈f₁′ , g₁≈g₁′) (f₂≈f₂′ , g₂≈g₂′) = ≈-resp-∘ f₁≈f₁′ f₂≈f₂′ , ≈-resp-∘ g₁≈g₁′ g₂≈g₂′

src/Category/Constructions/Arrow/Category.agda

@@ -0,0 +1,40 @@
+open import Category.Core
+open import Level using (Level)
+open import Data.Product using (_,_; Σ-syntax; _×_)
+
+module Category.Constructions.Arrow.Category {ℓ₁ ℓ₂ ℓ₃ : Level} (𝐂 : Category {ℓ₁} {ℓ₂} {ℓ₃}) where
+
+open Category 𝐂
+open HomReasoning
+open Eq
+
+_⃑ : Category
+_⃑ .Obj = Σ[ A ∈ Obj ] Σ[ B ∈ Obj ] Hom A B
+_⃑ .Hom (A , B , f) (A′ , B′ , f′)
+    = Σ[ g₁ ∈ Hom A A′ ] Σ[ g₂ ∈ Hom B B′ ] g₂ ∘ f ≈ f′ ∘ g₁
+_⃑ ._≈_ ( g₁ , g₂ , _) ( h₁ , h₂ , _) = g₁ ≈ h₁ × g₂ ≈ h₂
+_⃑ .equiv = record
+    { refl = refl , refl
+    ; sym = λ (g₁ , g₂) → sym g₁ , sym g₂
+    ; trans = λ (g₁ , g₂) (h₁ , h₂) → trans g₁ h₁ , trans g₂ h₂
+    }
+_⃑ ._∘_ {A , A′ , a} {B , B′ , b} {C , C′ , c} (g₁ , g₂ , g₂∘b≈c∘g₁) (h₁ , h₂ , h₂∘a≈b∘h₁)
+    = g₁ ∘ h₁ , g₂ ∘ h₂ , (
+        begin
+          (g₂ ∘ h₂) ∘ a
+        ≈⟨ sym (assoc g₂ h₂ a) ⟩
+          g₂ ∘ (h₂ ∘ a)
+        ≈⟨ ≈-resp-∘ refl h₂∘a≈b∘h₁ ⟩
+          g₂ ∘ (b ∘ h₁)
+        ≈⟨ assoc g₂ b h₁ ⟩
+          (g₂ ∘ b) ∘ h₁
+        ≈⟨ ≈-resp-∘ g₂∘b≈c∘g₁ refl ⟩
+          (c ∘ g₁) ∘ h₁
+        ≈⟨ sym (assoc c g₁ h₁) ⟩
+          c ∘ (g₁ ∘ h₁)
+        ∎)
+_⃑ .𝟙 {A , B , f} = (𝟙 , 𝟙 , trans (identity-ˡ f) (sym (identity-ʳ f)))
+_⃑ .assoc (f , f′ , _) (g , g′ , _) (h , h′ , _) = assoc f g h , assoc f′ g′ h′
+_⃑ .identity-ˡ (f , f′ , _) = identity-ˡ f , identity-ˡ f′
+_⃑ .identity-ʳ (f , f′ , _) = identity-ʳ f , identity-ʳ f′
+_⃑ .≈-resp-∘ (f₁≈f₁′ , g₁≈g₁′) (f₂≈f₂′ , g₂≈g₂′) = ≈-resp-∘ f₁≈f₁′ f₂≈f₂′ , ≈-resp-∘ g₁≈g₁′ g₂≈g₂′

src/Category/Constructions/Arrow/Projections.agda

@@ -0,0 +1,24 @@
+open import Category.Core
+open import Level using (Level)
+open Functor
+open import Data.Product using (proj₁ ; proj₂)
+open import Function renaming (_∘_ to _∙_)
+
+open import Category.Constructions.Arrow.Category
+
+module Category.Constructions.Arrow.Projections {ℓ₁ ℓ₂ ℓ₃ : Level} (𝐂 : Category {ℓ₁} {ℓ₂} {ℓ₃}) where
+
+open Category 𝐂
+open HomReasoning.Eq
+
+dom : Functor (𝐂 ⃑) 𝐂
+dom .F₀ = proj₁
+dom .F₁ = proj₁
+dom .fmap-resp-𝟙 = refl
+dom .fmap-resp-∘ _ _ = refl
+
+cod : Functor (𝐂 ⃑) 𝐂
+cod .F₀ = proj₁ ∙ proj₂
+cod .F₁ = proj₁ ∙ proj₂
+cod .fmap-resp-𝟙 = refl
+cod .fmap-resp-∘ _ _ = refl

src/Category/Constructions/Opposite.agda

@@ -0,0 +1,22 @@
+open import Category.Core
+open import Level using (Level; _⊔_)
+open import Relation.Binary using (IsEquivalence)
+open import Function using (flip)
+open IsEquivalence
+
+module Category.Constructions.Opposite where
+
+_ᵒᵖ : {ℓ₁ ℓ₂ ℓ₃ : Level} → Category {ℓ₁} {ℓ₂} {ℓ₃} → Category
+𝐂 ᵒᵖ = record
+        { Obj = Obj
+        ; Hom = flip Hom
+        ; _≈_ = _≈_
+        ; _∘_ = flip _∘_
+        ; 𝟙 = 𝟙
+        ; assoc = λ f g h → sym equiv (assoc h g f)
+        ; identity-ˡ = identity-ʳ
+        ; identity-ʳ = identity-ˡ
+        ; equiv = equiv
+        ; ≈-resp-∘ = flip ≈-resp-∘
+        }
+        where open Category 𝐂

src/Category/Constructions/Product/Category.agda

@@ -0,0 +1,33 @@
+open import Category.Core
+open import Data.Product using (_×_; _,_; zip)
+open import Level using (Level; _⊔_)
+open import Relation.Binary using (IsEquivalence)
+open IsEquivalence
+
+open Category
+
+module Category.Constructions.Product.Category
+       {ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level}
+       (𝐂 : Category {ℓ₁} {ℓ₂} {ℓ₃})
+       (𝐃 : Category {ℓ₄} {ℓ₅} {ℓ₆}) where
+
+private
+  module C = Category 𝐂
+  module D = Category 𝐃
+
+_×ᶜ_ : Category
+_×ᶜ_ .Obj = C.Obj × D.Obj
+_×ᶜ_ .Hom (A , A′) (B , B′) = C.Hom A B × D.Hom A′ B′
+_×ᶜ_ ._≈_ (f , f′) (g , g′) = f C.≈ g × f′ D.≈ g′
+_×ᶜ_ ._∘_ = zip C._∘_ D._∘_
+_×ᶜ_ .𝟙 = C.𝟙 , D.𝟙
+_×ᶜ_ .assoc (f , f′) (g , g′) (h , h′) = C.assoc f g h , D.assoc f′ g′ h′
+_×ᶜ_ .identity-ˡ (f , f′) = C.identity-ˡ f , D.identity-ˡ f′
+_×ᶜ_ .identity-ʳ (f , f′) = C.identity-ʳ f , D.identity-ʳ f′
+_×ᶜ_ .equiv = record
+  { refl = refl C.equiv , refl D.equiv
+  ; sym = λ (f , f′) → sym C.equiv f , sym D.equiv f′
+  ; trans = λ (f≈g , f′≈g′) (g≈h , g′≈h′) → trans C.equiv f≈g g≈h , trans D.equiv f′≈g′ g′≈h′
+  }
+_×ᶜ_ .≈-resp-∘ (f≈g , f′≈g′) (g≈h , g′≈h′) = C.≈-resp-∘ f≈g g≈h , D.≈-resp-∘ f′≈g′ g′≈h′
+

src/Category/Constructions/Product/Projections.agda

@@ -0,0 +1,31 @@
+open import Category.Core
+open import Level using (Level)
+open import Data.Product renaming (proj₁ to π₁; proj₂ to π₂)
+open import Relation.Binary using (IsEquivalence)
+open IsEquivalence
+
+module Category.Constructions.Product.Projections
+       {ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level}
+       (𝐂 : Category {ℓ₁} {ℓ₂} {ℓ₃})
+       (𝐃 : Category {ℓ₄} {ℓ₅} {ℓ₆}) where
+
+open import Category.Constructions.Product.Category
+open Functor
+
+open Category (𝐂 ×ᶜ 𝐃)
+
+private
+  module C = Category 𝐂
+  module D = Category 𝐃
+
+proj₁ : Functor (𝐂 ×ᶜ 𝐃) 𝐂
+proj₁ .F₀ = π₁
+proj₁ .F₁ = π₁
+proj₁ .fmap-resp-𝟙 = refl C.equiv
+proj₁ .fmap-resp-∘ _ _ = refl C.equiv
+
+proj₂ : Functor (𝐂 ×ᶜ 𝐃) 𝐃
+proj₂ .F₀ = π₂
+proj₂ .F₁ = π₂
+proj₂ .fmap-resp-𝟙 = refl D.equiv
+proj₂ .fmap-resp-∘ _ _ = refl D.equiv

src/Category/Constructions/Slice/Category.agda

@@ -0,0 +1,40 @@
+open import Category.Core
+open import Level using (Level)
+open import Data.Product using (_,_; Σ-syntax; _×_)
+open import Relation.Binary using (IsEquivalence)
+open IsEquivalence
+
+module Category.Constructions.Slice.Category
+       {ℓ₁ ℓ₂ ℓ₃ : Level}
+       (𝐂 : Category {ℓ₁} {ℓ₂} {ℓ₃})
+       (C : Category.Obj 𝐂) where
+
+open Category 𝐂
+
+_/_ : Category
+_/_ .Category.Obj = Σ[ A ∈ Obj ] Hom A C
+_/_ .Category.Hom (X , f) (X′ , f′) = Σ[ a ∈ Hom X X′ ] f′ ∘ a ≈ f
+_/_ .Category._≈_ (a , _) (b , _) = a ≈ b
+_/_ .Category._∘_ {(A , a)} {(B , b)} {(D , d)} (g , d∘g≈b) (f , b∘f≈a)
+    = (g ∘ f) , (
+      begin
+        d ∘ (g ∘ f)
+      ≈⟨ assoc d g f ⟩
+        (d ∘ g) ∘ f
+      ≈⟨ ≈-resp-∘ d∘g≈b (refl equiv) ⟩
+        b ∘ f
+      ≈⟨ b∘f≈a ⟩
+        a
+      ∎)
+    where open import Relation.Binary.Reasoning.Setoid
+               (record { Carrier = Hom A C ; _≈_ = _≈_ ; isEquivalence = equiv })
+_/_ .Category.𝟙 {(_ , f)}= 𝟙 , identity-ʳ f
+_/_ .Category.assoc (f , _) (g , _) (h , _) = assoc f g h
+_/_ .Category.identity-ˡ (f , _) = identity-ˡ f
+_/_ .Category.identity-ʳ (f , _) = identity-ʳ f
+_/_ .Category.equiv = record
+                       { refl = refl equiv
+                       ; sym = sym equiv
+                       ; trans = trans equiv
+                       }
+_/_ .Category.≈-resp-∘ = ≈-resp-∘

src/Category/Constructions/Slice/CompositionFunctor.agda

@@ -0,0 +1,30 @@
+open import Category.Core
+open import Level using (Level)
+open import Category.Constructions.Slice.Category
+open import Data.Product using (_,_)
+
+module Category.Constructions.Slice.CompositionFunctor
+       {ℓ₁ ℓ₂ ℓ₃ : Level}
+       (𝐂 : Category {ℓ₁} {ℓ₂} {ℓ₃})
+       (C D : Category.Obj 𝐂) where
+
+module 𝐂/C = Category (𝐂 / C)
+module 𝐂/D = Category (𝐂 / D)
+
+open Category 𝐂
+open HomReasoning
+open Eq
+
+open Functor
+comp : Hom C D → Functor (𝐂 / C) (𝐂 / D)
+comp g .F₀ (A , f) = (A , g ∘ f)
+comp g .F₁ {(A , a)} {(B , b)} (f , b∘f≈a) = f , (
+     begin
+        (g ∘ b) ∘ f
+     ≈⟨ sym (assoc g b f) ⟩
+        g ∘ (b ∘ f)
+     ≈⟨ ≈-resp-∘ refl b∘f≈a ⟩
+        g ∘ a
+     ∎)
+comp g .fmap-resp-𝟙 = refl
+comp g .fmap-resp-∘ _ _ = refl

src/Category/Constructions/Slice/Forgetful.agda

@@ -0,0 +1,21 @@
+open import Category.Core
+open import Level using (Level)
+open import Category.Constructions.Slice.Category
+open import Data.Product using (_,_; proj₁)
+
+module Category.Constructions.Slice.Forgetful
+       {ℓ₁ ℓ₂ ℓ₃ : Level}
+       (𝐂 : Category {ℓ₁} {ℓ₂} {ℓ₃})
+       (C : Category.Obj 𝐂) where
+
+module 𝐂/C = Category (𝐂 / C)
+
+open Category 𝐂
+open HomReasoning.Eq
+open Functor
+
+forget : Functor (𝐂 / C) 𝐂
+forget .F₀ = proj₁
+forget .F₁ = proj₁
+forget .fmap-resp-𝟙 = refl
+forget .fmap-resp-∘ _ _ = refl

src/Category/Constructions/Slice/ToArrow.agda

@@ -0,0 +1,24 @@
+open import Category.Core
+open import Level using (Level)
+open import Category.Constructions.Slice.Category
+open import Category.Constructions.Arrow.Category
+open import Data.Product using (_,_; Σ-syntax)
+
+module Category.Constructions.Slice.ToArrow
+       {ℓ₁ ℓ₂ ℓ₃ : Level}
+       (𝐂 : Category {ℓ₁} {ℓ₂} {ℓ₃})
+       (C : Category.Obj 𝐂) where
+
+module 𝐂/C = Category (𝐂 / C)
+module 𝐂⃑ = Category (𝐂 ⃑)
+
+open Category 𝐂
+open HomReasoning
+open Eq
+
+open Functor
+to-arrow : Functor (𝐂 / C) (𝐂 ⃑)
+to-arrow .F₀ (A , a) = A , C , a
+to-arrow .F₁ {(_ , a)} (f , b∘f≈a) = f , 𝟙 , trans (identity-ˡ a) (sym b∘f≈a)
+to-arrow .fmap-resp-𝟙 = refl , refl
+to-arrow .fmap-resp-∘ _ _ = refl , sym (identity-ˡ _)

src/Category/Core.agda

@@ -0,0 +1,39 @@
+module Category.Core where
+
+open import Level using (suc; _⊔_; Level)
+open import Relation.Binary using (Rel; IsEquivalence; Setoid)
+
+record Category {ℓ₁ ℓ₂ ℓ₃} : Set (suc (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
+  infix 4 _≈_
+  infix 9 _∘_
+  field
+    Obj : Set ℓ₁
+    Hom : Rel Obj ℓ₂
+    _≈_ : ∀ {A B} → Rel (Hom A B) ℓ₃
+    _∘_ : ∀ {A B C} → Hom B C → Hom A B → Hom A C
+    𝟙 : ∀ {A} → Hom A A
+    assoc : ∀ {A B C D} → (f : Hom C D) → (g : Hom B C) → (h : Hom A B) → f ∘ (g ∘ h) ≈ (f ∘ g) ∘ h
+    identity-ˡ : ∀ {A B} → (f : Hom A B) → 𝟙 ∘ f ≈ f
+    identity-ʳ : ∀ {A B} → (f : Hom A B) → f ∘ 𝟙 ≈ f
+    equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
+    ≈-resp-∘ : ∀ {A B C} → {f g : Hom B C} → {h i : Hom A B} → f ≈ g → h ≈ i → f ∘ h ≈ g ∘ i
+
+  hom-setoid : ∀ {A B} → Setoid _ _
+  hom-setoid {A} {B} = record
+    { Carrier = Hom A B
+    ; _≈_ = _≈_
+    ; isEquivalence = equiv }
+
+  module HomReasoning {A B : Obj} where
+    open import Relation.Binary.Reasoning.Setoid (hom-setoid {A} {B}) public
+    module Eq = IsEquivalence (Setoid.isEquivalence (hom-setoid {A} {B}))
+
+record Functor {ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆} (𝐂 : Category {ℓ₁} {ℓ₂} {ℓ₃}) (𝐃 : Category {ℓ₄} {ℓ₅} {ℓ₆}) : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄ ⊔ ℓ₅ ⊔ ℓ₆) where
+  open Category
+  open Category 𝐂 renaming (_∘_ to _∘𝐂_; 𝟙 to 𝟙𝐂; _≈_ to _≈𝐂_)
+  open Category 𝐃 renaming (_∘_ to _∘𝐃_; 𝟙 to 𝟙𝐃; _≈_ to _≈𝐃_)
+  field
+    F₀ : Obj 𝐂 → Obj 𝐃
+    F₁ : ∀ {A B} → Hom 𝐂 A B → Hom 𝐃 (F₀ A) (F₀ B)
+    fmap-resp-𝟙 : ∀ {A} → F₁ (𝟙𝐂 {A}) ≈𝐃 𝟙𝐃 {F₀ A}
+    fmap-resp-∘ : ∀ {A B C} → ∀ (f : Hom 𝐂 B C) → ∀ (g : Hom 𝐂 A B) → F₁ (f ∘𝐂 g) ≈𝐃 (F₁ f) ∘𝐃 (F₁ g)

src/Category/Definitions.agda

@@ -0,0 +1,47 @@
+open import Category.Core
+open import Data.Product using (_×_; Σ-syntax; ∃-syntax; _,_)
+
+module Category.Definitions {ℓ₁ ℓ₂ ℓ₃} (𝐂 : Category {ℓ₁} {ℓ₂} {ℓ₃}) where
+
+open Category 𝐂
+
+private
+  variable
+    a b : Obj
+    f : Hom a b
+    g : Hom b a
+
+IsLeftInverse : (f : Hom a b) → (g : Hom b a) → Set _
+IsLeftInverse f g = g ∘ f ≈ 𝟙
+
+IsRightInverse : (f : Hom a b) → (g : Hom b a) → Set _
+IsRightInverse f g = f ∘ g ≈ 𝟙
+
+IsInverse : (f : Hom a b) → (g : Hom b a) → Set _
+IsInverse f g = IsLeftInverse f g × IsRightInverse f g
+
+inverse-unique : (f : Hom a b) → (g h : Hom b a) → IsInverse f g → IsInverse f h → g ≈ h
+inverse-unique f g h (gf≈1 , fg≈1) (hf≈1 , fh≈1) =
+  begin
+    g
+  ≈⟨ sym (identity-ʳ g) ⟩
+    g ∘ 𝟙
+  ≈⟨ sym (≈-resp-∘ refl fh≈1) ⟩
+    g ∘ (f ∘ h)
+  ≈⟨ assoc g f h ⟩
+    (g ∘ f) ∘ h
+  ≈⟨ ≈-resp-∘ gf≈1 refl ⟩
+    𝟙 ∘ h
+  ≈⟨ identity-ˡ h ⟩
+    h
+  ∎
+  where open HomReasoning
+
+IsIsomorphism : (f : Hom a b) → Set _
+IsIsomorphism f = ∃[ g ] IsInverse f g
+
+_⁻¹ : (f : Hom a b) → {IsIsomorphism f} → Hom b a
+_⁻¹ f {g , _} = g
+
+_≅_ : Obj → Obj → Set _
+a ≅ b = Σ[ f ∈ Hom a b ] IsIsomorphism f

src/Category/Instances/Cat.agda

@@ -0,0 +1,29 @@
+open import Level using (Level)
+-- open import Category.Core
+-- open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+-- open import Data.Product using (_×_; Σ-syntax; _,_)
+-- open Category
+-- open Functor
+
+module Category.Instances.Cat {ℓ₁ ℓ₂ ℓ₃ : Level} where
+
+-- Cat : Category
+-- Cat .Obj = Category {ℓ₁} {ℓ₂} {ℓ₃}
+-- Cat .Hom 𝐂 𝐃 = Functor 𝐂 𝐃
+-- -- Cat ._≈_ {𝐂} {𝐃} 𝐅₁ 𝐅₂ = (∀ a → F₀ 𝐅₁ a ≡ F₀ 𝐅₂ a) × (∀ f → (_≈_ 𝐃) (F₁ 𝐅₁ f) {!!})
+-- Cat ._≈_ {𝐂} {𝐃} 𝐅₁ 𝐅₂ = Σ[ h ∈ (∀ a → F₀ 𝐅₁ a ≡ F₀ 𝐅₂ a) ]
+--     ∀ {a b : Obj 𝐂} → ∀ (f : Hom 𝐂 a b) → {!!}
+--     where
+--         transport : (a b : Obj 𝐂)
+--                   → (F₀ 𝐅₁ a ≡ F₀ 𝐅₂ a)
+--                   → (F₀ 𝐅₁ b ≡ F₀ 𝐅₂ b)
+--                   → (Hom 𝐃 (F₀ 𝐅₁ a) (F₀ 𝐅₁ b))
+--                   → (Hom 𝐃 (F₀ 𝐅₂ a) (F₀ 𝐅₂ b))
+--         transport a b h₁ h₂ H = {!!}
+-- Cat ._∘_ = {!!}
+-- Cat .𝟙 = {!!}
+-- Cat .assoc = {!!}
+-- Cat .identity-ˡ = {!!}
+-- Cat .identity-ʳ = {!!}
+-- Cat .equiv = {!!}
+-- Cat .≈-resp-∘ = {!!}

src/Category/Instances/Monoid.agda

@@ -0,0 +1,21 @@
+open import Category.Core
+open Category
+
+open import Algebra using (Monoid)
+open import Data.Unit using (⊤; tt)
+
+module Category.Instances.Monoid {c ℓ} (M : Monoid c ℓ) where
+
+open Monoid M renaming (Carrier to S; _≈_ to _M≈_; assoc to Massoc)
+
+MonoidCat : Category
+MonoidCat .Obj = ⊤
+MonoidCat .Hom tt tt = S
+MonoidCat ._≈_ = _M≈_
+MonoidCat ._∘_ = _∙_
+MonoidCat .𝟙 = ε
+MonoidCat .assoc f g h = sym (Massoc f g h)
+MonoidCat .identity-ˡ = identityˡ
+MonoidCat .identity-ʳ = identityʳ
+MonoidCat .equiv = isEquivalence
+MonoidCat .≈-resp-∘ = ∙-cong

src/Category/Instances/One.agda

@@ -0,0 +1,24 @@
+open import Category.Core
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Data.Unit
+
+open Category
+
+module Category.Instances.One where
+
+One : Category
+Obj One = ⊤
+Hom One = λ _ _ → ⊤
+_≈_ One = _≡_
+_∘_ One = λ _ _ → tt
+𝟙 One = tt
+assoc One = λ _ _ _ → refl
+identity-ˡ One = λ _ → refl
+identity-ʳ One = λ _ → refl
+equiv One = record
+  { refl = refl
+  ; sym = sym
+  ; trans = trans
+  }
+≈-resp-∘ One refl refl = refl

src/Category/Instances/Preorder.agda

@@ -0,0 +1,25 @@
+open import Category.Core
+open Category
+
+open import Relation.Binary using (Preorder; IsEquivalence)
+open import Data.Unit using (⊤; tt)
+
+module Category.Instances.Preorder {c ℓ₁ ℓ₂} (P : Preorder c ℓ₁ ℓ₂) where
+
+open Preorder P renaming (Carrier to S)
+
+PreorderCat : Category
+PreorderCat .Obj = S
+PreorderCat .Hom a b = a ≲ b
+PreorderCat ._≈_ _ _ = ⊤
+PreorderCat ._∘_ a≲b b≲c = trans b≲c a≲b
+PreorderCat .𝟙 = reflexive (IsEquivalence.refl isEquivalence)
+PreorderCat .assoc _ _ _ = tt
+PreorderCat .identity-ˡ _ = tt
+PreorderCat .identity-ʳ _ = tt
+PreorderCat .equiv = record
+                      { refl = tt
+                      ; sym = λ _ → tt
+                      ; trans = λ _ _ → tt
+                      }
+PreorderCat .≈-resp-∘ _ _ = tt

src/Category/Instances/Rel-Type-Functor.agda

@@ -0,0 +1,18 @@
+open import Category.Core
+open import Level using (Level; Lift; lift)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+open import Data.Product using (_,_; proj₁; proj₂)
+
+module Category.Instances.Rel-Type-Functor {ℓ : Level} where
+
+open import Category.Instances.Rel {ℓ} {ℓ}
+open import Category.Instances.TypeCategory {ℓ}
+
+open Functor
+
+Type→Rel : Functor TypeCat RelCat
+Type→Rel .F₀ A = A
+Type→Rel .F₁ f a b = (f a ≡ b)
+Type→Rel .fmap-resp-𝟙 = lift , Lift.lower
+Type→Rel .fmap-resp-∘ _ g .proj₁ {a} h = g a , refl , h
+Type→Rel .fmap-resp-∘ _ _ .proj₂ (_ , refl , refl) = refl

src/Category/Instances/Rel-op-functor.agda

@@ -0,0 +1,20 @@
+open import Category.Core
+open import Level using (Level; lift)
+open import Data.Product using (_,_; proj₁; proj₂)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+
+module Category.Instances.Rel-op-functor {ℓ₁ ℓ₂ : Level} where
+
+open import Category.Instances.Rel {ℓ₁} {ℓ₂}
+open import Category.Constructions.Opposite
+
+open Functor
+open Category RelCat
+
+Relᵒᵖ→Rel : Functor (RelCat ᵒᵖ) RelCat
+Relᵒᵖ→Rel .F₀ A = A
+Relᵒᵖ→Rel .F₁ R a b = R b a
+Relᵒᵖ→Rel .fmap-resp-𝟙 .proj₁ (lift refl) = lift refl
+Relᵒᵖ→Rel .fmap-resp-𝟙 .proj₂ (lift refl) = lift refl
+Relᵒᵖ→Rel .fmap-resp-∘ R S .proj₁ (b , Rcb , Sba) = b , (Sba , Rcb)
+Relᵒᵖ→Rel .fmap-resp-∘ R S .proj₂ (b , Sba , Rcb) = b , (Rcb , Sba)

src/Category/Instances/Rel.agda

@@ -0,0 +1,30 @@
+open import Category.Core
+open import Level using (suc; _⊔_; Lift; lift)
+open import Relation.Binary using (IsEquivalence; REL; _⇔_; _⇒_)
+open import Function using (id) renaming (_∘_ to _∙_)
+open import Data.Product using (_×_; ∃-syntax; _,_; proj₁; proj₂)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+
+open Category
+open IsEquivalence hiding (refl)
+
+module Category.Instances.Rel {ℓ₁ ℓ₂} where
+
+RelCat : Category
+RelCat .Obj = Set (ℓ₁)
+RelCat .Hom A B = REL A B (ℓ₁ ⊔ ℓ₂)
+RelCat ._≈_ R S = R ⇔ S
+RelCat ._∘_ R S a c = ∃[ b ] S a b × R b c
+RelCat .𝟙 a₁ a₂ = Lift (ℓ₁ ⊔ ℓ₂) (a₁ ≡ a₂)
+RelCat .assoc R S T .proj₁ {a} {d} (c , (b , Tab , Sdc) , Rcd) = b , Tab , c , Sdc , Rcd
+RelCat .assoc R S T .proj₂ {a} {d} (b , Tab , c , Sbc , Rcd) = c , (b , Tab , Sbc) , Rcd
+RelCat .identity-ˡ R .proj₁ (_ , Rab , lift refl) = Rab
+RelCat .identity-ˡ R .proj₂ {_} {b} Rab = b , Rab , lift refl
+RelCat .identity-ʳ R .proj₁ (_ , lift refl , Rab) = Rab
+RelCat .identity-ʳ R .proj₂ {a} Rab = a , lift refl , Rab
+RelCat .equiv .IsEquivalence.refl = (λ Rab → Rab) , (λ Rab → Rab)
+RelCat .equiv .sym (R⇒S , S⇒R) = S⇒R , R⇒S
+RelCat .equiv .trans (R⇒S , S⇒R) (S⇒T , T⇒S) .proj₁ Rab = S⇒T (R⇒S Rab)
+RelCat .equiv .trans (R⇒S , S⇒R) (S⇒T , T⇒S) .proj₂ Tcd = S⇒R (T⇒S Tcd)
+RelCat .≈-resp-∘ (f⇒g , g⇒f) (h⇒i , i⇒h) .proj₁ (b , hab , fbc) = b , h⇒i hab , f⇒g fbc
+RelCat .≈-resp-∘ (f⇒g , g⇒f) (h⇒i , i⇒h) .proj₂ (b , iab , gbc) = b , i⇒h iab , g⇒f gbc

src/Category/Instances/Two.agda

@@ -0,0 +1,40 @@
+open import Category.Core
+open import Data.Bool
+open import Data.Unit using (⊤; tt)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
+open import Relation.Binary.Structures using (IsEquivalence)
+
+open Category
+
+module Category.Instances.Two where
+
+Two : Category
+Obj Two = Bool
+Hom Two false false = ⊤
+Hom Two false true = ⊥
+Hom Two true _ = ⊤
+_≈_ Two = _≡_
+_∘_ Two {false} {false} {false} _ _ = tt
+_∘_ Two {true} {false} {false} _ _ = tt
+_∘_ Two {true} {true} {false} _ _ = tt
+_∘_ Two {true} {true} {true} _ _ = tt
+𝟙 Two {false} = tt
+𝟙 Two {true} = tt
+assoc Two {false} {false} {false} {false} _ _ _ = refl
+assoc Two {true} {false} {false} {false} _ _ _ = refl
+assoc Two {true} {true} {false} {false} _ _ _ = refl
+assoc Two {true} {true} {true} {false} _ _ _ = refl
+assoc Two {true} {true} {true} {true} _ _ _ = refl
+identity-ˡ Two {false} {false} _ = refl
+identity-ˡ Two {true} {false} _ = refl
+identity-ˡ Two {true} {true} _ = refl
+identity-ʳ Two {false} {false} _ = refl
+identity-ʳ Two {true} {false} _ = refl
+identity-ʳ Two {true} {true} _ = refl
+equiv Two = record
+  { refl = refl
+  ; sym = sym
+  ; trans = trans
+  }
+≈-resp-∘ Two refl refl = refl

src/Category/Instances/TypeCategory.agda

@@ -0,0 +1,25 @@
+open import Category.Core
+open import Level using (suc)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Function using (id) renaming (_∘_ to _∙_)
+
+module Category.Instances.TypeCategory {ℓ} where
+
+open Category
+
+TypeCat : Category {suc ℓ}
+Obj TypeCat = Set ℓ
+Hom TypeCat A B = A → B
+_≈_ TypeCat = _≡_
+_∘_ TypeCat = λ f g → f ∙ g
+𝟙 TypeCat = id
+assoc TypeCat = λ f g h → refl
+identity-ˡ TypeCat = λ f → refl
+identity-ʳ TypeCat = λ f → refl
+equiv TypeCat = record
+  { refl = refl
+  ; sym = sym
+  ; trans = trans
+  }
+≈-resp-∘ TypeCat refl refl = refl

src/Category/Properties.agda

@@ -0,0 +1,14 @@
+open import Category.Core
+
+module Category.Properties {ℓ₁ ℓ₂} (𝐂 : Category {ℓ₁} {ℓ₂}) where
+  open Category 𝐂
+
+  unique-identity : ∀ {A} → ∀ (f : Hom A A) → (∀ {B} → ∀ (g : Hom A B) → g ∘ f ≡ g) → f ≡ 𝟙
+  unique-identity f H =
+    begin
+      f
+    ≡⟨ sym (identity-ˡ f) ⟩
+      𝟙 ∘ f
+    ≡⟨ H 𝟙 ⟩
+      𝟙
+    ∎