commit 1be6e06756e0b1e320685649b741ca6eae0f4a66 Author: William Ball Date: Sun Oct 13 19:28:44 2024 -0700 initial commit diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..157baf0 --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ +.DS_Store +.idea +*.log +tmp/ +_build/ diff --git a/README.org b/README.org new file mode 100644 index 0000000..ca2ecf1 --- /dev/null +++ b/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. diff --git a/category.agda-lib b/category.agda-lib new file mode 100644 index 0000000..5ed7200 --- /dev/null +++ b/category.agda-lib @@ -0,0 +1,3 @@ +name: category +depend: standard-library-2.1 +include: src/ diff --git a/src/Category/Category.agda b/src/Category/Category.agda new file mode 100644 index 0000000..95fefea --- /dev/null +++ b/src/Category/Category.agda @@ -0,0 +1,3 @@ +module Category where + +open import Category.Core public diff --git a/src/Category/Constructions/Arrow.agda b/src/Category/Constructions/Arrow.agda new file mode 100644 index 0000000..40e3f33 --- /dev/null +++ b/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₂′ diff --git a/src/Category/Constructions/Arrow/Category.agda b/src/Category/Constructions/Arrow/Category.agda new file mode 100644 index 0000000..9184660 --- /dev/null +++ b/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₂′ diff --git a/src/Category/Constructions/Arrow/Projections.agda b/src/Category/Constructions/Arrow/Projections.agda new file mode 100644 index 0000000..5b0bd4c --- /dev/null +++ b/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 diff --git a/src/Category/Constructions/Opposite.agda b/src/Category/Constructions/Opposite.agda new file mode 100644 index 0000000..1eb4924 --- /dev/null +++ b/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 𝐂 diff --git a/src/Category/Constructions/Product/Category.agda b/src/Category/Constructions/Product/Category.agda new file mode 100644 index 0000000..38964ee --- /dev/null +++ b/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′ + diff --git a/src/Category/Constructions/Product/Projections.agda b/src/Category/Constructions/Product/Projections.agda new file mode 100644 index 0000000..4f6d34e --- /dev/null +++ b/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 diff --git a/src/Category/Constructions/Slice/Category.agda b/src/Category/Constructions/Slice/Category.agda new file mode 100644 index 0000000..a84e5b3 --- /dev/null +++ b/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-∘ diff --git a/src/Category/Constructions/Slice/CompositionFunctor.agda b/src/Category/Constructions/Slice/CompositionFunctor.agda new file mode 100644 index 0000000..1d17a84 --- /dev/null +++ b/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 diff --git a/src/Category/Constructions/Slice/Forgetful.agda b/src/Category/Constructions/Slice/Forgetful.agda new file mode 100644 index 0000000..e4aa8e5 --- /dev/null +++ b/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 diff --git a/src/Category/Constructions/Slice/ToArrow.agda b/src/Category/Constructions/Slice/ToArrow.agda new file mode 100644 index 0000000..d6891d1 --- /dev/null +++ b/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-ˡ _) diff --git a/src/Category/Core.agda b/src/Category/Core.agda new file mode 100644 index 0000000..40b4391 --- /dev/null +++ b/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) diff --git a/src/Category/Definitions.agda b/src/Category/Definitions.agda new file mode 100644 index 0000000..682761f --- /dev/null +++ b/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 diff --git a/src/Category/Instances/Cat.agda b/src/Category/Instances/Cat.agda new file mode 100644 index 0000000..d13da09 --- /dev/null +++ b/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-∘ = {!!} diff --git a/src/Category/Instances/Monoid.agda b/src/Category/Instances/Monoid.agda new file mode 100644 index 0000000..7e8a79d --- /dev/null +++ b/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 diff --git a/src/Category/Instances/One.agda b/src/Category/Instances/One.agda new file mode 100644 index 0000000..24acaf0 --- /dev/null +++ b/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 diff --git a/src/Category/Instances/Preorder.agda b/src/Category/Instances/Preorder.agda new file mode 100644 index 0000000..ff8133a --- /dev/null +++ b/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 diff --git a/src/Category/Instances/Rel-Type-Functor.agda b/src/Category/Instances/Rel-Type-Functor.agda new file mode 100644 index 0000000..df81f48 --- /dev/null +++ b/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 diff --git a/src/Category/Instances/Rel-op-functor.agda b/src/Category/Instances/Rel-op-functor.agda new file mode 100644 index 0000000..84cf369 --- /dev/null +++ b/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) diff --git a/src/Category/Instances/Rel.agda b/src/Category/Instances/Rel.agda new file mode 100644 index 0000000..187e10a --- /dev/null +++ b/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 diff --git a/src/Category/Instances/Two.agda b/src/Category/Instances/Two.agda new file mode 100644 index 0000000..fb42db4 --- /dev/null +++ b/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 diff --git a/src/Category/Instances/TypeCategory.agda b/src/Category/Instances/TypeCategory.agda new file mode 100644 index 0000000..18e72cc --- /dev/null +++ b/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 diff --git a/src/Category/Properties.agda b/src/Category/Properties.agda new file mode 100644 index 0000000..0331007 --- /dev/null +++ b/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 𝟙 ⟩ + 𝟙 + ∎