# HG changeset patch # User Shinji KONO # Date 1696675411 -32400 # Node ID 45de2b31bf02d51a02ac1fdcb3bd2508240ad1c3 # Parent 71049ed05151171a27a73862e51f7e67c052f155 add original library and fix for safe mode diff -r 71049ed05151 -r 45de2b31bf02 CategoryExcercise.agda-lib --- a/CategoryExcercise.agda-lib Thu Jul 20 12:36:15 2023 +0900 +++ b/CategoryExcercise.agda-lib Sat Oct 07 19:43:31 2023 +0900 @@ -1,6 +1,9 @@ -- File generated by Agda-Pkg name: CategoryExcercise -depend: standard-library category-agda +depend: standard-library include: src +flags: + --warning=noUnsupportedIndexedMatch + -- End diff -r 71049ed05151 -r 45de2b31bf02 CategoryExcercise.agda-pkg --- a/CategoryExcercise.agda-pkg Thu Jul 20 12:36:15 2023 +0900 +++ b/CategoryExcercise.agda-pkg Sat Oct 07 19:43:31 2023 +0900 @@ -10,8 +10,10 @@ tested-with: 2.6.2-102d9c8 description: CategoryExcercise is an Agda library ... depend: - - standard-library - - category-agda + - standard-library-2.0 include: - src +flags: + --warning=noUnsupportedIndexedMatch + # End diff -r 71049ed05151 -r 45de2b31bf02 src/CCC.agda --- a/src/CCC.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/CCC.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,11 +1,12 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + open import Level open import Category module CCC where open import HomReasoning -open import cat-utility +open import Definitions open import Relation.Binary.PropositionalEquality diff -r 71049ed05151 -r 45de2b31bf02 src/CCCMonoidal.agda --- a/src/CCCMonoidal.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/CCCMonoidal.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,10 +1,12 @@ +-- {-# OPTIONS --cubical-compatible --safe #-} + open import Level open import Category open import CCC module CCCMonoidal {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( c : CCC A ) where open import HomReasoning -open import cat-utility +open import Definitions open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> ) open import Category.Constructions.Product open import Relation.Binary.PropositionalEquality as ER hiding ( [_] ) diff -r 71049ed05151 -r 45de2b31bf02 src/CatExponetial.agda --- a/src/CatExponetial.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/CatExponetial.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + ---- -- @@ -13,7 +14,7 @@ -- {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ' } open import HomReasoning -open import cat-utility +open import Definitions -- open import Relation.Binary hiding (_⇔_) -- open import Relation.Binary.Core hiding (_⇔_) -- open import Relation.Binary.PropositionalEquality hiding ( [_] ) diff -r 71049ed05151 -r 45de2b31bf02 src/Category.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,95 @@ +{-# OPTIONS --cubical-compatible --safe #-} +module Category where +open import Level +open import Function +open import Relation.Binary +open import Relation.Binary.Core + +record IsCategory {c₁ c₂ ℓ : Level} (Obj : Set c₁) + (Hom : Obj → Obj → Set c₂) + (_≈_ : {A B : Obj} → Rel (Hom A B) ℓ) + (_o_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C) + (Id : {A : Obj} → Hom A A) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where + field + isEquivalence : {A B : Obj} → IsEquivalence {c₂} {ℓ} {Hom A B} _≈_ + identityL : {A B : Obj} → {f : Hom A B} → (Id o f) ≈ f + identityR : {A B : Obj} → {f : Hom A B} → (f o Id) ≈ f + o-resp-≈ : {A B C : Obj} {f g : Hom A B} {h i : Hom B C} → f ≈ g → h ≈ i → (h o f) ≈ (i o g) + associative : {A B C D : Obj} {f : Hom C D} {g : Hom B C} {h : Hom A B} + → (f o (g o h)) ≈ ((f o g) o h) + +record Category c₁ c₂ ℓ : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where + infixr 9 _o_ + infix 4 _≈_ + field + Obj : Set c₁ + Hom : Obj → Obj → Set c₂ + _o_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C + _≈_ : {A B : Obj} → Rel (Hom A B) ℓ + Id : {A : Obj} → Hom A A + isCategory : IsCategory Obj Hom _≈_ _o_ Id + + op : Category c₁ c₂ ℓ + op = record { Obj = Obj ; Hom = flip Hom ; _o_ = flip _o_ ; _≈_ = _≈_ ; Id = Id ; isCategory = opIsCategory } + where + opIsCategory : IsCategory {c₁} {c₂} {ℓ} Obj (flip Hom) _≈_ (flip _o_) Id + opIsCategory = record { isEquivalence = IsCategory.isEquivalence isCategory + ; identityL = IsCategory.identityR isCategory + ; identityR = IsCategory.identityL isCategory + ; associative = (IsEquivalence.sym (IsCategory.isEquivalence isCategory)) (IsCategory.associative isCategory) + ; o-resp-≈ = flip (IsCategory.o-resp-≈ isCategory) + } + dom : {A B : Obj} → Hom A B → Obj + dom {A} _ = A + cod : {A B : Obj} → Hom A B → Obj + cod {B = B} _ = B + homsetoid : {A B : Obj } → Setoid c₂ ℓ + homsetoid {A} {B} = record { Carrier = Hom A B + ; isEquivalence = IsCategory.isEquivalence isCategory + } + +Obj : ∀{c₁ c₂ ℓ} → (C : Category c₁ c₂ ℓ) → Set c₁ +Obj C = Category.Obj C + +Hom : ∀{c₁ c₂ ℓ} → (C : Category c₁ c₂ ℓ) → Obj C → Obj C → Set c₂ +Hom C = Category.Hom C + +_[_≈_] : ∀{c₁ c₂ ℓ} → (C : Category c₁ c₂ ℓ) → {A B : Obj C} → Rel (Hom C A B) ℓ +C [ f ≈ g ] = Category._≈_ C f g + +_[_o_] : ∀{c₁ c₂ ℓ} → (C : Category c₁ c₂ ℓ) → {a b c : Obj C} → Hom C b c → Hom C a b → Hom C a c +C [ f o g ] = Category._o_ C f g + +infixr 9 _[_o_] +infix 4 _[_≈_] + +Id : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} → (A : Obj C) → Hom C A A +Id {C = C} A = Category.Id C {A} + +record IsFunctor {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁′ c₂′ ℓ′) + (FObj : Obj C → Obj D) + (FMap : {A B : Obj C} → Hom C A B → Hom D (FObj A) (FObj B)) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + field + ≈-cong : {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → D [ FMap f ≈ FMap g ] + identity : {A : Obj C} → D [ (FMap {A} {A} (Id {_} {_} {_} {C} A)) ≈ (Id {_} {_} {_} {D} (FObj A)) ] + distr : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c} + → D [ FMap (C [ g o f ]) ≈ (D [ FMap g o FMap f ] )] + +record Functor {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + field + FObj : Obj domain → Obj codomain + FMap : {A B : Obj domain} → Hom domain A B → Hom codomain (FObj A) (FObj B) + isFunctor : IsFunctor domain codomain FObj FMap + +open import Relation.Binary.PropositionalEquality + +-- cong : ∀{c₁ c₂} {A : Set c₁} {B : Set c₂} {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b +-- cong {A} {B} f refl = refl + +≡-sym : ∀{c}{A : Set c} → Symmetric {_} {A} {_} _≡_ +≡-sym refl = refl + +≡-trans : ∀{c}{A : Set c} → Transitive {_} {A} {_} _≡_ +≡-trans refl refl = refl diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Cat.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Cat.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,118 @@ +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Cat where +open import Category +open import Level +open import Relation.Binary +open import Relation.Binary.Core + +identityFunctor : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} → Functor C C +identityFunctor {C = C} = + record { FObj = λ x → x + ; FMap = λ x → x + ; isFunctor = isFunctor + } + where + isFunctor : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} → IsFunctor C C (λ x → x) (λ x → x) + isFunctor {C = C} = + record { ≈-cong = λ x → x + ; identity = IsEquivalence.refl (IsCategory.isEquivalence (Category.isCategory C)) + ; distr = IsEquivalence.refl (IsCategory.isEquivalence (Category.isCategory C)) + } + +open Functor + +data [_]_~_ {c₁ c₂ ℓ} (C : Category c₁ c₂ ℓ) {A B : Obj C} (f : Hom C A B) + : ∀{X Y : Obj C} → Hom C X Y → Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where + refl : {g : Hom C A B} → (eqv : C [ f ≈ g ]) → [ C ] f ~ g + +_≃_ : ∀ {c₁ c₂ ℓ c₁′ c₂′ ℓ′} {C : Category c₁ c₂ ℓ} {D : Category c₁′ c₂′ ℓ′} + → (F G : Functor C D) → Set (suc ℓ′ ⊔ (suc c₂′ ⊔ (suc c₁′ ⊔ (c₂ ⊔ c₁)))) +_≃_ {C = C} {D = D} F G = ∀{A B : Obj C} → (f : Hom C A B) → [ D ] FMap F f ~ FMap G f + + +_○_ : ∀{c₁ c₂ ℓ c₁′ c₂′ ℓ′ c₁″ c₂″ ℓ″} {C : Category c₁ c₂ ℓ} {D : Category c₁′ c₂′ ℓ′} {E : Category c₁″ c₂″ ℓ″} + → Functor D E → Functor C D → Functor C E +_○_ {C = C} {D = D} {E = E} G F = + record { FObj = λ x → FObj G (FObj F x) + ; FMap = λ x → FMap G (FMap F x) + ; isFunctor = myIsFunctor + } + where + myIsFunctor : IsFunctor C E (λ x → FObj G (FObj F x)) (λ x → FMap G (FMap F x)) + myIsFunctor = + record { ≈-cong = λ x → IsFunctor.≈-cong (isFunctor G) (IsFunctor.≈-cong (isFunctor F) x) + ; identity = IsEquivalence.trans (IsCategory.isEquivalence (Category.isCategory E)) + (IsFunctor.≈-cong (isFunctor G) (IsFunctor.identity (isFunctor F))) + (IsFunctor.identity (isFunctor G)) + ; distr = IsEquivalence.trans (IsCategory.isEquivalence (Category.isCategory E)) + (IsFunctor.≈-cong (isFunctor G) (IsFunctor.distr (isFunctor F))) + (IsFunctor.distr (isFunctor G)) + } + +CatIsCategory : ∀{c₁ c₂ ℓ} + → IsCategory {suc (c₁ ⊔ c₂ ⊔ ℓ)} {suc (ℓ ⊔ (c₂ ⊔ c₁))} {suc (ℓ ⊔ c₁ ⊔ c₂)} (Category c₁ c₂ ℓ) Functor _≃_ _○_ identityFunctor +CatIsCategory {c₁} {c₂} {ℓ} = + record { isEquivalence = isEquivalence + ; o-resp-≈ = λ {A} {B} {C} {f} {g} {h} {i} → o-resp-≈ {A} {B} {C} {f} {g} {h} {i} + ; identityL = λ {C} {D} {f} → identityL {C} {D} {f} + ; identityR = λ {C} {D} {f} → identityR {C} {D} {f} + ; associative = λ {C} {D} {E} {F} {f} {g} {h} → associative {C} {D} {E} {F} {f} {g} {h} + } + where + isEquivalence : {C D : Category c₁ c₂ ℓ} → IsEquivalence {_} {_} {Functor C D} _≃_ + isEquivalence {C} {D} = + record { refl = λ {F} → ≃-refl {F} + ; sym = λ {F} {G} → ≃-sym {F} {G} + ; trans = λ {F} {G} {H} → ≃-trans {F} {G} {H} + } + where + ≃-refl : {F : Functor C D} → F ≃ F + ≃-refl {F} {A} {B} f = + refl {C = D} (IsFunctor.≈-cong (isFunctor F) + (IsEquivalence.refl + (IsCategory.isEquivalence (Category.isCategory C)))) + + ≃-sym : {F G : Functor C D} → F ≃ G → G ≃ F + ≃-sym {F} {G} F≃G {A} {B} f = helper (F≃G f) + where + helper : ∀{a b c d} {f : Hom D a b} {g : Hom D c d} → [ D ] f ~ g → [ D ] g ~ f + helper (refl Ff≈Gf) = refl {C = D} (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory D)) Ff≈Gf) + ≃-trans : {F G H : Functor C D} → F ≃ G → G ≃ H → F ≃ H + ≃-trans {F} {G} {H} F≃G G≃H {A} {B} f = helper (F≃G f) (G≃H f) + where + helper : ∀{O P Q R S T} {f : Hom D O P} {g : Hom D Q R } {h : Hom D S T} + → [ D ] f ~ g → [ D ] g ~ h → [ D ] f ~ h + helper (refl Ff≈Gf) (refl Gf≈Hf) = refl {C = D} (IsEquivalence.trans (IsCategory.isEquivalence (Category.isCategory D)) Ff≈Gf Gf≈Hf) + + o-resp-≈ : {A B C : Category c₁ c₂ ℓ} {f g : Functor A B} {h i : Functor B C} + → f ≃ g → h ≃ i → (h ○ f) ≃ (i ○ g) + o-resp-≈ {B = B} {C} {F} {G} {H} {I} F≃G H≃I {P} {Q} f = + helper {a = FObj F P} {b = FObj F Q} {c = FObj G P} {d = FObj G Q} + {ϕ = FMap F f} {ψ = FMap G f} {π = FMap I (FMap G f) } + (F≃G f) (H≃I (FMap G f)) + where + helper : ∀{a b c d} {z w} {ϕ : Hom B a b} {ψ : Hom B c d} {π : Hom C z w} + → [ B ] ϕ ~ ψ → [ C ] (FMap H ψ) ~ π → [ C ] (FMap H ϕ) ~ π + helper (refl Ff≈Gf) (refl Hf≈If) = + refl {C = C} (IsEquivalence.trans + (IsCategory.isEquivalence (Category.isCategory C)) + (IsFunctor.≈-cong (isFunctor H) Ff≈Gf) Hf≈If) + identityL : {C D : Category c₁ c₂ ℓ} {f : Functor C D} → (identityFunctor ○ f) ≃ f + identityL {C} {D} {f} {A} {B} ϕ = refl {_} (IsEquivalence.refl (IsCategory.isEquivalence (Category.isCategory D))) + identityR : {C D : Category c₁ c₂ ℓ} {f : Functor C D} → (f ○ identityFunctor) ≃ f + identityR {C} {D} {f} {A} {B} ϕ = refl {_} (IsEquivalence.refl (IsCategory.isEquivalence (Category.isCategory D))) + associative : {C D E F : Category c₁ c₂ ℓ} {f : Functor E F} {g : Functor D E} {h : Functor C D} + → (f ○ (g ○ h)) ≃ ((f ○ g) ○ h) + associative {F = F} _ = refl (IsEquivalence.refl (IsCategory.isEquivalence (Category.isCategory F))) + +CAT : ∀{c₁ c₂ ℓ} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (ℓ ⊔ (c₂ ⊔ c₁))) (suc (ℓ ⊔ c₁ ⊔ c₂)) +CAT {c₁} {c₂} {ℓ} = + record { Obj = Category c₁ c₂ ℓ + ; Hom = Functor + ; _o_ = _○_ + ; _≈_ = _≃_ + ; Id = identityFunctor + ; isCategory = CatIsCategory {c₁} {c₂} {ℓ} + } + diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Cone.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Cone.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,65 @@ +{-# OPTIONS --cubical-compatible --irrelevant-projections #-} + +import Category + +module Category.Cone {c₁ c₂ ℓ} (C : Category.Category c₁ c₂ ℓ) where +open Category.Category C +open import Level +open import Relation.Binary +open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality hiding (isEquivalence) + +record Diagram {c₁′ c₂′ ℓ′} (J : Category.Category c₁′ c₂′ ℓ′) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + field + type : Category.Functor J C + index : Set c₁′ + index = Category.Category.Obj J + edge : index → index → Set c₂′ + edge = Category.Category.Hom J + +open Diagram + +record Cone {c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} (D : Diagram J) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + open Category.Functor (type D) + field + apex : Obj + proj : ∀ i → Hom apex (FObj i) + .isCone : ∀{i j : index D} {α : edge D i j } → proj j ≈ FMap α o proj i + +record _-Cone⟶_ {c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} {D : Diagram J} (C₁ : Cone D) (C₂ : Cone D) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + -- private + open Cone + field + morphism : Hom (apex C₁) (apex C₂) + .isConeMorphism : ∀ {j} → proj C₁ j ≈ proj C₂ j o morphism + +open Cone +open _-Cone⟶_ + +ConeId : ∀{c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} {D : Diagram J} {C₁ : Cone D} → C₁ -Cone⟶ C₁ +ConeId {C₁ = C₁} = + record { morphism = Id { apex C₁ } ; isConeMorphism = proof } + where + .proof : ∀ {j} → proj C₁ j ≈ proj C₁ j o Id + proof = ≈-sym identityR + where open Category.IsCategory isCategory + open IsEquivalence isEquivalence renaming (sym to ≈-sym) + +open import HomReasoning + +_∘_ : ∀ {c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} {D : Diagram J} {C₁ C₂ C₃ : Cone D} + → C₂ -Cone⟶ C₃ → C₁ -Cone⟶ C₂ → C₁ -Cone⟶ C₃ +_∘_ {_} {_} {_} {J} {D = D} {C₁} {C₂} {C₃} C₂toC₃ C₁toC₂ = + record { morphism = morph ; isConeMorphism = proof } + where + morph = morphism C₂toC₃ o morphism C₁toC₂ + .proof : {j : index D} → proj C₁ j ≈ proj C₃ j o (morphism C₂toC₃ o morphism C₁toC₂) + proof {j} = begin + proj C₁ j ≈⟨ isConeMorphism C₁toC₂ ⟩ + proj C₂ j o morphism C₁toC₂ ≈⟨ car (isConeMorphism C₂toC₃) ⟩ + (proj C₃ j o morphism C₂toC₃) o morphism C₁toC₂ ≈↑⟨ assoc ⟩ + proj C₃ j o (morphism C₂toC₃ o morphism C₁toC₂) ∎ where + open ≈-Reasoning C hiding (_o_ ) + +-- end diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Constructions/Coslice.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Constructions/Coslice.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,91 @@ +{-# OPTIONS --universe-polymorphism #-} +module Category.Constructions.Coslice where +open import Category +open import Level +open import Relation.Binary +open import Relation.Binary.Core + +import Relation.Binary.EqReasoning as EqR + +record CosliceObj {c₁ c₂ ℓ} (C : Category c₁ c₂ ℓ) (O : Obj C) : Set (c₁ ⊔ c₂) where + constructor ⟦_⟧ + field + {X} : Obj C + arrow : Hom C O X + +record _⟶_ {c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} {O : Obj C} (F G : CosliceObj C O) : Set (c₁ ⊔ c₂ ⊔ ℓ) where + private + f = CosliceObj.arrow F + g = CosliceObj.arrow G + field + arrow : Hom C (Category.cod C f) (Category.cod C g) + proof : C [ (C [ arrow o f ]) ≈ g ] + +_∘_ : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} {O : Obj C} {f g h : CosliceObj C O} → (g ⟶ h) → (f ⟶ g) → (f ⟶ h) +_∘_ {C = C} {O} {f′} {g′} {h′} ψ φ = + record { arrow = C [ a₂ o a₁ ] + ; proof = begin + (a₂ o a₁) o f ≈⟨ symm associative ⟩ + a₂ o (a₁ o f) ≈⟨ o-resp-≈ φ-proof reflex ⟩ + a₂ o g ≈⟨ ψ-proof ⟩ + h + ∎ + } + where + f = CosliceObj.arrow f′ + g = CosliceObj.arrow g′ + h = CosliceObj.arrow h′ + module Cat = Category.Category C + open IsCategory Cat.isCategory + open Cat + a₁ = _⟶_.arrow φ + a₂ = _⟶_.arrow ψ + open IsEquivalence (Setoid.isEquivalence homsetoid) renaming (refl to reflex) + open IsEquivalence (Setoid.isEquivalence homsetoid) renaming (sym to symm) + open EqR homsetoid + φ-proof = _⟶_.proof φ + ψ-proof = _⟶_.proof ψ + +_∼_ : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} {O : Obj C} {F G : CosliceObj C O} → Rel (F ⟶ G) _ +_∼_ {C = C} φ ψ = Category._≈_ C (_⟶_.arrow φ) (_⟶_.arrow ψ) + +CosliceId : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} {O : Obj C} {F : CosliceObj C O} → (F ⟶ F) +CosliceId {C = C} {O} {F = F} = + record { arrow = Cat.Id + ; proof = identityL + } + where + module Cat = Category.Category C + module isCat = IsCategory Cat.isCategory + open Cat + open isCat + f = CosliceObj.arrow F + +_\\_ : ∀{c₁ c₂ ℓ} → (C : Category c₁ c₂ ℓ) → (O : Obj C) → Category _ _ _ +_\\_ {c₁} {c₂} {ℓ} C O = record { Obj = CosliceObj C O + ; Hom = _⟶_ {C = C} {O} + ; Id = CosliceId + ; _o_ = _∘_ + ; _≈_ = _∼_ + ; isCategory = isCategory + } + where + open Category.Category C hiding (isCategory) + open IsCategory (Category.isCategory C) + ∼-refl : {F G : CosliceObj C O} {φ : F ⟶ G} → φ ∼ φ + ∼-refl = IsEquivalence.refl isEquivalence + ∼-trans : {F G : CosliceObj C O} {φ ψ σ : F ⟶ G} → φ ∼ ψ → ψ ∼ σ → φ ∼ σ + ∼-trans = IsEquivalence.trans isEquivalence + ∼-sym : {F G : CosliceObj C O} {φ ψ : F ⟶ G} → φ ∼ ψ → ψ ∼ φ + ∼-sym = IsEquivalence.sym isEquivalence + + isCategory = record { isEquivalence = record { refl = λ{φ} → ∼-refl {φ = φ} + ; sym = λ{φ} {ψ} → ∼-sym {φ = φ} {ψ} + ; trans = λ{φ} {ψ} {σ} → ∼-trans {φ = φ} {ψ} {σ} + } + ; identityL = identityL + ; identityR = identityR + ; associative = associative + ; o-resp-≈ = o-resp-≈ + } + diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Constructions/Product.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Constructions/Product.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,56 @@ +{-# OPTIONS --universe-polymorphism #-} +module Category.Constructions.Product where +open import Category +open import Level +open import Data.Product renaming (_×_ to _*_) +open import Relation.Binary +open import Relation.Binary.Core + +_×_ : ∀{c₁ c₁′ c₂ c₂′ ℓ ℓ′} → Category c₁ c₂ ℓ → Category c₁′ c₂′ ℓ′ → Category (c₁ ⊔ c₁′) (c₂ ⊔ c₂′) (ℓ ⊔ ℓ′) +C₁ × C₂ = record { Obj = ObjProd + ; Hom = _⟶_ + ; Id = IdProd + ; _o_ = _∘_ + ; _≈_ = _≈_ + ; isCategory = record { isEquivalence = record { refl = λ {φ} → ≈-refl {φ = φ} + ; sym = λ {φ ψ} → ≈-symm {φ = φ} {ψ} + ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ} + } + ; identityL = identityL + ; identityR = identityR + ; o-resp-≈ = o-resp-≈ + ; associative = associative + } + } + where + ObjProd : Set _ + ObjProd = Obj C₁ * Obj C₂ + _⟶_ : ObjProd → ObjProd → Set _ + _⟶_ = λ x y → Hom C₁ (proj₁ x) (proj₁ y) * Hom C₂ (proj₂ x) (proj₂ y) + IdProd : {A : ObjProd} → A ⟶ A + IdProd {x} = (Id {C = C₁} (proj₁ x) , Id {C = C₂} (proj₂ x)) + _∘_ : {A B C : Obj C₁} {A′ B′ C′ : Obj C₂} → (Hom C₁ B C * Hom C₂ B′ C′) → (Hom C₁ A B * Hom C₂ A′ B′) → (Hom C₁ A C * Hom C₂ A′ C′) + g ∘ f = (C₁ [ proj₁ g o proj₁ f ] , C₂ [ proj₂ g o proj₂ f ] ) + _≈_ : {A B : ObjProd} → Rel (A ⟶ B) _ + φ ≈ ψ = C₁ [ proj₁ φ ≈ proj₁ ψ ] * C₂ [ proj₂ φ ≈ proj₂ ψ ] + C₁-equiv : ∀{A B} → IsEquivalence (Category._≈_ C₁ {A = A} {B = B}) + C₁-equiv = IsCategory.isEquivalence (Category.isCategory C₁) + C₂-equiv : ∀{A B} → IsEquivalence (Category._≈_ C₂ {A = A} {B = B}) + C₂-equiv = IsCategory.isEquivalence (Category.isCategory C₂) + ≈-refl : {A B : ObjProd} {φ : A ⟶ B} → φ ≈ φ + ≈-refl = (IsEquivalence.refl C₁-equiv , IsEquivalence.refl C₂-equiv) + ≈-symm : {A B : ObjProd} {φ ψ : A ⟶ B} → φ ≈ ψ → ψ ≈ φ + ≈-symm φ≈ψ = (IsEquivalence.sym C₁-equiv (proj₁ φ≈ψ), IsEquivalence.sym C₂-equiv (proj₂ φ≈ψ)) + ≈-trans : {A B : ObjProd} {φ ψ σ : A ⟶ B} → φ ≈ ψ → ψ ≈ σ → φ ≈ σ + ≈-trans φ≈ψ ψ≈σ = ( IsEquivalence.trans C₁-equiv (proj₁ φ≈ψ) (proj₁ ψ≈σ) + , IsEquivalence.trans C₂-equiv (proj₂ φ≈ψ) (proj₂ ψ≈σ)) + identityL : {A B : ObjProd} {φ : A ⟶ B} → (IdProd ∘ φ) ≈ φ + identityL = (IsCategory.identityL (Category.isCategory C₁), IsCategory.identityL (Category.isCategory C₂)) + identityR : {A B : ObjProd} {φ : A ⟶ B} → (φ ∘ IdProd) ≈ φ + identityR = (IsCategory.identityR (Category.isCategory C₁), IsCategory.identityR (Category.isCategory C₂)) + o-resp-≈ : {A B C : ObjProd} {f g : A ⟶ B} {h i : B ⟶ C} → f ≈ g → h ≈ i → (h ∘ f) ≈ (i ∘ g) + o-resp-≈ f≈g h≈i = (IsCategory.o-resp-≈ (Category.isCategory C₁) (proj₁ f≈g) (proj₁ h≈i), + IsCategory.o-resp-≈ (Category.isCategory C₂) (proj₂ f≈g) (proj₂ h≈i)) + associative : {A B C D : ObjProd} {f : C ⟶ D} {g : B ⟶ C} {h : A ⟶ B} + → (f ∘ (g ∘ h)) ≈ ((f ∘ g) ∘ h) + associative = (IsCategory.associative (Category.isCategory C₁), IsCategory.associative (Category.isCategory C₂)) diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Constructions/Slice.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Constructions/Slice.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,94 @@ +{-# OPTIONS --universe-polymorphism #-} +module Category.Constructions.Slice where +open import Category +open import Level +open import Relation.Binary +open import Relation.Binary.Core + +import Relation.Binary.EqReasoning as EqR + +record SliceObj {c₁ c₂ ℓ} (C : Category c₁ c₂ ℓ) (O : Obj C) : Set (c₁ ⊔ c₂) where + constructor ⟦_⟧ + field + {X} : Obj C + arrow : Hom C X O + +record _⟶_ {c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} {O : Obj C} (F G : SliceObj C O) : Set (c₁ ⊔ c₂ ⊔ ℓ) where + private + f = SliceObj.arrow F + g = SliceObj.arrow G + field + arrow : Hom C (Category.dom C f) (Category.dom C g) + proof : C [ f ≈ C [ g o arrow ] ] + +_∘_ : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} {O : Obj C} {f g h : SliceObj C O} → (g ⟶ h) → (f ⟶ g) → (f ⟶ h) +_∘_ {C = C} {O} {f′} {g′} {h′} ψ φ = + record { arrow = C [ a₂ o a₁ ] + ; proof = begin + f ≈⟨ φ-proof ⟩ + g o a₁ ≈⟨ o-resp-≈ reflex ψ-proof ⟩ + (h o a₂) o a₁ ≈⟨ symm associative ⟩ + h o (a₂ o a₁) + ∎ + } + where + f = SliceObj.arrow f′ + g = SliceObj.arrow g′ + h = SliceObj.arrow h′ + module Cat = Category.Category C + open IsCategory Cat.isCategory + open Cat + a₁ = _⟶_.arrow φ + a₂ = _⟶_.arrow ψ + open IsEquivalence (Setoid.isEquivalence homsetoid) renaming (refl to reflex) + open IsEquivalence (Setoid.isEquivalence homsetoid) renaming (sym to symm) + open EqR homsetoid + φ-proof = _⟶_.proof φ + ψ-proof : g ≈ h o a₂ + ψ-proof = _⟶_.proof ψ + +_∼_ : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} {O : Obj C} {F G : SliceObj C O} → Rel (F ⟶ G) _ +_∼_ {C = C} φ ψ = Category._≈_ C (_⟶_.arrow φ) (_⟶_.arrow ψ) + +SliceId : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} {O : Obj C} {F : SliceObj C O} → (F ⟶ F) +SliceId {C = C} {O} {F = F} = + record { arrow = Cat.Id + ; proof = ≈-sym identityR + } + where + module Cat = Category.Category C + module isCat = IsCategory Cat.isCategory + open Cat + open isCat + f = SliceObj.arrow F + module Eq = IsEquivalence (Setoid.isEquivalence homsetoid) + open Eq renaming (sym to ≈-sym) + +_/_ : ∀{c₁ c₂ ℓ} → (C : Category c₁ c₂ ℓ) → (O : Obj C) → Category _ _ _ +_/_ {c₁} {c₂} {ℓ} C O = record { Obj = SliceObj C O + ; Hom = _⟶_ {C = C} {O} + ; Id = SliceId + ; _o_ = _∘_ + ; _≈_ = _∼_ + ; isCategory = isCategory + } + where + open Category.Category C hiding (isCategory) + open IsCategory (Category.isCategory C) + ∼-refl : {F G : SliceObj C O} {φ : F ⟶ G} → φ ∼ φ + ∼-refl = IsEquivalence.refl isEquivalence + ∼-trans : {F G : SliceObj C O} {φ ψ σ : F ⟶ G} → φ ∼ ψ → ψ ∼ σ → φ ∼ σ + ∼-trans = IsEquivalence.trans isEquivalence + ∼-sym : {F G : SliceObj C O} {φ ψ : F ⟶ G} → φ ∼ ψ → ψ ∼ φ + ∼-sym = IsEquivalence.sym isEquivalence + + isCategory = record { isEquivalence = record { refl = λ{φ} → ∼-refl {φ = φ} + ; sym = λ{φ} {ψ} → ∼-sym {φ = φ} {ψ} + ; trans = λ{φ} {ψ} {σ} → ∼-trans {φ = φ} {ψ} {σ} + } + ; identityL = identityL + ; identityR = identityR + ; associative = associative + ; o-resp-≈ = o-resp-≈ + } + diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Group.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Group.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,135 @@ +{-# OPTIONS --universe-polymorphism #-} +module Category.Group where +open import Category +open import Algebra +open import Algebra.Structures +open import Algebra.Morphism +import Algebra.Props.Group as GroupP +import Relation.Binary.EqReasoning as EqR +open import Relation.Binary.Core +open import Relation.Binary +open import Level +open import Data.Product + +GrpObj : ∀{c ℓ} → Set (suc (c ⊔ ℓ)) +GrpObj {c} {ℓ} = Group c ℓ + +record _-Group⟶_ {c ℓ c′ ℓ′} (From : Group c ℓ) (To : Group c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′ ⊔ ℓ′) where + private + module F = Group From + module T = Group To + open Definitions F.Carrier T.Carrier T._≈_ + field + ⟦_⟧ : Morphism + ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_ + ∙-homo : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_ + + ε-homo : Homomorphic₀ ⟦_⟧ F.ε T.ε + ε-homo = left-identity-unique ⟦ F.ε ⟧ ⟦ F.ε ⟧ (begin + T._∙_ ⟦ F.ε ⟧ ⟦ F.ε ⟧ ≈⟨ T.sym (∙-homo F.ε F.ε) ⟩ + ⟦ F._∙_ F.ε F.ε ⟧ ≈⟨ ⟦⟧-cong (proj₁ (IsMonoid.identity (Monoid.isMonoid F.monoid)) F.ε) ⟩ + ⟦ F.ε ⟧ ∎) + where + open GroupP To + open EqR T.setoid + ⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹ + ⁻¹-homo x = left-inverse-unique ⟦ F._⁻¹ x ⟧ ⟦ x ⟧ (begin + T._∙_ ⟦ F._⁻¹ x ⟧ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (F._⁻¹ x) x) ⟩ + ⟦ F._∙_ (F._⁻¹ x) x ⟧ ≈⟨ ⟦⟧-cong (proj₁ (IsGroup.inverse F.isGroup) x) ⟩ + ⟦ F.ε ⟧ ≈⟨ ε-homo ⟩ + T.ε ∎) + where + open GroupP To + open EqR T.setoid + +_⟪_⟫ : ∀{c ℓ c′ ℓ′} {G : Group c ℓ} {F : Group c′ ℓ′} → (M : G -Group⟶ F) → Group.Carrier G → Group.Carrier F +f ⟪ x ⟫ = _-Group⟶_.⟦_⟧ f x + +GrpId : ∀{c ℓ} {G : Group c ℓ} → G -Group⟶ G +GrpId {G = G} = record { ⟦_⟧ = ⟦_⟧ ; ⟦⟧-cong = ⟦⟧-cong ; ∙-homo = ∙-homo } + where + open Algebra.Group G + open Definitions Carrier Carrier _≈_ + ⟦_⟧ : Carrier → Carrier + ⟦_⟧ = λ x → x + ⟦⟧-cong : ⟦_⟧ Preserves _≈_ ⟶ _≈_ + ⟦⟧-cong = λ x → x + ∙-homo : Homomorphic₂ ⟦_⟧ _∙_ _∙_ + ∙-homo x y = IsEquivalence.refl (Setoid.isEquivalence setoid) + +_∘_ : ∀{c₁ ℓ₁ c₂ ℓ₂ c₃ ℓ₃} {G₁ : Group c₁ ℓ₁} {G₂ : Group c₂ ℓ₂} {G₃ : Group c₃ ℓ₃} + → (g : G₂ -Group⟶ G₃) → (f : G₁ -Group⟶ G₂) → G₁ -Group⟶ G₃ +_∘_ {G₁ = G₁} {G₂} {G₃} g f = record { ⟦_⟧ = ⟦_⟧ ; ⟦⟧-cong = ⟦⟧-cong ; ∙-homo = ∙-homo } + where + module F = Group G₁ + module M = Group G₂ + module T = Group G₃ + module hom = _-Group⟶_ + open Definitions (F.Carrier) (T.Carrier) (T._≈_) + ⟦_⟧ : F.Carrier → T.Carrier + ⟦ x ⟧ = g ⟪ f ⟪ x ⟫ ⟫ + ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_ + ⟦⟧-cong x = hom.⟦⟧-cong g (hom.⟦⟧-cong f x) + ∙-homo : Homomorphic₂ ⟦_⟧ (F._∙_) (T._∙_) + ∙-homo x y = begin + ⟦ F._∙_ x y ⟧ ≈⟨ hom.⟦⟧-cong g (hom.∙-homo f x y) ⟩ + g ⟪ M._∙_ (f ⟪ x ⟫) (f ⟪ y ⟫) ⟫ ≈⟨ hom.∙-homo g (f ⟪ x ⟫) (f ⟪ y ⟫) ⟩ + T._∙_ ⟦ x ⟧ ⟦ y ⟧ ∎ + where + open IsEquivalence T.isEquivalence + open EqR T.setoid + +_≈_ : ∀{c ℓ c′ ℓ′} {G₁ : Group c ℓ} {G₂ : Group c′ ℓ′} → Rel (G₁ -Group⟶ G₂) (ℓ′ ⊔ c) +_≈_ {G₁ = G₁} {G₂} φ ψ = ∀(x : F.Carrier) → T._≈_ (φ ⟪ x ⟫) (ψ ⟪ x ⟫) + where + module F = Group G₁ + module T = Group G₂ + +≈-refl : ∀{c ℓ c′ ℓ′} {G₁ : Group c ℓ} {G₂ : Group c′ ℓ′} {F : G₁ -Group⟶ G₂} → F ≈ F +≈-refl {G₁ = G₁} {F = F} _ = _-Group⟶_.⟦⟧-cong F (IsEquivalence.refl (Group.isEquivalence G₁)) + +≈-sym : ∀{c ℓ c′ ℓ′} {G₁ : Group c ℓ} {G₂ : Group c′ ℓ′} {F G : G₁ -Group⟶ G₂} → F ≈ G → G ≈ F +≈-sym {G₁ = G₁} {G₂} {F} {G} F≈G x = IsEquivalence.sym (Group.isEquivalence G₂)(F≈G x) + +≈-trans : ∀{c ℓ c′ ℓ′} {G₁ : Group c ℓ} {G₂ : Group c′ ℓ′} {F G H : G₁ -Group⟶ G₂} + → F ≈ G → G ≈ H → F ≈ H +≈-trans {G₁ = G₁} {G₂} {F} {G} F≈G G≈H x = IsEquivalence.trans (Group.isEquivalence G₂) (F≈G x) (G≈H x) + +Grp : ∀{c ℓ} → Category _ _ _ +Grp {c} {ℓ} = record { Obj = Group c ℓ + ; Hom = _-Group⟶_ + ; Id = GrpId + ; _o_ = _∘_ + ; _≈_ = _≈_ + ; isCategory = isCategory + } + where + isCategory : IsCategory (Group c ℓ) _-Group⟶_ _≈_ _∘_ GrpId + isCategory = + record { isEquivalence = record { refl = λ {F} → ≈-refl {F = F} + ; sym = λ {F} {G} → ≈-sym {F = F} {G} + ; trans = λ {F} {G} {H} → ≈-trans {F = F} {G} {H} + } + ; identityL = λ {G₁} {G₂} {f} → identityL {G₁} {G₂} {f} + ; identityR = λ {G₁} {G₂} {f} → identityR {G₁} {G₂} {f} + ; o-resp-≈ = λ {A} {B} {C} {f} {g} {h} {i} → o-resp-≈ {A} {B} {C} {f} {g} {h} {i} + ; associative = λ {G₁} {G₂} {G₃} {G₄} {f} {g} {h} → associative {G₁} {G₂} {G₃} {G₄} {f} {g} {h} + } + where + identityL : {G₁ G₂ : Group c ℓ} {f : G₁ -Group⟶ G₂} → (GrpId ∘ f) ≈ f + identityL {G₁} {G₂} {f} = ≈-refl {G₁ = G₁} {F = f} + identityR : {G₁ G₂ : Group c ℓ} {f : G₁ -Group⟶ G₂} → (f ∘ GrpId) ≈ f + identityR {G₁} {G₂} {f} = ≈-refl {G₁ = G₁} {F = f} + o-resp-≈ : {G₁ G₂ G₃ : Group c ℓ} {f g : G₁ -Group⟶ G₂} {h i : G₂ -Group⟶ G₃} + → f ≈ g → h ≈ i → (h ∘ f) ≈ (i ∘ g) + o-resp-≈ {G₁} {G₂} {G₃} {f} {g} {h} {i} f≈g h≈i x = begin + (h ⟪ f ⟪ x ⟫ ⟫) ≈⟨ (h≈i ( f ⟪ x ⟫ )) ⟩ + (i ⟪ f ⟪ x ⟫ ⟫) ≈⟨ _-Group⟶_.⟦⟧-cong i (f≈g x) ⟩ + (i ⟪ g ⟪ x ⟫ ⟫) ∎ + where + module T = Group G₃ + open IsEquivalence T.isEquivalence + open EqR T.setoid + associative : {G₁ G₂ G₃ G₄ : Group c ℓ} {f : G₃ -Group⟶ G₄} {g : G₂ -Group⟶ G₃} {h : G₁ -Group⟶ G₂} + → (f ∘ (g ∘ h)) ≈ ((f ∘ g) ∘ h) + associative {G₁} {G₂} {G₃} {G₄} {f} {g} {h} = ≈-refl {G₁ = G₁} {F = f ∘ (g ∘ h)} diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Isomorphism.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Isomorphism.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,128 @@ +{-# OPTIONS --universe-polymorphism #-} +import Category + +module Category.Isomorphism {c₁ c₂ ℓ} (C : Category.Category c₁ c₂ ℓ) where +open Category.Category C +open import Level +import Relation.Binary.EqReasoning as EqR +open import Relation.Binary +open import Relation.Binary.Core + +record _⁻¹≈_ {A B} (f : Hom A B) (g : Hom B A) : Set (c₁ ⊔ c₂ ⊔ ℓ) where + field + invˡ : g o f ≈ Id + invʳ : f o g ≈ Id + +record Iso {A B : Obj} (f : Hom A B) : Set (c₁ ⊔ c₂ ⊔ ℓ) where + field + inverse : Hom B A + proof : f ⁻¹≈ inverse + +record _≅_ (A : Obj) (B : Obj) : Set (c₁ ⊔ c₂ ⊔ ℓ) where + field + f : Hom A B + iso : Iso f + +inverse-unique : {A B : Obj} {f : Hom A B} {g g′ : Hom B A} → f ⁻¹≈ g → f ⁻¹≈ g′ → g ≈ g′ +inverse-unique {f = f} {g} {g′} g-inv g′-inv = + begin + g ≈⟨ ≈-sym₂ identityL ⟩ + Id o g ≈⟨ o-resp-≈ ≈-refl (≈-sym₁ (_⁻¹≈_.invˡ g′-inv)) ⟩ + (g′ o f) o g ≈⟨ ≈-sym₂ associative ⟩ + g′ o (f o g) ≈⟨ o-resp-≈ (_⁻¹≈_.invʳ g-inv) ≈-refl ⟩ + g′ o Id ≈⟨ identityR ⟩ + g′ + ∎ + where + open EqR homsetoid + open Category.IsCategory isCategory + open IsEquivalence isEquivalence + renaming (refl to ≈-refl; sym to ≈-sym₂) + open IsEquivalence isEquivalence + renaming (sym to ≈-sym₁) + +inverse-opposite : {A B : Obj} {f : Hom A B} {g : Hom B A} → f ⁻¹≈ g → g ⁻¹≈ f +inverse-opposite iso = record { invʳ = _⁻¹≈_.invˡ iso ; invˡ = _⁻¹≈_.invʳ iso } + +idIso : {A : Obj} → Iso (Id {A}) +idIso {A} = record { inverse = Id {A} ; proof = myProof} + where + open Category.IsCategory isCategory + myProof : Id {A} ⁻¹≈ Id {A} + myProof = record { invˡ = identityL + ; invʳ = identityL + } + +≅-refl : {A : Obj} → A ≅ A +≅-refl {A} = record {f = Id ; iso = idIso } + +≅-trans : {A B C : Obj} → A ≅ B → B ≅ C → A ≅ C +≅-trans {A} {B} {C} A≅B B≅C = record { f = g o h + ; iso = iso + } + where + module ACongB = _≅_ A≅B + module BCongC = _≅_ B≅C + g = BCongC.f + h = ACongB.f + module IsoG = Iso BCongC.iso + module IsoH = Iso ACongB.iso + g⁻¹ = IsoG.inverse + h⁻¹ = IsoH.inverse + module ProofH = _⁻¹≈_ IsoH.proof + module ProofG = _⁻¹≈_ IsoG.proof + invˡ : (h⁻¹ o g⁻¹) o (g o h) ≈ Id + invˡ = begin + (h⁻¹ o g⁻¹) o (g o h) ≈⟨ associative ⟩ + ((h⁻¹ o g⁻¹) o g) o h ≈⟨ o-resp-≈ ≈-refl (≈-sym′ associative) ⟩ + (h⁻¹ o (g⁻¹ o g)) o h ≈⟨ o-resp-≈ ≈-refl (o-resp-≈ (ProofG.invˡ) ≈-refl′) ⟩ + (h⁻¹ o Id) o h ≈⟨ o-resp-≈ ≈-refl identityR ⟩ + h⁻¹ o h ≈⟨ ProofH.invˡ ⟩ + Id + ∎ + where + open EqR homsetoid + open Category.IsCategory isCategory + open IsEquivalence isEquivalence + renaming (refl to ≈-refl; sym to ≈-sym) + open IsEquivalence isEquivalence + renaming (refl to ≈-refl′; sym to ≈-sym′) + invʳ : (g o h) o (h⁻¹ o g⁻¹) ≈ Id + invʳ = begin + (g o h) o (h⁻¹ o g⁻¹) ≈⟨ associative ⟩ + ((g o h) o h⁻¹) o g⁻¹ ≈⟨ o-resp-≈ ≈-refl (≈-sym′ associative) ⟩ + (g o (h o h⁻¹)) o g⁻¹ ≈⟨ o-resp-≈ ≈-refl (o-resp-≈ (ProofH.invʳ) ≈-refl′) ⟩ + (g o Id) o g⁻¹ ≈⟨ o-resp-≈ ≈-refl identityR ⟩ + g o g⁻¹ ≈⟨ ProofG.invʳ ⟩ + Id + ∎ + where + open EqR homsetoid + open Category.IsCategory isCategory + open IsEquivalence isEquivalence + renaming (refl to ≈-refl; sym to ≈-sym) + open IsEquivalence isEquivalence + renaming (refl to ≈-refl′; sym to ≈-sym′) + + proof : (g o h) ⁻¹≈ (h⁻¹ o g⁻¹) + proof = record { invˡ = invˡ ; invʳ = invʳ } + iso : Iso (g o h) + iso = record { inverse = h⁻¹ o g⁻¹ + ; proof = proof + } + +≅-sym : {A B : Obj} → A ≅ B → B ≅ A +≅-sym {A} {B} A≅B = record { f = inverse ; iso = iso } + where + module ACongB = _≅_ A≅B + module IsoF = Iso ACongB.iso + inverse = IsoF.inverse + iso = record { inverse = ACongB.f ; proof = inverse-opposite IsoF.proof } + +≅-is-equivalence : IsEquivalence _≅_ +≅-is-equivalence = record { refl = ≅-refl + ; sym = ≅-sym + ; trans = ≅-trans + } + + diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Monoid.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Monoid.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,93 @@ +{-# OPTIONS --universe-polymorphism #-} +module Category.Monoid where +open import Category +open import Relation.Binary +open import Relation.Binary.Core +open import Algebra.Structures +open import Algebra +open import Level +open import Data.Product + +data MonoidObj : Set1 where + * : MonoidObj + +data MonoidMor {c ℓ : Level} {M : Monoid c ℓ} : MonoidObj → MonoidObj → Set c where + Mor : Monoid.Carrier M → MonoidMor * * + +MonoidId : {c ℓ : Level} {M : Monoid c ℓ} {A : MonoidObj} → MonoidMor {c} {ℓ} {M} A A +MonoidId {_} {_} {M} {*} = Mor (Monoid.ε M) + +comp : ∀{c ℓ} {M : Monoid c ℓ} {A B C : MonoidObj} + → MonoidMor {c} {ℓ} {M} B C + → MonoidMor {c} {ℓ} {M} A B + → MonoidMor {c} {ℓ} {M} A C +comp {_} {_} {M} {*} {*} {*} (Mor a) (Mor b) = Mor (Monoid._∙_ M a b) + +data _≃_ {c ℓ : Level} {M : Monoid c ℓ} : Rel (MonoidMor {_} {_} {M} * *) (suc (c ⊔ ℓ)) where + Eq : {n m : Monoid.Carrier M} → (Monoid._≈_ M n m) → Mor n ≃ Mor m + +moneq_refl : ∀{c ℓ} {M : Monoid c ℓ} → Reflexive (_≃_ {c} {ℓ} {M}) +moneq_refl {c} {ℓ} {M} {Mor f} = Eq (IsEquivalence.refl (Monoid.isEquivalence M)) + +moneq_sym : ∀{c ℓ} {M : Monoid c ℓ} → Symmetric (_≃_ {c} {ℓ} {M}) +moneq_sym {c} {ℓ} {M} {Mor f} {Mor g} (Eq eqv) = Eq (IsEquivalence.sym (Monoid.isEquivalence M) eqv) + +moneq_trans : ∀{c ℓ} {M : Monoid c ℓ} → Transitive (_≃_ {c} {ℓ} {M}) +moneq_trans {c} {ℓ} {M} {Mor f} {Mor g} (Eq eq₁) (Eq eq₂) = Eq (IsEquivalence.trans (Monoid.isEquivalence M) eq₁ eq₂) + +_~_ : ∀{c ℓ} {M : Monoid c ℓ} {A B : MonoidObj} → Rel (MonoidMor {_} {_} {M} A B) (suc (c ⊔ ℓ)) +_~_ {_} {_} {M} {*} {*} = _≃_ + +reflexive : ∀{c ℓ} {M : Monoid c ℓ} {A B : MonoidObj} → Reflexive (_~_ {c} {ℓ} {M} {A} {B}) +reflexive {_} {_} {M} {*} {*} = moneq_refl + +transitive : ∀{c ℓ} {M : Monoid c ℓ} {A B : MonoidObj} → Transitive (_~_ {c} {ℓ} {M} {A} {B}) +transitive {_} {_} {M} {*} {*} = moneq_trans + +symmetric : ∀{c ℓ} {M : Monoid c ℓ} {A B : MonoidObj} → Symmetric (_~_ {c} {ℓ} {M} {A} {B}) +symmetric {_} {_} {M} {*} {*} = moneq_sym + +isCategory : ∀{c ℓ} → (M : Monoid c ℓ) → IsCategory MonoidObj (MonoidMor {c} {ℓ} {M}) _~_ comp MonoidId +isCategory {c} {ℓ} M = + record { isEquivalence = isEquivalence + ; identityL = identityL + ; identityR = identityR + ; o-resp-≈ = o-resp-≈ + ; associative = assoc + } + where + isEquivalence : {A B : MonoidObj} + → IsEquivalence {c} {suc (c ⊔ ℓ)} {MonoidMor A B} (_~_ {c} {ℓ} {M} {A} {B}) + isEquivalence {*} {*} = record { refl = reflexive; sym = symmetric; trans = transitive } + o-resp-≃ : {f g h i : MonoidMor {c} {ℓ} {M} * *} → f ≃ g → h ≃ i → comp h f ≃ comp i g + o-resp-≃ {Mor f} {Mor g} {Mor h} {Mor i} (Eq eq₁) (Eq eq₂) = + Eq (IsSemigroup.∙-cong (IsMonoid.isSemigroup (Monoid.isMonoid M)) eq₂ eq₁) + o-resp-≈ : {A B C : MonoidObj} {f g : MonoidMor {c} {ℓ} {M} A B} {h i : MonoidMor B C} + → f ~ g → h ~ i → comp h f ~ comp i g + o-resp-≈ {*} {*} {*} {f} {g} {h} = o-resp-≃ + assoc : {A B C D : MonoidObj} + {f : MonoidMor {c} {ℓ} {M} A B} {g : MonoidMor {c} {ℓ} {M} B C} {h : MonoidMor {c} {ℓ} {M} C D} + → comp h (comp g f) ~ comp (comp h g) f + assoc {*} {*} {*} {*} {Mor f} {Mor g} {Mor h} = + Eq (IsEquivalence.sym + (IsSemigroup.isEquivalence + (IsMonoid.isSemigroup (Monoid.isMonoid M))) + (IsSemigroup.assoc (IsMonoid.isSemigroup (Monoid.isMonoid M)) h g + f)) + + identityL : {c ℓ : Level} {M : Monoid c ℓ} {A B : MonoidObj} {f : MonoidMor {c} {ℓ} {M} A B} → (comp MonoidId f) ~ f + identityL {c} {ℓ} {M} {*} {*} {Mor f} = Eq {c} {ℓ} {M} (proj₁ (IsMonoid.identity (Monoid.isMonoid M)) f) + + identityR : {c ℓ : Level} {M : Monoid c ℓ} {A B : MonoidObj} {f : MonoidMor {c} {ℓ} {M} A B} → (comp f MonoidId) ~ f + identityR {c} {ℓ} {M} {*} {*} {Mor f} = Eq {c} {ℓ} {M} (proj₂ (IsMonoid.identity (Monoid.isMonoid M)) f) + + + +MONOID : ∀{c ℓ} → (M : Monoid c ℓ) → Category (suc zero) c (suc (ℓ ⊔ c)) +MONOID M = record { Obj = MonoidObj + ; Hom = MonoidMor {_} {_} {M} + ; _o_ = comp + ; _≈_ = _~_ + ; Id = MonoidId + ; isCategory = isCategory M + } diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Object/Terminal.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Object/Terminal.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,38 @@ +{-# OPTIONS --universe-polymorphism #-} +import Category + +module Category.Object.Terminal {c₁ c₂ ℓ} (C : Category.Category c₁ c₂ ℓ) where +open Category.Category C +open import Category.Isomorphism C +open import Level +import Relation.Binary.EqReasoning as EqR +open import Relation.Binary +open import Relation.Binary.Core + +record Terminal : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where + field + ⊤ : Obj + ! : ∀{A : Obj} → Hom A ⊤ + !-unique : ∀{A : Obj} → (f : Hom A ⊤) → (f ≈ !) + + !-unique₂ : ∀{A : Obj} → (f : Hom A ⊤) → (g : Hom A ⊤) → (f ≈ g) + !-unique₂ f g = begin + f ≈⟨ !-unique f ⟩ + ! ≈⟨ ≈-sym (!-unique g) ⟩ + g + ∎ + where + open EqR homsetoid + open Category.IsCategory isCategory + open IsEquivalence isEquivalence renaming (sym to ≈-sym) + + +open Terminal + +terminal-up-to-iso : (t₁ t₂ : Terminal) → ⊤ t₁ ≅ ⊤ t₂ +terminal-up-to-iso t₁ t₂ = record { f = ! t₂ {⊤ t₁} ; iso = iso } + where + proof = record { invˡ = !-unique₂ t₁ (! t₁ o ! t₂) Id + ; invʳ = !-unique₂ t₂ (! t₂ o ! t₁) Id + } + iso = record { inverse = ! t₁ ; proof = proof} diff -r 71049ed05151 -r 45de2b31bf02 src/Category/One.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/One.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,52 @@ +module Category.One where +open import Category +open import Level +open import Relation.Binary +open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +data OneObject : Set where + OneObj : OneObject + +data OneMor : OneObject → OneObject → Set where + OneIdMor : OneMor OneObj OneObj + +comp : {A B C : OneObject} → OneMor B C → OneMor A B → OneMor A C +comp OneIdMor OneIdMor = OneIdMor + +OneEquiv : {A B : OneObject} → IsEquivalence {zero} {zero} {OneMor A B} _≡_ +OneEquiv = record { refl = refl ; sym = ≡-sym; trans = ≡-trans} + +OneID : {A : OneObject} → OneMor A A +OneID {OneObj} = OneIdMor + +OneAssoc : {A B C D : OneObject} {f : OneMor C D} {g : OneMor B C } {h : OneMor A B} + → comp f (comp g h) ≡ comp (comp f g) h +OneAssoc {OneObj} {OneObj} {OneObj} {OneObj} {OneIdMor} {OneIdMor} {OneIdMor} = refl + +OneIdentityL : {A B : OneObject} {f : OneMor A B} → (comp OneID f) ≡ f +OneIdentityL {OneObj} {OneObj} {OneIdMor} = refl + +OneIdentityR : {A B : OneObject} {f : OneMor A B} → (comp f OneID) ≡ f +OneIdentityR {OneObj} {OneObj} {OneIdMor} = refl + +o-resp-≡ : {A B C : OneObject} {f g : OneMor A B} {h i : OneMor B C} → f ≡ g → h ≡ i → comp h f ≡ comp i g +o-resp-≡ {OneObj} {OneObj} {OneObj} {f} {g} {h} {i} f≡g h≡i = + ≡-trans (cong (comp h) f≡g) (cong (λ x → comp x g) h≡i) + + +isCategory : IsCategory {zero} {zero} {zero} OneObject OneMor _≡_ comp OneID +isCategory = record { isEquivalence = OneEquiv + ; identityL = OneIdentityL + ; identityR = OneIdentityR + ; o-resp-≈ = o-resp-≡ + ; associative = OneAssoc + } + +ONE : Category zero zero zero +ONE = record { Obj = OneObject + ; Hom = OneMor + ; _≈_ = _≡_ + ; Id = OneID + ; isCategory = isCategory + } diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Poset.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Poset.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,75 @@ +{-# OPTIONS --universe-polymorphism #-} +module Category.Poset where +open import Category +open import Relation.Binary +open import Relation.Binary.Core +open import Level + +PosetObj : ∀{c ℓ₁ ℓ₂} → (Poset c ℓ₁ ℓ₂) → Set c +PosetObj P = Poset.Carrier P + + +data PosetMor {c ℓ₁ ℓ₂} (P : Poset c ℓ₁ ℓ₂) : PosetObj P → PosetObj P → Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + Ord : {n m : Poset.Carrier P} → Poset._≤_ P n m → PosetMor P n m + +PosetId : ∀{c ℓ₁ ℓ₂} → (P : Poset c ℓ₁ ℓ₂) → {n : PosetObj P} → PosetMor P n n +PosetId P = Ord (IsPreorder.reflexive + (IsPartialOrder.isPreorder (Poset.isPartialOrder P)) + (IsEquivalence.refl + (IsPreorder.isEquivalence + (IsPartialOrder.isPreorder (Poset.isPartialOrder P))))) + +_[_≦_] : ∀{c ℓ₁ ℓ₂} → (P : Poset c ℓ₁ ℓ₂) → PosetObj P → PosetObj P → Set ℓ₂ +P [ n ≦ m ] = Poset._≤_ P n m + +_[_≡_] : ∀{c ℓ₁ ℓ₂} → (P : Poset c ℓ₁ ℓ₂) → PosetObj P → PosetObj P → Set ℓ₁ +P [ n ≡ m ] = Poset._≈_ P n m + +data _≃_ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} {A B : PosetObj P} : PosetMor P A B → PosetMor P A B → Set (suc (ℓ₂ ⊔ (ℓ₁ ⊔ c))) where + refl : {ord₁ ord₂ : PosetMor P A B} → ord₁ ≃ ord₂ + +≃-sym : ∀{c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} {A B : PosetObj P} {ord₁ ord₂ : PosetMor P A B} + → ord₁ ≃ ord₂ → ord₂ ≃ ord₁ +≃-sym refl = refl + +≃-trans : ∀{c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} {A B : PosetObj P} {ord₁ ord₂ ord₃ : PosetMor P A B} + → ord₁ ≃ ord₂ → ord₂ ≃ ord₃ → ord₁ ≃ ord₃ +≃-trans refl refl = refl + +infix 4 _[_≡_] _[_≦_] + +comp : ∀{c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} {A B C : PosetObj P} + → PosetMor P B C + → PosetMor P A B + → PosetMor P A C +comp {P = P} (Ord ord₂) (Ord ord₁) = + Ord (IsPreorder.trans (IsPartialOrder.isPreorder (Poset.isPartialOrder P)) ord₁ ord₂) + +CategoryFromPoset : ∀{c ℓ₁ ℓ₂} → Poset c ℓ₁ ℓ₂ → Category c (suc (ℓ₂ ⊔ (ℓ₁ ⊔ c))) (suc (ℓ₂ ⊔ (ℓ₁ ⊔ c))) +CategoryFromPoset P = record { Obj = PosetObj P + ; Hom = PosetMor P + ; _o_ = comp + ; _≈_ = _≃_ + ; Id = PosetId P + ; isCategory = isCategory + } + where + isCategory : IsCategory (PosetObj P) (PosetMor P) _≃_ comp (PosetId P) + isCategory = + record { isEquivalence = record {refl = refl; sym = ≃-sym ; trans = ≃-trans} + ; identityL = identityL + ; identityR = identityR + ; associative = associative + ; o-resp-≈ = o-resp-≈ + } + where + identityL : {A B : PosetObj P} {f : PosetMor P A B} → comp (PosetId P) f ≃ f + identityL {A} {B} {Ord ord} = refl + identityR : {A B : PosetObj P} {f : PosetMor P A B} → comp f (PosetId P) ≃ f + identityR = refl + associative : {A B C D : PosetObj P} {f : PosetMor P A B} {g : PosetMor P B C} {h : PosetMor P C D} + → comp h (comp g f) ≃ comp (comp h g) f + associative = refl + o-resp-≈ : {A B C : PosetObj P} {f g : PosetMor P A B} {h i : PosetMor P B C} + → f ≃ g → h ≃ i → comp h f ≃ comp i g + o-resp-≈ refl refl = refl diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Rel.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Rel.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,86 @@ +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Rel where +open import Category +open import Relation.Binary.Core +open import Relation.Binary +open import Level + +RelObj : ∀ ℓ → Set (suc ℓ) +RelObj ℓ = Set ℓ + +_-Rel⟶_ : ∀{ℓ} → RelObj ℓ → RelObj ℓ → Set _ +_-Rel⟶_ {ℓ} A B = REL A B (suc ℓ) + +data RelId {ℓ} {A : RelObj ℓ} (x : A) : A → Set (suc ℓ) where + ReflRel : RelId x x + +data _∘_ {ℓ} {A B C : RelObj ℓ} (P : B -Rel⟶ C ) (Q : A -Rel⟶ B) (i : A) (k : C) : Set (suc ℓ) where + Comp : {j : B} → {a : P j k} → {b : Q i j} → _∘_ P Q i k + +data _≈_ {ℓ} {A B : RelObj ℓ} (P Q : A -Rel⟶ B) : Set (suc ℓ) where + exactly : P ⇒ Q → Q ⇒ P → P ≈ Q + +≈-refl : ∀{ℓ} {A B : RelObj ℓ} {P : A -Rel⟶ B} → P ≈ P +≈-refl = exactly (λ z → z) (λ z → z) + +≈-sym : ∀{ℓ} {A B : RelObj ℓ} {P Q : A -Rel⟶ B} → P ≈ Q → Q ≈ P +≈-sym (exactly P⇒Q Q⇒P) = exactly Q⇒P P⇒Q + +≈-trans : ∀{ℓ} {A B : RelObj ℓ} {P Q R : A -Rel⟶ B} + → P ≈ Q → Q ≈ R → P ≈ R +≈-trans (exactly P⇒Q Q⇒P) (exactly Q⇒R R⇒Q) + = exactly (λ z → Q⇒R (P⇒Q z)) (λ z → Q⇒P (R⇒Q z)) + +Rels : ∀{ℓ} → Category _ _ (suc ℓ) +Rels {ℓ} = record { Obj = RelObj ℓ + ; Hom = _-Rel⟶_ + ; _o_ = _∘_ + ; _≈_ = _≈_ + ; isCategory = isCategory + } + where + isCategory : IsCategory (RelObj ℓ) _-Rel⟶_ _≈_ _∘_ RelId + isCategory = + record { isEquivalence = record { refl = ≈-refl ; trans = ≈-trans ; sym = ≈-sym} + ; identityL = λ {P=P} → identityL {P=P} + ; identityR = λ {P=P} → identityR {P=P} + ; o-resp-≈ = λ {P=P} {Q} {R} {S} → o-resp-≈ {P=P}{Q}{R}{S} + ; associative = λ {P=P} {Q} {R} → associative {P=P} {Q} {R} + } + where + identityL : {A B : RelObj ℓ} {P : A -Rel⟶ B} → (RelId ∘ P) ≈ P + identityL {A} {B} {P} = exactly lhs rhs + where + lhs : ∀{i : A} {j : B} → (RelId ∘ P) i j → P i j + lhs {i} {j} (Comp {a = ReflRel} {b = Pij}) = Pij + rhs : ∀{i : A} {j : B} → P i j → (RelId ∘ P) i j + rhs {i} {j} (Pij) = Comp {j = j} {ReflRel} {Pij} + identityR : {A B : RelObj ℓ} {P : A -Rel⟶ B} → (P ∘ RelId) ≈ P + identityR {A} {B} {P} = exactly lhs rhs + where + lhs : ∀{i : A} {j : B} → (P ∘ RelId) i j → P i j + lhs (Comp {a = Pij} {b = ReflRel}) = Pij + rhs : ∀{i : A} {j : B} → P i j → (P ∘ RelId) i j + rhs {i} Pij = Comp {j = i} {Pij} {ReflRel} + + o-resp-≈ : {A B C : RelObj ℓ} {P Q : A -Rel⟶ B} {R S : B -Rel⟶ C} + → P ≈ Q → R ≈ S → (R ∘ P) ≈ (S ∘ Q) + o-resp-≈ {A} {B} {C} {P = P} {Q} {R} {S} (exactly P⇒Q Q⇒P) (exactly R⇒S S⇒R) + = exactly lhs rhs + where + lhs : ∀ {i : A} {j : C} → (R ∘ P) i j → (S ∘ Q) i j + lhs {i} {j} (Comp {a = Rkj} {b = Pik} ) = Comp {a = R⇒S Rkj} {b = P⇒Q Pik} + rhs : S ∘ Q ⇒ R ∘ P + rhs {i} {j} (Comp {a = Skj} {b = Qik} ) = Comp {a = S⇒R Skj} {b = Q⇒P Qik} + + associative : {A B C D : RelObj ℓ} {P : C -Rel⟶ D} {Q : B -Rel⟶ C} {R : A -Rel⟶ B} + → (P ∘ (Q ∘ R)) ≈ ((P ∘ Q) ∘ R) + associative {A} {B} {C} {D} {P} {Q} {R} = exactly lhs rhs + where + lhs : ∀{i : A} {l : D} → (P ∘ (Q ∘ R)) i l → ((P ∘ Q) ∘ R) i l + lhs {i} {l} (Comp {a = Pkl} {b = Comp {a = Qjk} {b = Rij}}) = + Comp {a = Comp {a = Pkl} {b = Qjk}} {b = Rij} + rhs : ∀{i : A} {l : D} → ((P ∘ Q) ∘ R) i l → (P ∘ (Q ∘ R)) i l + rhs {i} {l} (Comp {a = Comp {a = Pkl} {b = Qjk}} {b = Rij}) = + Comp {a = Pkl} {b = Comp {a = Qjk} {b = Rij}} diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Ring.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Ring.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,150 @@ +{-# OPTIONS --universe-polymorphism #-} +module Category.Ring where +open import Category +open import Algebra +open import Algebra.Structures +open import Algebra.Morphism +import Relation.Binary.EqReasoning as EqR +open import Relation.Binary.Core +open import Relation.Binary +open import Level +open import Data.Product + +RingObj : ∀{c ℓ} → Set (suc (c ⊔ ℓ)) +RingObj {c} {ℓ} = Ring c ℓ + +RingHom : ∀{c ℓ} → Set (suc (c ⊔ ℓ)) +RingHom {c} {ℓ} = {R₁ R₂ : Ring c ℓ} → R₁ -Ring⟶ R₂ + +RingId : ∀{c ℓ} {R : Ring c ℓ} → R -Ring⟶ R +RingId {R = R} = record { ⟦_⟧ = ⟦_⟧ ; ⟦⟧-cong = ⟦⟧-cong ; +-homo = +-homo + ; *-homo = *-homo ; 1-homo = 1-homo + } + where + open Algebra.Ring R + open Definitions Carrier Carrier _≈_ + ⟦_⟧ : Morphism + ⟦_⟧ = λ x → x + ⟦⟧-cong : ⟦_⟧ Preserves _≈_ ⟶ _≈_ + ⟦⟧-cong = λ x → x + +-homo : Homomorphic₂ ⟦_⟧ _+_ _+_ + +-homo x y = IsEquivalence.refl isEquivalence + *-homo : Homomorphic₂ ⟦_⟧ _*_ _*_ + *-homo x y = IsEquivalence.refl isEquivalence + 1-homo : Homomorphic₀ ⟦_⟧ 1# 1# + 1-homo = IsEquivalence.refl isEquivalence + +[_]_ : ∀{c ℓ c′ ℓ′} {R₁ : Ring c ℓ} {R₂ : Ring c′ ℓ′} → R₁ -Ring⟶ R₂ → Ring.Carrier R₁ → Ring.Carrier R₂ +[ f ] x = _-Ring⟶_.⟦_⟧ f x + +_∘_ : ∀{c₁ ℓ₁ c₂ ℓ₂ c₃ ℓ₃} {R₁ : Ring c₁ ℓ₁} {R₂ : Ring c₂ ℓ₂} {R₃ : Ring c₃ ℓ₃} + → R₂ -Ring⟶ R₃ → R₁ -Ring⟶ R₂ → R₁ -Ring⟶ R₃ +_∘_ {R₁ = R₁} {R₂} {R₃} g f = + record { ⟦_⟧ = ⟦_⟧ ; ⟦⟧-cong = ⟦⟧-cong ; +-homo = +-homo + ; *-homo = *-homo ; 1-homo = 1-homo + } + where + module F = Ring R₁ + module M = Ring R₂ + module T = Ring R₃ + module homo = _-Ring⟶_ + open Definitions F.Carrier T.Carrier T._≈_ + ⟦_⟧ : Morphism + ⟦ x ⟧ = [ g ] ([ f ] x) + ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_ + ⟦⟧-cong x = homo.⟦⟧-cong g (homo.⟦⟧-cong f x) + +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_ + +-homo x y = + begin + ⟦ F._+_ x y ⟧ ≈⟨ homo.⟦⟧-cong g (homo.+-homo f x y) ⟩ + [ g ] ( M._+_ ([ f ] x) ([ f ] y) ) ≈⟨ homo.+-homo g ([ f ] x) ([ f ] y) ⟩ + T._+_ ⟦ x ⟧ ⟦ y ⟧ + ∎ + where + open IsEquivalence T.isEquivalence + open EqR T.setoid + *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_ + *-homo x y = + begin + ⟦ F._*_ x y ⟧ ≈⟨ homo.⟦⟧-cong g (homo.*-homo f x y) ⟩ + [ g ] ( M._*_ ([ f ] x) ([ f ] y) ) ≈⟨ homo.*-homo g ([ f ] x) ([ f ] y) ⟩ + T._*_ ⟦ x ⟧ ⟦ y ⟧ + ∎ + where + open IsEquivalence T.isEquivalence + open EqR T.setoid + 1-homo : Homomorphic₀ ⟦_⟧ F.1# T.1# + 1-homo = + begin + ⟦ F.1# ⟧ ≈⟨ homo.⟦⟧-cong g (homo.1-homo f) ⟩ + [ g ] M.1# ≈⟨ homo.1-homo g ⟩ + T.1# + ∎ + where + open IsEquivalence T.isEquivalence + open EqR T.setoid + +_≈_ : ∀{c ℓ c′ ℓ′} {R₁ : Ring c ℓ} {R₂ : Ring c′ ℓ′} → Rel (R₁ -Ring⟶ R₂) (ℓ′ ⊔ c) +_≈_ {R₁ = R₁} {R₂} φ ψ = ∀(x : F.Carrier) → T._≈_ ([ φ ] x) ([ ψ ] x) + where + module F = Ring R₁ + module T = Ring R₂ + +≈-refl : ∀{c ℓ c′ ℓ′} {R₁ : Ring c ℓ} {R₂ : Ring c′ ℓ′} {F : R₁ -Ring⟶ R₂} → F ≈ F +≈-refl {R₁ = R₁} {F = F} _ = _-Ring⟶_.⟦⟧-cong F (IsEquivalence.refl (Ring.isEquivalence R₁)) + +≈-sym : ∀{c ℓ c′ ℓ′} {R₁ : Ring c ℓ} {R₂ : Ring c′ ℓ′} {F G : R₁ -Ring⟶ R₂} → F ≈ G → G ≈ F +≈-sym {R₁ = R₁} {R₂} {F} {G} F≈G x = IsEquivalence.sym (Ring.isEquivalence R₂)(F≈G x) + +≈-trans : ∀{c ℓ c′ ℓ′} {R₁ : Ring c ℓ} {R₂ : Ring c′ ℓ′} {F G H : R₁ -Ring⟶ R₂} + → F ≈ G → G ≈ H → F ≈ H +≈-trans {R₁ = R₁} {R₂} {F} {G} F≈G G≈H x = IsEquivalence.trans (Ring.isEquivalence R₂) (F≈G x) (G≈H x) + +≈-isEquivalence : ∀{c ℓ c′ ℓ′} {R₁ : Ring c ℓ} {R₂ : Ring c′ ℓ′} + → IsEquivalence {A = R₁ -Ring⟶ R₂} _≈_ +≈-isEquivalence {R₁ = R₁} {R₂} = record { refl = λ {F} → ≈-refl {R₁ = R₁} {R₂} {F} + ; sym = λ{F} {G} → ≈-sym {R₁ = R₁} {R₂} {F} {G} + ; trans = λ{F} {G} {H} → ≈-trans {R₁ = R₁} {R₂} {F} {G} {H} + } + + +RingCat : ∀{c ℓ} → Category _ _ _ +RingCat {c} {ℓ} = + record { Obj = Ring c ℓ + ; Hom = _-Ring⟶_ + ; Id = RingId + ; _o_ = _∘_ + ; _≈_ = _≈_ + ; isCategory = isCategory + } + where + isCategory : IsCategory (Ring c ℓ) _-Ring⟶_ _≈_ _∘_ RingId + isCategory = + record { isEquivalence = ≈-isEquivalence {c} {ℓ} {c} {ℓ} + ; identityL = λ {R₁ R₂ f} → identityL {R₁} {R₂} {f} + ; identityR = λ {R₁ R₂ f} → identityR {R₁} {R₂} {f} + ; o-resp-≈ = λ {A} {B} {C} {f} {g} {h} {i} → o-resp-≈ {A} {B} {C} {f} {g} {h} {i} + ; associative = λ {R₁} {R₂} {R₃} {R₄} {f} {g} {h} → associative {R₁} {R₂} {R₃} {R₄} {f} {g} {h} + } + where + identityL : {R₁ R₂ : Ring c ℓ} {f : R₁ -Ring⟶ R₂} → (RingId ∘ f) ≈ f + identityL {f = f} = ≈-refl {F = f} + identityR : {R₁ R₂ : Ring c ℓ} {f : R₁ -Ring⟶ R₂} → (f ∘ RingId) ≈ f + identityR {f = f} = ≈-refl {F = f} + o-resp-≈ : {R₁ R₂ R₃ : Ring c ℓ} {f g : R₁ -Ring⟶ R₂} {h i : R₂ -Ring⟶ R₃} + → f ≈ g → h ≈ i → (h ∘ f) ≈ (i ∘ g) + o-resp-≈ {R₃ = R₃} {f} {g} {h} {i} f≈g h≈i x = + begin + ([ h ∘ f ] x) ≈⟨ h≈i ([ f ] x) ⟩ + ([ i ∘ f ] x) ≈⟨ _-Ring⟶_.⟦⟧-cong i (f≈g x) ⟩ + ([ i ∘ g ] x) + ∎ + where + module T = Ring R₃ + open IsEquivalence T.isEquivalence + open EqR T.setoid + associative : {R₁ R₂ R₃ R₄ : Ring c ℓ} {f : R₃ -Ring⟶ R₄} {g : R₂ -Ring⟶ R₃} {h : R₁ -Ring⟶ R₂} + → (f ∘ (g ∘ h)) ≈ ((f ∘ g) ∘ h) + associative {f = f} {g} {h} = ≈-refl {F = f ∘ (g ∘ h)} + + diff -r 71049ed05151 -r 45de2b31bf02 src/Category/Sets.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Sets.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,29 @@ +{-# OPTIONS --cubical-compatible --safe #-} + +module Category.Sets where +open import Category +open import Relation.Binary.Core +open import Relation.Binary +open import Level +open import Function +open import Relation.Binary.PropositionalEquality + +_==_ : ∀{ℓ} {a b : Set ℓ} → (f g : a → b) → Set ℓ +_==_ {_} {a} {b} f g = (x : a) → f x ≡ g x + +Sets : ∀{ℓ} → Category _ _ ℓ +Sets {ℓ} = record { Obj = Set ℓ + ; Hom = λ a b → a → b + ; _o_ = λ f g → f ∘ g + ; _≈_ = _==_ + ; isCategory = isCategory + } + where + isCategory : IsCategory (Set ℓ) (λ a b → a → b) _==_ (λ f g → f ∘ g) (λ x → x) + isCategory = record { isEquivalence = record {refl = λ x → refl + ; trans = λ i=j j=k x → trans (i=j x) (j=k x) ; sym = λ eq x → sym (eq x)} + ; identityL = λ x → refl + ; identityR = λ x → refl + ; o-resp-≈ = λ {c} {b} {a} {f} {g} {h} {i} f=g h=i x → trans (h=i (f x)) (cong i (f=g x)) + ; associative = λ x → refl + } diff -r 71049ed05151 -r 45de2b31bf02 src/Comma.agda --- a/src/Comma.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/Comma.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,10 +1,12 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Level open import Category module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁'' c₂'' ℓ''} {C : Category c₁' c₂' ℓ'} ( F : Functor A C ) ( G : Functor B C ) where open import HomReasoning -open import cat-utility +open import Definitions -- -- F G diff -r 71049ed05151 -r 45de2b31bf02 src/Comma1.agda --- a/src/Comma1.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/Comma1.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,10 +1,12 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Level open import Category module Comma1 {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} ( F : Functor A C ) ( G : Functor A C ) where open import HomReasoning -open import cat-utility +open import Definitions -- -- F G diff -r 71049ed05151 -r 45de2b31bf02 src/Definitions.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Definitions.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,639 @@ +{-# OPTIONS --cubical-compatible --safe #-} +module Definitions where + +-- Shinji KONO + + open import Level + open import Category + open import HomReasoning + + open Functor + + id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a + id1 A a = (Id {_} {_} {_} {A} a) + -- We cannot make A implicit + + -- + -- one to one (without naturality) + -- + record Iso {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) + (x y : Obj C ) + : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where + field + ≅→ : Hom C x y + ≅← : Hom C y x + iso→ : C [ C [ ≅← o ≅→ ] ≈ id1 C x ] + iso← : C [ C [ ≅→ o ≅← ] ≈ id1 C y ] + + ≡-iso : {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (x : Obj C ) → Iso C x x + ≡-iso C x = record { ≅→ = id1 C _ ; ≅← = id1 C _ ; iso→ = ≈-Reasoning.idL C ; iso← = ≈-Reasoning.idL C } + sym-iso : {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) {x y : Obj C } → Iso C x y → Iso C y x + sym-iso C i = record { ≅→ = Iso.≅← i ; ≅← = Iso.≅→ i ; iso→ = Iso.iso← i ; iso← = Iso.iso→ i } + + -- Iso with cong + -- + record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B ) + : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where + field + ≅→ : Hom A a b → Hom B a' b' + ≅← : Hom B a' b' → Hom A a b + iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ] + iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ] + cong→ : {f g : Hom A a b } → A [ f ≈ g ] → B [ ≅→ f ≈ ≅→ g ] + cong← : {f g : Hom B a' b'} → B [ f ≈ g ] → A [ ≅← f ≈ ≅← g ] + + -- F(f) + -- F(a) ---→ F(b) + -- | | + -- |t(a) |t(b) G(f)t(a) = t(b)F(f) + -- | | + -- v v + -- G(a) ---→ G(b) + -- G(f) + + record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) + ( F G : Functor D C ) + (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A)) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + field + commute : {a b : Obj D} {f : Hom D a b} + → C [ C [ ( FMap G f ) o ( TMap a ) ] ≈ C [ (TMap b ) o (FMap F f) ] ] + + record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) + (F G : Functor domain codomain ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + field + TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) + isNTrans : IsNTrans domain codomain F G TMap + + ---- + -- C is locally small i.e. Hom C i j is a set c₁ + -- + open import Relation.Binary.PropositionalEquality using (_≡_) + record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + hom→ : {i j : Obj C } → Hom C i j → I + hom← : {i j : Obj C } → ( f : I ) → Hom C i j + hom-iso : {i j : Obj C } → { f : Hom C i j } → C [ hom← ( hom→ f ) ≈ f ] + hom-rev : {i j : Obj C } → { f : I } → hom→ ( hom← {i} {j} f ) ≡ f + ≡←≈ : {i j : Obj C } → { f g : Hom C i j } → C [ f ≈ g ] → f ≡ g + + record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + ( U : Functor B A ) + ( F : Obj A → Obj B ) + ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) + ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + universalMapping : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → + A [ A [ FMap U ( f * ) o η a ] ≈ f ] + uniquness : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g : Hom B (F a) b } → + A [ A [ FMap U g o η a ] ≈ f ] → B [ f * ≈ g ] + + record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + ( U : Functor B A ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + infixr 11 _* + field + F : Obj A → Obj B + η : (a : Obj A) → Hom A a ( FObj U (F a) ) + _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b + isUniversalMapping : IsUniversalMapping A B U F η _* + + record coIsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + ( F : Functor A B ) + ( U : Obj B → Obj A ) + ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b ) + ( _* : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b ) ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + couniversalMapping : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → + B [ B [ ε b o FMap F ( f * ) ] ≈ f ] + uniquness : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → { g : Hom A a (U b) } → + B [ B [ ε b o FMap F g ] ≈ f ] → A [ f * ≈ g ] + + record coUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + ( F : Functor A B ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + infixr 11 _* + field + U : Obj B → Obj A + ε : (b : Obj B) → Hom B ( FObj F (U b) ) b + _* : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b ) + iscoUniversalMapping : coIsUniversalMapping A B F U ε _* + + open NTrans + open import Category.Cat + record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + ( U : Functor B A ) + ( F : Functor A B ) + ( η : NTrans A A identityFunctor ( U ○ F ) ) + ( ε : NTrans B B ( F ○ U ) identityFunctor ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + adjoint1 : { b : Obj B } → + A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ] + adjoint2 : {a : Obj A} → + B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ] + + record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + U : Functor B A + F : Functor A B + η : NTrans A A identityFunctor ( U ○ F ) + ε : NTrans B B ( F ○ U ) identityFunctor + isAdjunction : IsAdjunction A B U F η ε + U-functor = U + F-functor = F + Eta = η + Epsiron = ε + + + record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + ( T : Functor A A ) + ( η : NTrans A A identityFunctor T ) + ( μ : NTrans A A (T ○ T) T) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + assoc : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] + unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] + unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] + + record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + T : Functor A A + η : NTrans A A identityFunctor T + μ : NTrans A A (T ○ T) T + isMonad : IsMonad A T η μ + -- g ○ f = μ(c) T(g) f + join : { a b : Obj A } → { c : Obj A } → + ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) + join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ] + + record IsCoMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + ( S : Functor A A ) + ( ε : NTrans A A S identityFunctor ) + ( δ : NTrans A A S (S ○ S) ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + assoc : {a : Obj A} → A [ A [ TMap δ (FObj S a) o TMap δ a ] ≈ A [ FMap S (TMap δ a) o TMap δ a ] ] + unity1 : {a : Obj A} → A [ A [ TMap ε ( FObj S a ) o TMap δ a ] ≈ Id {_} {_} {_} {A} (FObj S a) ] + unity2 : {a : Obj A} → A [ A [ (FMap S (TMap ε a )) o TMap δ a ] ≈ Id {_} {_} {_} {A} (FObj S a) ] + + record coMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Functor A A) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + ε : NTrans A A S identityFunctor + δ : NTrans A A S (S ○ S) + isCoMonad : IsCoMonad A S ε δ + -- g ○ f = g S(f) δ(a) + coJoin : { a b : Obj A } → { c : Obj A } → + ( Hom A (FObj S b ) c ) → ( Hom A ( FObj S a) b ) → Hom A ( FObj S a ) c + coJoin {a} {_} {_} g f = A [ A [ g o FMap S f ] o TMap δ a ] + + open NTrans + nat : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} + {a b : Obj D} {f : Hom D a b} {F G : Functor D A } + → (η : NTrans D A F G ) + → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ] + nat η = IsNTrans.commute ( isNTrans η ) + + nat1 : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} + {a b : Obj D} {F G : Functor D A } + → (η : NTrans D A F G ) → (f : Hom D a b) + → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ] + nat1 η f = IsNTrans.commute ( isNTrans η ) + + + Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') + (F : Functor B C) → { G H : Functor A B } → ( n : NTrans A B G H ) → NTrans A C (F ○ G) (F ○ H) + Functor*Nat A {B} C F {G} {H} n = record { + TMap = λ a → FMap F (TMap n a) + ; isNTrans = record { + commute = commute + } + } where + commute : {a b : Obj A} {f : Hom A a b} + → C [ C [ (FMap F ( FMap H f )) o ( FMap F (TMap n a)) ] ≈ C [ (FMap F (TMap n b )) o (FMap F (FMap G f)) ] ] + commute {a} {b} {f} = let open ≈-Reasoning (C) in + begin + (FMap F ( FMap H f )) o ( FMap F (TMap n a)) + ≈⟨ sym (distr F) ⟩ + FMap F ( B [ (FMap H f) o TMap n a ]) + ≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩ + FMap F ( B [ (TMap n b ) o FMap G f ] ) + ≈⟨ distr F ⟩ + (FMap F (TMap n b )) o (FMap F (FMap G f)) + ∎ + + Nat*Functor : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') + { G H : Functor B C } → ( n : NTrans B C G H ) → (F : Functor A B) → NTrans A C (G ○ F) (H ○ F) + Nat*Functor A {B} C {G} {H} n F = record { + TMap = λ a → TMap n (FObj F a) + ; isNTrans = record { + commute = commute + } + } where + commute : {a b : Obj A} {f : Hom A a b} + → C [ C [ ( FMap H (FMap F f )) o ( TMap n (FObj F a)) ] ≈ C [ (TMap n (FObj F b )) o (FMap G (FMap F f)) ] ] + commute {a} {b} {f} = IsNTrans.commute ( isNTrans n) + + -- T ≃ (U_R ○ F_R) + -- μ = U_R ε F_R + -- nat-ε + -- nat-η -- same as η but has different types + + record MResolution {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁' c₂' ℓ' ) ( M : Monad A ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + UR : Functor B A + FR : Functor A B + ηR : NTrans A A identityFunctor ( UR ○ FR ) + εR : NTrans B B ( FR ○ UR ) identityFunctor + μR : NTrans A A ( (UR ○ FR) ○ ( UR ○ FR )) ( UR ○ FR ) + Adj : IsAdjunction A B UR FR ηR εR + T=UF : Monad.T M ≃ (UR ○ FR) + μ=UεF : {x : Obj A } → A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ] + -- ηR=η : {x : Obj A } → A [ TMap ηR x ≈ TMap η x ] -- We need T → UR FR conversion + -- μR=μ : {x : Obj A } → A [ TMap μR x ≈ TMap μ x ] + + + -- + -- e f e + -- c -------→ a ---------→ b -------→ c + -- ↑ . ---------→ . | + -- | . g . | + -- |k . . | k + -- | . h h . ↓ + -- d d + + record IsEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] + k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c + ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ] + uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → + A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] + equalizer1 : Hom A c a + equalizer1 = e + + record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + equalizer-c : Obj A + equalizer : Hom A equalizer-c a + isEqualizer : IsEqualizer A equalizer f g + + record IsCoEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A b c) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + ef=eg : A [ A [ e o f ] ≈ A [ e o g ] ] + k : {d : Obj A} (h : Hom A b d) → A [ A [ h o f ] ≈ A [ h o g ] ] → Hom A c d + ke=h : {d : Obj A} → ∀ {h : Hom A b d } → {eq : A [ A [ h o f ] ≈ A [ h o g ] ] } → A [ A [ k {d} h eq o e ] ≈ h ] + uniqueness : {d : Obj A} → ∀ {h : Hom A b d } → {eq : A [ A [ h o f ] ≈ A [ h o g ] ] } → {k' : Hom A c d} → + A [ A [ k' o e ] ≈ h ] → A [ k {d} h eq ≈ k' ] + equalizer1 : Hom A b c + equalizer1 = e + + record CoEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + coEqualizer-c : Obj A + coEqualizer : Hom A coEqualizer-c a + isCoEqualizer : IsEqualizer A coEqualizer f g + + -- + -- Product + -- + -- c + -- f | g + -- |f×g + -- v + -- a <-------- ab ---------→ b + -- π1 π2 + + + record IsProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A) + ( π1 : Hom A ab a ) + ( π2 : Hom A ab b ) + : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + _×_ : {c : Obj A} ( f : Hom A c a ) → ( g : Hom A c b ) → Hom A c ab + π1fxg=f : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π1 o ( f × g ) ] ≈ f ] + π2fxg=g : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π2 o ( f × g ) ] ≈ g ] + uniqueness : {c : Obj A} { h : Hom A c ab } → A [ ( A [ π1 o h ] ) × ( A [ π2 o h ] ) ≈ h ] + ×-cong : {c : Obj A} { f f' : Hom A c a } → { g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f × g ≈ f' × g' ] + + record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( a b : Obj A ) + : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + product : Obj A + π1 : Hom A product a + π2 : Hom A product b + isProduct : IsProduct A a b product π1 π2 + + record IsCoProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A) + ( κ1 : Hom A a ab ) + ( κ2 : Hom A b ab ) + : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + _+_ : {c : Obj A} ( f : Hom A a c ) → ( g : Hom A b c ) → Hom A ab c + κ1f+g=f : {c : Obj A} { f : Hom A a c } → { g : Hom A b c } → A [ A [ ( f + g ) o κ1 ] ≈ f ] + κ2f+g=g : {c : Obj A} { f : Hom A a c } → { g : Hom A b c } → A [ A [ ( f + g ) o κ2 ] ≈ g ] + uniqueness : {c : Obj A} { h : Hom A ab c } → A [ ( A [ h o κ1 ] ) + ( A [ h o κ2 ] ) ≈ h ] + +-cong : {c : Obj A} { f f' : Hom A a c } → { g g' : Hom A b c } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f + g ≈ f' + g' ] + + record coProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( a b : Obj A ) + : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + coproduct : Obj A + κ1 : Hom A a coproduct + κ2 : Hom A b coproduct + isProduct : IsCoProduct A a b coproduct κ1 κ2 + + ----- + -- + -- product on arbitrary index + -- + + record IsIProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) + ( p : Obj A ) -- product + ( ai : I → Obj A ) -- families + ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections + : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where + field + iproduct : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p + pif=q : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } + → ∀ { i : I } → A [ A [ ( pi i ) o ( iproduct qi ) ] ≈ (qi i) ] + ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] + ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } + → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ] + -- another form of uniquness + ip-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p ) + → ( ∀ { i : I } → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] ) + → A [ product' ≈ iproduct qi ] + ip-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin + product' + ≈↑⟨ ip-uniqueness ⟩ + iproduct (λ i₁ → A [ pi i₁ o product' ]) + ≈⟨ ip-cong ( λ i → begin + pi i o product' + ≈⟨ eq {i} ⟩ + qi i + ∎ ) ⟩ + iproduct qi + ∎ + + record IProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) (ai : I → Obj A) : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where + field + iprod : Obj A + pi : (i : I ) → Hom A iprod ( ai i ) + isIProduct : IsIProduct I A iprod ai pi + + record IsICoProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) + ( p : Obj A ) -- coproduct + ( ci : I → Obj A ) -- cases + ( ki : (i : I ) → Hom A ( ci i ) p ) -- coprojections + : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where + field + icoproduct : {q : Obj A} → ( qi : (i : I) → Hom A (ci i) q ) → Hom A p q + kif=q : {q : Obj A} → { qi : (i : I) → Hom A (ci i) q } + → ∀ { i : I } → A [ A [ ( icoproduct qi ) o ( ki i ) ] ≈ (qi i) ] + icp-uniqueness : {q : Obj A} { h : Hom A p q } → A [ icoproduct ( λ (i : I) → A [ h o (ki i) ] ) ≈ h ] + icp-cong : {q : Obj A} → { qi : (i : I) → Hom A (ci i) q} → { qi' : (i : I) → Hom A (ci i) q } + → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ icoproduct qi ≈ icoproduct qi' ] + -- another form of uniquness + icp-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A (ci i) q ) → ( product' : Hom A p q ) + → ( ∀ { i : I } → A [ A [ product' o ( ki i )] ≈ (qi i) ] ) + → A [ product' ≈ icoproduct qi ] + icp-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin + product' + ≈↑⟨ icp-uniqueness ⟩ + icoproduct (λ i₁ → A [ product' o ki i₁ ]) + ≈⟨ icp-cong ( λ i → begin + product' o ki i + ≈⟨ eq {i} ⟩ + qi i + ∎ ) ⟩ + icoproduct qi + ∎ + + record ICoProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) (ci : I → Obj A) : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where + field + icoprod : Obj A + ki : (i : I ) → Hom A ( ci i ) icoprod + isICoProduct : IsICoProduct I A icoprod ci ki + + + -- Pullback + -- f + -- a ------→ c + -- ^ ^ + -- π1 | |g + -- | | + -- ab ------→ b + -- ^ π2 + -- | + -- d + -- + record IsPullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b c ab : Obj A} + ( f : Hom A a c ) ( g : Hom A b c ) + ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) + : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + commute : A [ A [ f o π1 ] ≈ A [ g o π2 ] ] + pullback : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d ab + π1p=π1 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } + → A [ A [ π1 o pullback eq ] ≈ π1' ] + π2p=π2 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } + → A [ A [ π2 o pullback eq ] ≈ π2' ] + uniqueness : { d : Obj A } → ( p' : Hom A d ab ) → ( π1' : Hom A d a ) ( π2' : Hom A d b ) → ( eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] ) + → ( π1p=π1' : A [ A [ π1 o p' ] ≈ π1' ] ) + → ( π2p=π2' : A [ A [ π2 o p' ] ≈ π2' ] ) + → A [ pullback eq ≈ p' ] + + record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b c : Obj A} + ( f : Hom A a c ) ( g : Hom A b c ) + : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + ab : Obj A + π1 : Hom A ab a + π2 : Hom A ab b + isPullback : IsPullback A f g π1 π2 + + -- + -- Limit + -- + ----- + + -- Constancy Functor + + K : { c₁' c₂' ℓ' : Level} (I : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( A : Category c₁'' c₂'' ℓ'' ) + → ( a : Obj A ) → Functor I A + K I A a = record { + FObj = λ i → a ; + FMap = λ f → id1 A a ; + isFunctor = let open ≈-Reasoning (A) in record { + ≈-cong = λ f=g → refl-hom + ; identity = refl-hom + ; distr = sym idL + } + } + + + record IsLimit { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) + (a0 : Obj A ) (t0 : NTrans I A ( K I A a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where + field + limit : ( a : Obj A ) → ( t : NTrans I A ( K I A a ) Γ ) → Hom A a a0 + t0f=t : { a : Obj A } → { t : NTrans I A ( K I A a ) Γ } → ∀ { i : Obj I } → + A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ] + limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K I A a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } → + A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ] + + record Limit { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) + : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where + field + a0 : Obj A + t0 : NTrans I A ( K I A a0 ) Γ + isLimit : IsLimit I A Γ a0 t0 + + LimitNat : { c₁' c₂' ℓ' : Level} (I : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( B : Category c₁ c₂ ℓ ) { c₁'' c₂'' ℓ'' : Level} + ( C : Category c₁'' c₂'' ℓ'' ) + ( Γ : Functor I B ) + ( lim : Obj B ) ( tb : NTrans I B ( K I B lim ) Γ ) → + ( U : Functor B C) → NTrans I C ( K I C (FObj U lim) ) (U ○ Γ) + LimitNat I B C Γ lim tb U = record { + TMap = TMap (Functor*Nat I C U tb) ; + isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (C) in begin + FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a + ≈⟨ nat ( Functor*Nat I C U tb ) ⟩ + TMap (Functor*Nat I C U tb) b o FMap (U ○ K I B lim) f + ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩ + TMap (Functor*Nat I C U tb) b o FMap (K I C (FObj U lim)) f + ∎ + } } + + open Limit + record LimitPreserve { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) + { c₁'' c₂'' ℓ'' : Level} ( C : Category c₁'' c₂'' ℓ'' ) + (G : Functor A C) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁'' ⊔ c₂'' ⊔ ℓ'' )) where + field + preserve : ( Γ : Functor I A ) → ( limita : Limit I A Γ ) → + IsLimit I C (G ○ Γ) (FObj G (a0 limita ) ) (LimitNat I A C Γ (a0 limita ) (t0 limita) G ) + plimit : { Γ : Functor I A } → ( limita : Limit I A Γ ) → Limit I C (G ○ Γ ) + plimit {Γ} limita = record { a0 = (FObj G (a0 limita )) + ; t0 = LimitNat I A C Γ (a0 limita ) (t0 limita) G + ; isLimit = preserve Γ limita } + + record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) + : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where + field + climit : ( Γ : Functor I A ) → Limit I A Γ + cproduct : ( I : Set c₁' ) (fi : I → Obj A ) → IProduct I A fi -- c₁ should be a free level + cequalizer : {a b : Obj A} (f g : Hom A a b) → Equalizer A f g + open Limit + limit-c : ( Γ : Functor I A ) → Obj A + limit-c Γ = a0 ( climit Γ) + limit-u : ( Γ : Functor I A ) → NTrans I A ( K I A (limit-c Γ )) Γ + limit-u Γ = t0 ( climit Γ) + open Equalizer + equalizer-p : {a b : Obj A} (f g : Hom A a b) → Obj A + equalizer-p f g = equalizer-c (cequalizer f g ) + equalizer-e : {a b : Obj A} (f g : Hom A a b) → Hom A (equalizer-p f g) a + equalizer-e f g = equalizer (cequalizer f g ) + + +-- initial object + + record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where + field + initial : ∀( a : Obj A ) → Hom A i a + uniqueness : { a : Obj A } → ( f : Hom A i a ) → A [ f ≈ initial a ] + + record InitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where + field + initialObject : Obj A + hasInitialObject : HasInitialObject A initialObject + + open import Category.Sets + + Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y ) + (a : Obj A) → Functor (Category.op A) (Sets {c₂}) + Yoneda {c₁} {c₂} {ℓ} A ≡←≈ a = record { + FObj = λ b → Hom (Category.op A) a b + ; FMap = λ {x} {y} (f : Hom A y x ) → λ ( g : Hom A x a ) → (Category.op A) [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) + ; isFunctor = record { + identity = λ {b} x → ≡←≈ idL + ; distr = λ {a} {b} {c} {f} {g} x → ≡←≈ ( sym assoc ) + ; ≈-cong = λ eq x → ≡←≈ ( resp refl-hom eq ) + } + } where + open ≈-Reasoning (Category.op A) + + -- + -- better than ≡←≈ + -- + Cong≈ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Set (c₁ ⊔ c₂ ⊔ ℓ) + Cong≈ A a = {c b : Obj A} (f : Hom A a c → Hom A a b ) + {x y : Hom A a c} → A [ x ≈ y ] → A [ f x ≈ f y ] where + open ≈-Reasoning A + + Sets≈ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Cong≈ A a → Category c₁ c₂ (c₂ ⊔ ℓ) + Sets≈ A a ≈-cong = record { Obj = Obj A + ; Hom = λ b c → Hom (Category.op A) b a → Hom (Category.op A) c a + ; _o_ = λ f g x → f (g x ) + ; _≈_ = λ {b} f g → (x : Hom (Category.op A) b a) → f x ≈ g x + ; isCategory = record { isEquivalence = record {refl = λ x → refl-hom + ; trans = λ i=j j=k x → trans-hom (i=j x) (j=k x) ; sym = λ eq x → sym-hom (eq x)} + ; identityL = λ x → refl-hom + ; identityR = λ x → refl-hom + ; o-resp-≈ = λ {c} {b} {a} {f} {g} {h} {i} f=g h=i x → trans-hom (h=i (f x)) ( ≈-cong i (f=g x) ) + ; associative = λ x → refl-hom } + } where + open ≈-Reasoning A + + Yoneda≈ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) + (a : Obj A) → (≈-cong : Cong≈ (Category.op A) a ) → Functor (Category.op A) (Sets≈ (Category.op A) a ≈-cong) + Yoneda≈ {c₁} {c₂} {ℓ} A a ≈-cong = record { + FObj = λ b → b + ; FMap = λ {x} {y} (f : Hom A y x ) ( g : Hom A x a ) → A [ g o f ] + ; isFunctor = record { + identity = λ {b} x → idR + ; distr = λ {a} {b} {c} {f} {g} x → assoc + ; ≈-cong = λ eq x → resp eq refl-hom + } + } where + open ≈-Reasoning A + + -- + -- Representable U ≈　Hom(A,-) + + record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) + ( ≡←≈ : {a b : Obj A } { x y : Hom A b a } → (x≈y : (Category.op A) [ x ≈ y ]) → x ≡ y ) + ( U : Functor (Category.op A) (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where + field + -- FObj U x : A → Set + -- FMap U f = Set → Set (locally small) + -- λ b → Hom (a,b) : A → Set + -- λ f → Hom (a,-) = λ b → Hom a b + + repr→ : NTrans (Category.op A) (Sets {c₂}) U (Yoneda A ≡←≈ a ) + repr← : NTrans (Category.op A) (Sets {c₂}) (Yoneda A ≡←≈ a) U + reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A ≡←≈ a) x )] + reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] + + + record Representable≈ { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) + ( ≡←≈ : {a b : Obj A } { x y : Hom A b a } → (x≈y : (Category.op A) [ x ≈ y ]) → x ≡ y ) + (≈-cong : (a : Obj A) → Cong≈ (Category.op A) a ) + (a : Obj A) + ( U : Functor (Category.op A) (Sets≈ (Category.op A) a (≈-cong a)) ) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where + field + repr→ : NTrans (Category.op A) (Sets≈ (Category.op A) a (≈-cong a)) U (Yoneda≈ A a (≈-cong a)) + repr← : NTrans (Category.op A) (Sets≈ (Category.op A) a (≈-cong a)) (Yoneda≈ A a (≈-cong a)) U + reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] + ≈ id1 (Sets≈ (Category.op A) a (≈-cong a)) (FObj (Yoneda≈ A a (≈-cong a)) x )] + reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] + ≈ id1 (Sets≈ (Category.op A) a (≈-cong a)) (FObj U x)] + + diff -r 71049ed05151 -r 45de2b31bf02 src/HomReasoning.agda --- a/src/HomReasoning.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/HomReasoning.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,37 +1,14 @@ +{-# OPTIONS --cubical-compatible --safe #-} module HomReasoning where -- Shinji KONO -open import Category -- https://github.com/konn/category-agda open import Level -open Functor - --- F(f) --- F(a) ---→ F(b) --- | | --- |t(a) |t(b) G(f)t(a) = t(b)F(f) --- | | --- v v --- G(a) ---→ G(b) --- G(f) - -record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) - ( F G : Functor D C ) - (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A)) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where - field - commute : {a b : Obj D} {f : Hom D a b} - → C [ C [ ( FMap G f ) o ( TMap a ) ] ≈ C [ (TMap b ) o (FMap F f) ] ] - -record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) - (F G : Functor domain codomain ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where - field - TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) - isNTrans : IsNTrans domain codomain F G TMap +open import Category module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where open import Relation.Binary + open Functor _o_ : {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b x o y = A [ x o y ] @@ -125,19 +102,6 @@ { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} {a b : Obj C} {f g : Hom C a b} → (T : Functor C D) → C [ f ≈ g ] → D [ FMap T f ≈ FMap T g ] fcong T = IsFunctor.≈-cong (isFunctor T) - open NTrans - nat : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} - {a b : Obj D} {f : Hom D a b} {F G : Functor D A } - → (η : NTrans D A F G ) - → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ] - nat η = IsNTrans.commute ( isNTrans η ) - - nat1 : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} - {a b : Obj D} {F G : Functor D A } - → (η : NTrans D A F G ) → (f : Hom D a b) - → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ] - nat1 η f = IsNTrans.commute ( isNTrans η ) - infix 3 _∎ infixr 2 _≈⟨_⟩_ _≈⟨⟩_ infixr 2 _≈↑⟨_⟩_ diff -r 71049ed05151 -r 45de2b31bf02 src/Polynominal.agda --- a/src/Polynominal.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/Polynominal.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,10 +1,11 @@ -{-# OPTIONS --allow-unsolved-metas #-} +-- {-# OPTIONS --cubical-compatible #-} + open import Category open import CCC open import Level open import HomReasoning -open import cat-utility +open import Definitions open import Relation.Nullary open import Data.Empty open import Data.Product renaming ( <_,_> to ⟪_,_⟫ ) @@ -12,7 +13,7 @@ module Polynominal { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( C : CCC A ) where open CCC.CCC C - open ≈-Reasoning A hiding (_∙_) + open ≈-Reasoning A -- hiding (_∙_) _∙_ = _[_o_] A diff -r 71049ed05151 -r 45de2b31bf02 src/S.agda --- a/src/S.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/S.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,3 +1,4 @@ + --I'd like to write the Limit in Sets Category using Agda. Assuming local smallness, a functor is a pair of map on Set OC and I, like this. -- -- sobj : OC → Set c₂ @@ -8,12 +9,13 @@ -- --In the following agda code, I'd like to prove snat-cong lemma. + -- {-# OPTIONS --cubical-compatible --safe #-} open import Level module S where open import Relation.Binary.Core open import Function - import Relation.Binary.PropositionalEquality + open import Relation.Binary.PropositionalEquality open import Relation.Binary.HeterogeneousEquality using (_≅_;refl) record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) diff -r 71049ed05151 -r 45de2b31bf02 src/SetsCompleteness.agda --- a/src/SetsCompleteness.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/SetsCompleteness.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,10 +1,12 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Category -- https://github.com/konn/category-agda open import Level open import Category.Sets renaming ( _o_ to _*_ ) module SetsCompleteness where -open import cat-utility +open import Definitions open import Relation.Binary.Core open import Function import Relation.Binary.PropositionalEquality @@ -79,13 +81,13 @@ ipcx {q} {qi} {qi'} qi=qi x = begin record { pi1 = λ i → (qi i) x } - ≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡cong ( λ f → f x ) (qi=qi i) )) ⟩ + ≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ? ⟩ -- ( extensionality Sets (λ i → ≡cong ( λ f → f x ) (qi=qi i) )) ⟩ record { pi1 = λ i → (qi' i) x } ∎ where open import Relation.Binary.PropositionalEquality open ≡-Reasoning ip-cong : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 qi ≈ iproduct1 qi' ] - ip-cong {q} {qi} {qi'} qi=qi = extensionality Sets ( ipcx qi=qi ) + ip-cong {q} {qi} {qi'} qi=qi = ? -- extensionality Sets ( ipcx qi=qi ) data coproduct {c} (a b : Set c) : Set c where k1 : ( i : a ) → coproduct a b @@ -98,8 +100,8 @@ ; κ2 = λ i → k2 i ; isProduct = record { _+_ = sum - ; κ1f+g=f = extensionality Sets (λ x → refl ) - ; κ2f+g=g = extensionality Sets (λ x → refl ) + ; κ1f+g=f = ? -- extensionality Sets (λ x → refl ) + ; κ2f+g=g = ? -- extensionality Sets (λ x → refl ) ; uniqueness = λ {c} {h} → extensionality Sets (λ x → uniq {c} {h} x ) ; +-cong = λ {c} {f} {f'} {g} {g'} feq geq → extensionality Sets (pccong feq geq) } diff -r 71049ed05151 -r 45de2b31bf02 src/ToposEx.agda --- a/src/ToposEx.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/ToposEx.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,8 +1,11 @@ {-# OPTIONS --allow-unsolved-metas #-} + +-- {-# OPTIONS --cubical-compatible #-} + open import CCC open import Level open import Category -open import cat-utility +open import Definitions open import HomReasoning module ToposEx {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) (n : ToposNat A (CCC.１ c)) where @@ -322,7 +325,7 @@ nsuc (prop33.xnat (p f (g o π))) o initialNat (prop33.xnat (p f' (g' o π))) ∎ open Functor - open import Category.Sets hiding (_o_) + open import Category.Sets -- hiding (_o_) open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym) record Singleton (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ) where @@ -383,11 +386,11 @@ I : Set c₁ small : Small A I - open import yoneda A I small - - cs : CCC SetsAop - cs = {!!} - - toposS : Topos SetsAop cs - toposS = {!!} - +-- open import yoneda A I small +-- +-- cs : CCC SetsAop +-- cs = {!!} +-- +-- toposS : Topos SetsAop cs +-- toposS = {!!} +-- diff -r 71049ed05151 -r 45de2b31bf02 src/ToposIL.agda --- a/src/ToposIL.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/ToposIL.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,7 +1,11 @@ +{-# OPTIONS --allow-unsolved-metas #-} + +-- {-# OPTIONS --cubical-compatible --safe #-} + open import CCC open import Level open import Category -open import cat-utility +open import Definitions open import HomReasoning open import Data.List hiding ( [_] ) module ToposIL {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (n : ToposNat A (CCC.１ c)) where @@ -12,7 +16,7 @@ open CCC.CCC c open Functor - open import Category.Sets hiding (_o_) + open import Category.Sets hiding (_==_) open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym) open import Polynominal A c @@ -100,7 +104,7 @@ ; applyCong = {!!} } } where - open ≈-Reasoning A hiding (_∙_) + open ≈-Reasoning A -- hiding (_∙_) _⊢_ : {a b : Obj A} (p : Poly a (Topos.Ω t) b ) (q : Poly a (Topos.Ω t) b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) _⊢_ {a} {b} p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] → A [ Poly.f q ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] diff -r 71049ed05151 -r 45de2b31bf02 src/ToposSub.agda --- a/src/ToposSub.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/ToposSub.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,7 +1,11 @@ +{-# OPTIONS --allow-unsolved-metas #-} + +-- {-# OPTIONS --cubical-compatible --safe #-} + open import CCC open import Level open import Category -open import cat-utility +open import Definitions open import HomReasoning module ToposSub {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) (n : ToposNat A (CCC.１ c)) where diff -r 71049ed05151 -r 45de2b31bf02 src/adj-monad.agda --- a/src/adj-monad.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/adj-monad.agda Sat Oct 07 19:43:31 2023 +0900 @@ -5,11 +5,13 @@ --T(a) = t(a) --T(f) = tf(f) +{-# OPTIONS --cubical-compatible --safe #-} + open import Category -- https://github.com/konn/category-agda open import Level --open import Category.HomReasoning open import HomReasoning -open import cat-utility +open import Definitions open import Category.Cat module adj-monad where diff -r 71049ed05151 -r 45de2b31bf02 src/bi-ccc.agda --- a/src/bi-ccc.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/bi-ccc.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,10 +1,12 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module bi-ccc where open import Category open import CCC open import Level open import HomReasoning -open import cat-utility +open import Definitions record IsBICCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ⊥ : Obj A) -- ０ diff -r 71049ed05151 -r 45de2b31bf02 src/cat-utility.agda --- a/src/cat-utility.agda Thu Jul 20 12:36:15 2023 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,560 +0,0 @@ -module cat-utility where - --- Shinji KONO - - open import Category -- https://github.com/konn/category-agda - open import Level - --open import Category.HomReasoning - open import HomReasoning - - open Functor - - id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a - id1 A a = (Id {_} {_} {_} {A} a) - -- We cannot make A implicit - - -- - -- one to one (without naturality) - -- - record Iso {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) - (x y : Obj C ) - : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where - field - ≅→ : Hom C x y - ≅← : Hom C y x - iso→ : C [ C [ ≅← o ≅→ ] ≈ id1 C x ] - iso← : C [ C [ ≅→ o ≅← ] ≈ id1 C y ] - - ≡-iso : {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (x : Obj C ) → Iso C x x - ≡-iso C x = record { ≅→ = id1 C _ ; ≅← = id1 C _ ; iso→ = ≈-Reasoning.idL C ; iso← = ≈-Reasoning.idL C } - sym-iso : {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) {x y : Obj C } → Iso C x y → Iso C y x - sym-iso C i = record { ≅→ = Iso.≅← i ; ≅← = Iso.≅→ i ; iso→ = Iso.iso← i ; iso← = Iso.iso→ i } - - -- Iso with cong - -- - record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B ) - : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where - field - ≅→ : Hom A a b → Hom B a' b' - ≅← : Hom B a' b' → Hom A a b - iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ] - iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ] - cong→ : {f g : Hom A a b } → A [ f ≈ g ] → B [ ≅→ f ≈ ≅→ g ] - cong← : {f g : Hom B a' b'} → B [ f ≈ g ] → A [ ≅← f ≈ ≅← g ] - - record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - ( U : Functor B A ) - ( F : Obj A → Obj B ) - ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) - ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - field - universalMapping : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → - A [ A [ FMap U ( f * ) o η a ] ≈ f ] - uniquness : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g : Hom B (F a) b } → - A [ A [ FMap U g o η a ] ≈ f ] → B [ f * ≈ g ] - - record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - ( U : Functor B A ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - infixr 11 _* - field - F : Obj A → Obj B - η : (a : Obj A) → Hom A a ( FObj U (F a) ) - _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b - isUniversalMapping : IsUniversalMapping A B U F η _* - - record coIsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - ( F : Functor A B ) - ( U : Obj B → Obj A ) - ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b ) - ( _* : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b ) ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - field - couniversalMapping : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → - B [ B [ ε b o FMap F ( f * ) ] ≈ f ] - uniquness : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → { g : Hom A a (U b) } → - B [ B [ ε b o FMap F g ] ≈ f ] → A [ f * ≈ g ] - - record coUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - ( F : Functor A B ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - infixr 11 _* - field - U : Obj B → Obj A - ε : (b : Obj B) → Hom B ( FObj F (U b) ) b - _* : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b ) - iscoUniversalMapping : coIsUniversalMapping A B F U ε _* - - open NTrans - open import Category.Cat - record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - ( U : Functor B A ) - ( F : Functor A B ) - ( η : NTrans A A identityFunctor ( U ○ F ) ) - ( ε : NTrans B B ( F ○ U ) identityFunctor ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - field - adjoint1 : { b : Obj B } → - A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ] - adjoint2 : {a : Obj A} → - B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ] - - record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - field - U : Functor B A - F : Functor A B - η : NTrans A A identityFunctor ( U ○ F ) - ε : NTrans B B ( F ○ U ) identityFunctor - isAdjunction : IsAdjunction A B U F η ε - U-functor = U - F-functor = F - Eta = η - Epsiron = ε - - - record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - ( T : Functor A A ) - ( η : NTrans A A identityFunctor T ) - ( μ : NTrans A A (T ○ T) T) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - field - assoc : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] - unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] - unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] - - record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - field - T : Functor A A - η : NTrans A A identityFunctor T - μ : NTrans A A (T ○ T) T - isMonad : IsMonad A T η μ - -- g ○ f = μ(c) T(g) f - join : { a b : Obj A } → { c : Obj A } → - ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) - join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ] - - record IsCoMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - ( S : Functor A A ) - ( ε : NTrans A A S identityFunctor ) - ( δ : NTrans A A S (S ○ S) ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - field - assoc : {a : Obj A} → A [ A [ TMap δ (FObj S a) o TMap δ a ] ≈ A [ FMap S (TMap δ a) o TMap δ a ] ] - unity1 : {a : Obj A} → A [ A [ TMap ε ( FObj S a ) o TMap δ a ] ≈ Id {_} {_} {_} {A} (FObj S a) ] - unity2 : {a : Obj A} → A [ A [ (FMap S (TMap ε a )) o TMap δ a ] ≈ Id {_} {_} {_} {A} (FObj S a) ] - - record coMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Functor A A) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - field - ε : NTrans A A S identityFunctor - δ : NTrans A A S (S ○ S) - isCoMonad : IsCoMonad A S ε δ - -- g ○ f = g S(f) δ(a) - coJoin : { a b : Obj A } → { c : Obj A } → - ( Hom A (FObj S b ) c ) → ( Hom A ( FObj S a) b ) → Hom A ( FObj S a ) c - coJoin {a} {_} {_} g f = A [ A [ g o FMap S f ] o TMap δ a ] - - - Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') - (F : Functor B C) → { G H : Functor A B } → ( n : NTrans A B G H ) → NTrans A C (F ○ G) (F ○ H) - Functor*Nat A {B} C F {G} {H} n = record { - TMap = λ a → FMap F (TMap n a) - ; isNTrans = record { - commute = commute - } - } where - commute : {a b : Obj A} {f : Hom A a b} - → C [ C [ (FMap F ( FMap H f )) o ( FMap F (TMap n a)) ] ≈ C [ (FMap F (TMap n b )) o (FMap F (FMap G f)) ] ] - commute {a} {b} {f} = let open ≈-Reasoning (C) in - begin - (FMap F ( FMap H f )) o ( FMap F (TMap n a)) - ≈⟨ sym (distr F) ⟩ - FMap F ( B [ (FMap H f) o TMap n a ]) - ≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩ - FMap F ( B [ (TMap n b ) o FMap G f ] ) - ≈⟨ distr F ⟩ - (FMap F (TMap n b )) o (FMap F (FMap G f)) - ∎ - - Nat*Functor : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') - { G H : Functor B C } → ( n : NTrans B C G H ) → (F : Functor A B) → NTrans A C (G ○ F) (H ○ F) - Nat*Functor A {B} C {G} {H} n F = record { - TMap = λ a → TMap n (FObj F a) - ; isNTrans = record { - commute = commute - } - } where - commute : {a b : Obj A} {f : Hom A a b} - → C [ C [ ( FMap H (FMap F f )) o ( TMap n (FObj F a)) ] ≈ C [ (TMap n (FObj F b )) o (FMap G (FMap F f)) ] ] - commute {a} {b} {f} = IsNTrans.commute ( isNTrans n) - - -- T ≃ (U_R ○ F_R) - -- μ = U_R ε F_R - -- nat-ε - -- nat-η -- same as η but has different types - - record MResolution {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁' c₂' ℓ' ) ( M : Monad A ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - field - UR : Functor B A - FR : Functor A B - ηR : NTrans A A identityFunctor ( UR ○ FR ) - εR : NTrans B B ( FR ○ UR ) identityFunctor - μR : NTrans A A ( (UR ○ FR) ○ ( UR ○ FR )) ( UR ○ FR ) - Adj : IsAdjunction A B UR FR ηR εR - T=UF : Monad.T M ≃ (UR ○ FR) - μ=UεF : {x : Obj A } → A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ] - -- ηR=η : {x : Obj A } → A [ TMap ηR x ≈ TMap η x ] -- We need T → UR FR conversion - -- μR=μ : {x : Obj A } → A [ TMap μR x ≈ TMap μ x ] - - - -- - -- e f e - -- c -------→ a ---------→ b -------→ c - -- ↑ . ---------→ . | - -- | . g . | - -- |k . . | k - -- | . h h . ↓ - -- d d - - record IsEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where - field - fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] - k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c - ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ] - uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → - A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] - equalizer1 : Hom A c a - equalizer1 = e - - record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where - field - equalizer-c : Obj A - equalizer : Hom A equalizer-c a - isEqualizer : IsEqualizer A equalizer f g - - record IsCoEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A b c) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where - field - ef=eg : A [ A [ e o f ] ≈ A [ e o g ] ] - k : {d : Obj A} (h : Hom A b d) → A [ A [ h o f ] ≈ A [ h o g ] ] → Hom A c d - ke=h : {d : Obj A} → ∀ {h : Hom A b d } → {eq : A [ A [ h o f ] ≈ A [ h o g ] ] } → A [ A [ k {d} h eq o e ] ≈ h ] - uniqueness : {d : Obj A} → ∀ {h : Hom A b d } → {eq : A [ A [ h o f ] ≈ A [ h o g ] ] } → {k' : Hom A c d} → - A [ A [ k' o e ] ≈ h ] → A [ k {d} h eq ≈ k' ] - equalizer1 : Hom A b c - equalizer1 = e - - record CoEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where - field - coEqualizer-c : Obj A - coEqualizer : Hom A coEqualizer-c a - isCoEqualizer : IsEqualizer A coEqualizer f g - - -- - -- Product - -- - -- c - -- f | g - -- |f×g - -- v - -- a <-------- ab ---------→ b - -- π1 π2 - - - record IsProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A) - ( π1 : Hom A ab a ) - ( π2 : Hom A ab b ) - : Set (ℓ ⊔ (c₁ ⊔ c₂)) where - field - _×_ : {c : Obj A} ( f : Hom A c a ) → ( g : Hom A c b ) → Hom A c ab - π1fxg=f : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π1 o ( f × g ) ] ≈ f ] - π2fxg=g : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π2 o ( f × g ) ] ≈ g ] - uniqueness : {c : Obj A} { h : Hom A c ab } → A [ ( A [ π1 o h ] ) × ( A [ π2 o h ] ) ≈ h ] - ×-cong : {c : Obj A} { f f' : Hom A c a } → { g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f × g ≈ f' × g' ] - - record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( a b : Obj A ) - : Set (ℓ ⊔ (c₁ ⊔ c₂)) where - field - product : Obj A - π1 : Hom A product a - π2 : Hom A product b - isProduct : IsProduct A a b product π1 π2 - - record IsCoProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A) - ( κ1 : Hom A a ab ) - ( κ2 : Hom A b ab ) - : Set (ℓ ⊔ (c₁ ⊔ c₂)) where - field - _+_ : {c : Obj A} ( f : Hom A a c ) → ( g : Hom A b c ) → Hom A ab c - κ1f+g=f : {c : Obj A} { f : Hom A a c } → { g : Hom A b c } → A [ A [ ( f + g ) o κ1 ] ≈ f ] - κ2f+g=g : {c : Obj A} { f : Hom A a c } → { g : Hom A b c } → A [ A [ ( f + g ) o κ2 ] ≈ g ] - uniqueness : {c : Obj A} { h : Hom A ab c } → A [ ( A [ h o κ1 ] ) + ( A [ h o κ2 ] ) ≈ h ] - +-cong : {c : Obj A} { f f' : Hom A a c } → { g g' : Hom A b c } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f + g ≈ f' + g' ] - - record coProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( a b : Obj A ) - : Set (ℓ ⊔ (c₁ ⊔ c₂)) where - field - coproduct : Obj A - κ1 : Hom A a coproduct - κ2 : Hom A b coproduct - isProduct : IsCoProduct A a b coproduct κ1 κ2 - - ---- - -- C is locally small i.e. Hom C i j is a set c₁ - -- - open import Relation.Binary.PropositionalEquality using (_≡_) - record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - field - hom→ : {i j : Obj C } → Hom C i j → I - hom← : {i j : Obj C } → ( f : I ) → Hom C i j - hom-iso : {i j : Obj C } → { f : Hom C i j } → C [ hom← ( hom→ f ) ≈ f ] - hom-rev : {i j : Obj C } → { f : I } → hom→ ( hom← {i} {j} f ) ≡ f - ≡←≈ : {i j : Obj C } → { f g : Hom C i j } → C [ f ≈ g ] → f ≡ g - - ----- - -- - -- product on arbitrary index - -- - - record IsIProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) - ( p : Obj A ) -- product - ( ai : I → Obj A ) -- families - ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections - : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where - field - iproduct : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p - pif=q : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } - → ∀ { i : I } → A [ A [ ( pi i ) o ( iproduct qi ) ] ≈ (qi i) ] - ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] - ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } - → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ] - -- another form of uniquness - ip-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p ) - → ( ∀ { i : I } → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] ) - → A [ product' ≈ iproduct qi ] - ip-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin - product' - ≈↑⟨ ip-uniqueness ⟩ - iproduct (λ i₁ → A [ pi i₁ o product' ]) - ≈⟨ ip-cong ( λ i → begin - pi i o product' - ≈⟨ eq {i} ⟩ - qi i - ∎ ) ⟩ - iproduct qi - ∎ - - record IProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) (ai : I → Obj A) : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where - field - iprod : Obj A - pi : (i : I ) → Hom A iprod ( ai i ) - isIProduct : IsIProduct I A iprod ai pi - - record IsICoProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) - ( p : Obj A ) -- coproduct - ( ci : I → Obj A ) -- cases - ( ki : (i : I ) → Hom A ( ci i ) p ) -- coprojections - : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where - field - icoproduct : {q : Obj A} → ( qi : (i : I) → Hom A (ci i) q ) → Hom A p q - kif=q : {q : Obj A} → { qi : (i : I) → Hom A (ci i) q } - → ∀ { i : I } → A [ A [ ( icoproduct qi ) o ( ki i ) ] ≈ (qi i) ] - icp-uniqueness : {q : Obj A} { h : Hom A p q } → A [ icoproduct ( λ (i : I) → A [ h o (ki i) ] ) ≈ h ] - icp-cong : {q : Obj A} → { qi : (i : I) → Hom A (ci i) q} → { qi' : (i : I) → Hom A (ci i) q } - → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ icoproduct qi ≈ icoproduct qi' ] - -- another form of uniquness - icp-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A (ci i) q ) → ( product' : Hom A p q ) - → ( ∀ { i : I } → A [ A [ product' o ( ki i )] ≈ (qi i) ] ) - → A [ product' ≈ icoproduct qi ] - icp-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin - product' - ≈↑⟨ icp-uniqueness ⟩ - icoproduct (λ i₁ → A [ product' o ki i₁ ]) - ≈⟨ icp-cong ( λ i → begin - product' o ki i - ≈⟨ eq {i} ⟩ - qi i - ∎ ) ⟩ - icoproduct qi - ∎ - - record ICoProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) (ci : I → Obj A) : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where - field - icoprod : Obj A - ki : (i : I ) → Hom A ( ci i ) icoprod - isICoProduct : IsICoProduct I A icoprod ci ki - - - -- Pullback - -- f - -- a ------→ c - -- ^ ^ - -- π1 | |g - -- | | - -- ab ------→ b - -- ^ π2 - -- | - -- d - -- - record IsPullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b c ab : Obj A} - ( f : Hom A a c ) ( g : Hom A b c ) - ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) - : Set (ℓ ⊔ (c₁ ⊔ c₂)) where - field - commute : A [ A [ f o π1 ] ≈ A [ g o π2 ] ] - pullback : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d ab - π1p=π1 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } - → A [ A [ π1 o pullback eq ] ≈ π1' ] - π2p=π2 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } - → A [ A [ π2 o pullback eq ] ≈ π2' ] - uniqueness : { d : Obj A } → ( p' : Hom A d ab ) → ( π1' : Hom A d a ) ( π2' : Hom A d b ) → ( eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] ) - → ( π1p=π1' : A [ A [ π1 o p' ] ≈ π1' ] ) - → ( π2p=π2' : A [ A [ π2 o p' ] ≈ π2' ] ) - → A [ pullback eq ≈ p' ] - - record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b c : Obj A} - ( f : Hom A a c ) ( g : Hom A b c ) - : Set (ℓ ⊔ (c₁ ⊔ c₂)) where - field - ab : Obj A - π1 : Hom A ab a - π2 : Hom A ab b - isPullback : IsPullback A f g π1 π2 - - -- - -- Limit - -- - ----- - - -- Constancy Functor - - K : { c₁' c₂' ℓ' : Level} (I : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( A : Category c₁'' c₂'' ℓ'' ) - → ( a : Obj A ) → Functor I A - K I A a = record { - FObj = λ i → a ; - FMap = λ f → id1 A a ; - isFunctor = let open ≈-Reasoning (A) in record { - ≈-cong = λ f=g → refl-hom - ; identity = refl-hom - ; distr = sym idL - } - } - - - record IsLimit { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) - (a0 : Obj A ) (t0 : NTrans I A ( K I A a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where - field - limit : ( a : Obj A ) → ( t : NTrans I A ( K I A a ) Γ ) → Hom A a a0 - t0f=t : { a : Obj A } → { t : NTrans I A ( K I A a ) Γ } → ∀ { i : Obj I } → - A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ] - limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K I A a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } → - A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ] - - record Limit { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) - : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where - field - a0 : Obj A - t0 : NTrans I A ( K I A a0 ) Γ - isLimit : IsLimit I A Γ a0 t0 - - LimitNat : { c₁' c₂' ℓ' : Level} (I : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( B : Category c₁ c₂ ℓ ) { c₁'' c₂'' ℓ'' : Level} - ( C : Category c₁'' c₂'' ℓ'' ) - ( Γ : Functor I B ) - ( lim : Obj B ) ( tb : NTrans I B ( K I B lim ) Γ ) → - ( U : Functor B C) → NTrans I C ( K I C (FObj U lim) ) (U ○ Γ) - LimitNat I B C Γ lim tb U = record { - TMap = TMap (Functor*Nat I C U tb) ; - isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (C) in begin - FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a - ≈⟨ nat ( Functor*Nat I C U tb ) ⟩ - TMap (Functor*Nat I C U tb) b o FMap (U ○ K I B lim) f - ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩ - TMap (Functor*Nat I C U tb) b o FMap (K I C (FObj U lim)) f - ∎ - } } - - open Limit - record LimitPreserve { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) - { c₁'' c₂'' ℓ'' : Level} ( C : Category c₁'' c₂'' ℓ'' ) - (G : Functor A C) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁'' ⊔ c₂'' ⊔ ℓ'' )) where - field - preserve : ( Γ : Functor I A ) → ( limita : Limit I A Γ ) → - IsLimit I C (G ○ Γ) (FObj G (a0 limita ) ) (LimitNat I A C Γ (a0 limita ) (t0 limita) G ) - plimit : { Γ : Functor I A } → ( limita : Limit I A Γ ) → Limit I C (G ○ Γ ) - plimit {Γ} limita = record { a0 = (FObj G (a0 limita )) - ; t0 = LimitNat I A C Γ (a0 limita ) (t0 limita) G - ; isLimit = preserve Γ limita } - - record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) - : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where - field - climit : ( Γ : Functor I A ) → Limit I A Γ - cproduct : ( I : Set c₁' ) (fi : I → Obj A ) → IProduct I A fi -- c₁ should be a free level - cequalizer : {a b : Obj A} (f g : Hom A a b) → Equalizer A f g - open Limit - limit-c : ( Γ : Functor I A ) → Obj A - limit-c Γ = a0 ( climit Γ) - limit-u : ( Γ : Functor I A ) → NTrans I A ( K I A (limit-c Γ )) Γ - limit-u Γ = t0 ( climit Γ) - open Equalizer - equalizer-p : {a b : Obj A} (f g : Hom A a b) → Obj A - equalizer-p f g = equalizer-c (cequalizer f g ) - equalizer-e : {a b : Obj A} (f g : Hom A a b) → Hom A (equalizer-p f g) a - equalizer-e f g = equalizer (cequalizer f g ) - - --- initial object - - record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where - field - initial : ∀( a : Obj A ) → Hom A i a - uniqueness : { a : Obj A } → ( f : Hom A i a ) → A [ f ≈ initial a ] - - record InitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where - field - initialObject : Obj A - hasInitialObject : HasInitialObject A initialObject - - open import Category.Sets - import Axiom.Extensionality.Propositional - postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ - - Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y ) - (a : Obj A) → Functor (Category.op A) (Sets {c₂}) - Yoneda {c₁} {c₂} {ℓ} A ≡←≈ a = record { - FObj = λ b → Hom (Category.op A) a b - ; FMap = λ {x} {y} (f : Hom A y x ) → λ ( g : Hom A x a ) → (Category.op A) [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) - ; isFunctor = record { - identity = λ {b} → extensionality (Category.op A) ( λ x → lemma-y-obj1 {b} x ) ; - distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; - ≈-cong = λ eq → extensionality (Category.op A) ( λ x → lemma-y-obj3 x eq ) - } - } where - lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x - lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≡←≈ idL - lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ - (Category.op A) [ (Category.op A) [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x - lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≡←≈ ( sym assoc ) - lemma-y-obj3 : {b c : Obj A} {f g : Hom A c b } → (x : Hom A b a ) → (Category.op A) [ f ≈ g ] → (Category.op A) [ f o x ] ≡ (Category.op A) [ g o x ] - lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≡←≈ ( resp refl-hom eq ) - - -- Representable U ≈　Hom(A,-) - - record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) - ( ≡←≈ : {a b : Obj A } { x y : Hom A b a } → (x≈y : (Category.op A) [ x ≈ y ]) → x ≡ y ) - ( U : Functor (Category.op A) (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where - field - -- FObj U x : A → Set - -- FMap U f = Set → Set (locally small) - -- λ b → Hom (a,b) : A → Set - -- λ f → Hom (a,-) = λ b → Hom a b - - repr→ : NTrans (Category.op A) (Sets {c₂}) U (Yoneda A ≡←≈ a ) - repr← : NTrans (Category.op A) (Sets {c₂}) (Yoneda A ≡←≈ a) U - reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A ≡←≈ a) x )] - reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] - - diff -r 71049ed05151 -r 45de2b31bf02 src/category-ex.agda --- a/src/category-ex.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/category-ex.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,3 +1,5 @@ +-- {-# OPTIONS --cubical-compatible --safe #-} + module category-ex where open import Level diff -r 71049ed05151 -r 45de2b31bf02 src/code-data.agda --- a/src/code-data.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/code-data.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,8 +1,10 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Category -- https://github.com/konn/category-agda open import Level --open import Category.HomReasoning open import HomReasoning -open import cat-utility +open import Definitions open import Category.Cat module code-data { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where @@ -45,7 +47,7 @@ open import Relation.Binary.Core isDataCategory : IsCategory DataObj DataHom _≗_ _∙_ DataId -isDataCategory = record { isEquivalence = isEquivalence +isDataCategory = record { isEquivalence = record { refl = refl-hom ; sym = sym ; trans = trans-hom } ; identityL = \{a} {b} {f} -> identityL a b f ; identityR = \{a} {b} {f} -> identityR a b f ; o-resp-≈ = \{a} {b} {c} {f} {g} {h} {i} -> o-resp {a} {b} {c} {f} {g} {h} {i} @@ -99,13 +101,6 @@ ≈⟨ idR ⟩ continuation f ∎ - isEquivalence : {a : DataObj } {b : DataObj } → - IsEquivalence {_} {_} {DataHom a b } _≗_ - isEquivalence {C} {D} = -- this is the same function as A's equivalence but has different types - record { refl = refl-hom - ; sym = sym - ; trans = trans-hom - } DataCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ DataCategory = record { Obj = DataObj diff -r 71049ed05151 -r 45de2b31bf02 src/cokleisli.agda --- a/src/cokleisli.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/cokleisli.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,7 +1,9 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Category open import Level open import HomReasoning -open import cat-utility +open import Definitions module coKleisli { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where diff -r 71049ed05151 -r 45de2b31bf02 src/comparison-em.agda --- a/src/comparison-em.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/comparison-em.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + -- -- -- -- -- -- -- -- -- Comparison Functor of Eilenberg-Moore Category -- defines U^K and F^K as a resolution of Monad @@ -10,7 +12,7 @@ open import Level --open import Category.HomReasoning open import HomReasoning -open import cat-utility +open import Definitions open import Category.Cat open import Relation.Binary.Core diff -r 71049ed05151 -r 45de2b31bf02 src/comparison-functor.agda --- a/src/comparison-functor.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/comparison-functor.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + -- -- -- -- -- -- -- -- -- Comparison Functor of Kelisli Category -- defines U_K and F_K as a resolution of Monad @@ -10,7 +12,7 @@ open import Level --open import Category.HomReasoning open import HomReasoning -open import cat-utility +open import Definitions open import Category.Cat open import Relation.Binary.Core diff -r 71049ed05151 -r 45de2b31bf02 src/em-category.agda --- a/src/em-category.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/em-category.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + -- -- -- -- -- -- -- -- -- Monad to Eilenberg-Moore Category -- defines U^T and F^T as a resolution of Monad @@ -17,7 +19,7 @@ open import Level --open import Category.HomReasoning open import HomReasoning -open import cat-utility +open import Definitions open import Category.Cat module em-category { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } @@ -115,7 +117,7 @@ EMassoc {_} {_} {_} {_} {f} {g} {h} = ( IsCategory.associative (Category.isCategory A) ) isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_ EM-id -isEilenberg-MooreCategory = record { isEquivalence = isEquivalence +isEilenberg-MooreCategory = record { isEquivalence = record { refl = refl-hom ; sym = sym ; trans = trans-hom } ; identityL = IsCategory.identityL (Category.isCategory A) ; identityR = IsCategory.identityR (Category.isCategory A) ; o-resp-≈ = IsCategory.o-resp-≈ (Category.isCategory A) @@ -123,13 +125,6 @@ } where open ≈-Reasoning (A) - isEquivalence : {a : EMObj } {b : EMObj } → - IsEquivalence {_} {_} {EMHom a b } _≗_ - isEquivalence {C} {D} = -- this is the same function as A's equivalence but has different types - record { refl = refl-hom - ; sym = sym - ; trans = trans-hom - } Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ Eilenberg-MooreCategory = record { Obj = EMObj diff -r 71049ed05151 -r 45de2b31bf02 src/epi.agda --- a/src/epi.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/epi.agda Sat Oct 07 19:43:31 2023 +0900 @@ -162,7 +162,7 @@ monic arrow-ad arrow-ad _ refl = refl monic arrow-cd arrow-cd _ refl = refl -open import cat-utility +open import Definitions open import Relation.Nullary open import Data.Empty diff -r 71049ed05151 -r 45de2b31bf02 src/equalizer.agda --- a/src/equalizer.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/equalizer.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + --- -- -- Equalizer @@ -18,7 +20,7 @@ module equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where open import HomReasoning -open import cat-utility +open import Definitions -- -- Some obvious conditions for k (fe = ge) → ( fh = gh ) @@ -415,49 +417,49 @@ -- Bourroni equations gives an Equalizer -- -lemma-equ2 : {a b : Obj A} (f g : Hom A a b) → ( bur : Burroni ) → IsEqualizer A {equ bur f g} {a} {b} (α bur f g ) f g -lemma-equ2 {a} {b} f g bur = record { - fe=ge = fe=ge1 ; - k = k1 ; - ek=h = λ {d} {h} {eq} → ek=h1 {d} {h} {eq} ; - uniqueness = λ {d} {h} {eq} {k'} ek=h → uniqueness1 {d} {h} {eq} {k'} ek=h - } where - c : Obj A - c = equ bur f g - e : Hom A c a - e = α bur f g - k1 : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c - k1 {d} h fh=gh = β bur {d} {a} {b} f g h fh=gh - fe=ge1 : A [ A [ f o (α bur f g ) ] ≈ A [ g o (α bur f g ) ] ] - fe=ge1 = b1 bur f g - ek=h1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ (α bur f g ) o k1 {d} h eq ] ≈ h ] - ek=h1 {d} {h} {eq} = let open ≈-Reasoning (A) in - begin - α bur f g o k1 h eq - ≈⟨ assoc ⟩ - (α bur f g o γ bur f g h) o δ bur (f o h) (g o h) eq - ≈⟨ car (b2 bur f g) ⟩ - ( h o α bur ( f o h ) ( g o h ) ) o δ bur (f o h) (g o h) eq - ≈↑⟨ assoc ⟩ - h o α bur (f o h) (g o h) o δ bur (f o h) (g o h) eq - ≈⟨ cdr ( b3 bur (f o h) (g o h) eq ) ⟩ - h o id d - ≈⟨ idR ⟩ - h - ∎ - --- e f --- c -------→ a ---------→ b --- ^ . ---------→ --- | . g --- |k . --- | . h --- d - - postulate - uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → - A [ A [ (α bur f g ) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ] --- uniqueness1 {d} {h} {eq} {k'} ek=h = +-- emma-equ2 : {a b : Obj A} (f g : Hom A a b) → ( bur : Burroni ) → IsEqualizer A {equ bur f g} {a} {b} (α bur f g ) f g +-- emma-equ2 {a} {b} f g bur = record { +-- fe=ge = fe=ge1 ; +-- k = k1 ; +-- ek=h = λ {d} {h} {eq} → ek=h1 {d} {h} {eq} ; +-- uniqueness = λ {d} {h} {eq} {k'} ek=h → uniqueness1 {d} {h} {eq} {k'} ek=h +-- } where +-- c : Obj A +-- c = equ bur f g +-- e : Hom A c a +-- e = α bur f g +-- k1 : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c +-- k1 {d} h fh=gh = β bur {d} {a} {b} f g h fh=gh +-- fe=ge1 : A [ A [ f o (α bur f g ) ] ≈ A [ g o (α bur f g ) ] ] +-- fe=ge1 = b1 bur f g +-- ek=h1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ (α bur f g ) o k1 {d} h eq ] ≈ h ] +-- ek=h1 {d} {h} {eq} = let open ≈-Reasoning (A) in +-- begin +-- α bur f g o k1 h eq +-- ≈⟨ assoc ⟩ +-- (α bur f g o γ bur f g h) o δ bur (f o h) (g o h) eq +-- ≈⟨ car (b2 bur f g) ⟩ +-- ( h o α bur ( f o h ) ( g o h ) ) o δ bur (f o h) (g o h) eq +-- ≈↑⟨ assoc ⟩ +-- h o α bur (f o h) (g o h) o δ bur (f o h) (g o h) eq +-- ≈⟨ cdr ( b3 bur (f o h) (g o h) eq ) ⟩ +-- h o id d +-- ≈⟨ idR ⟩ +-- h +-- ∎ +-- +-- - e f +-- - c -------→ a ---------→ b +-- - ^ . ---------→ +-- - | . g +-- - |k . +-- - | . h +-- - d +-- +-- +-- uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → +-- A [ A [ (α bur f g ) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ] +-- uniqueness1 {d} {h} {eq} {k'} ek=h = -- begin -- k1 {d} h eq -- ≈⟨⟩ @@ -466,8 +468,8 @@ -- γ bur f g (α bur f g o k' ) o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g ))) -- ≈⟨ b4 bur f g ⟩ -- k' --- ∎ - +-- ∎ where open ≈-Reasoning A +-- -- end diff -r 71049ed05151 -r 45de2b31bf02 src/free-monoid.agda --- a/src/free-monoid.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/free-monoid.agda Sat Oct 07 19:43:31 2023 +0900 @@ -3,17 +3,19 @@ -- Shinji KONO +{-# OPTIONS --cubical-compatible --safe #-} + open import Category -- https://github.com/konn/category-agda open import Level module free-monoid { c c₁ c₂ ℓ : Level } where -open import Category.Sets +open import Category.Sets hiding (_==_) open import Category.Cat open import HomReasoning -open import cat-utility +open import Definitions open import Relation.Binary.Structures open import universal-mapping -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality -- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeMonoid.agda @@ -132,7 +134,7 @@ f == g → h == i → (h + f) == (i + g) o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f==g h==i = let open ≡-Reasoning in begin morph ( h + f ) - ≡⟨ ≡-cong ( λ g → ( ( λ (x : Carrier a ) → g x ) )) (extensionality (Sets ) {Carrier a} lemma11) ⟩ + ≡⟨ ≡-cong ( λ g → ( ( λ (x : Carrier a ) → g x ) )) ? ⟩ -- (extensionality (Sets ) {Carrier a} lemma11) ⟩ morph ( i + g ) ∎ where @@ -242,23 +244,24 @@ uniquness = λ {a b f g} → uniquness {a} {b} {f} {g} } } where - universalMapping : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → FMap U ( solution a b f ) o eta a ≡ f - universalMapping {a} {b} {f} = let open ≡-Reasoning in + universalMapping : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → ? -- FMap U ( solution a b f ) o eta a ≡ f + universalMapping {a} {b} {f} = begin FMap U ( solution a b f ) o eta a - ≡⟨⟩ + ≡⟨ refl ⟩ ( λ (x : a ) → Φ {a} {b} f (eta a x) ) - ≡⟨⟩ + ≡⟨ refl ⟩ ( λ (x : a ) → Φ {a} {b} f ( x :: [] ) ) - ≡⟨⟩ + ≡⟨ refl ⟩ ( λ (x : a ) → b < ( f x ) ∙ (Φ {a} {b} f [] ) > ) - ≡⟨⟩ + ≡⟨ refl ⟩ ( λ (x : a ) → b < ( f x ) ∙ ( ε b ) > ) ≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality A {a} lemma-ext1) ⟩ ( λ (x : a ) → f x ) - ≡⟨⟩ + ≡⟨ refl ⟩ f ∎ where + open ≡-Reasoning lemma-ext1 : ∀( x : a ) → b < ( f x ) ∙ ( ε b ) > ≡ f x lemma-ext1 x = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x) uniquness : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → diff -r 71049ed05151 -r 45de2b31bf02 src/freyd.agda --- a/src/freyd.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/freyd.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,15 +1,20 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Category -- https://github.com/konn/category-agda open import Level module freyd where -open import cat-utility +open import Definitions open import HomReasoning open import Relation.Binary.Core open Functor -- C is small full subcategory of A ( C is image of F ) -- but we don't use smallness in this proof +-- +-- Exisiting self functor is stronger than a subcategory. It may not exisit constructively. +-- but it makes the proof easier. record FullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where diff -r 71049ed05151 -r 45de2b31bf02 src/freyd1.agda --- a/src/freyd1.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/freyd1.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,10 +1,12 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Category -- https://github.com/konn/category-agda open import Level module freyd1 {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} ( F : Functor A C ) ( G : Functor A C ) where -open import cat-utility +open import Definitions open import HomReasoning open Functor diff -r 71049ed05151 -r 45de2b31bf02 src/freyd2.agda --- a/src/freyd2.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/freyd2.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Category -- https://github.com/konn/category-agda open import Level open import Category.Sets renaming ( _o_ to _*_ ) @@ -6,7 +8,7 @@ where open import HomReasoning -open import cat-utility +open import Definitions open import Relation.Binary.Core open import Function diff -r 71049ed05151 -r 45de2b31bf02 src/graph.agda --- a/src/graph.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/graph.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Category -- https://github.com/konn/category-agda open import Level @@ -197,7 +199,7 @@ identityR {a} {b} {f} = refl o-resp-≈ : {A B C : S } {f g : ( DiscreteHom {c₁} A B)} {h i : ( DiscreteHom B C)} → dom f ≡ dom g → dom h ≡ dom i → dom ( h * f ) ≡ dom ( i * g ) - o-resp-≈ {a} {b} {c} {f} {g} {h} {i} refl refl = refl + o-resp-≈ {a} {b} {c} {f} {g} {h} {i} eq _ = refl diff -r 71049ed05151 -r 45de2b31bf02 src/idF.agda --- a/src/idF.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/idF.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module idF where open import Category diff -r 71049ed05151 -r 45de2b31bf02 src/kleisli.agda --- a/src/kleisli.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/kleisli.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + -- -- -- -- -- -- -- -- -- Monad to Kelisli Category -- defines U_T and F_T as a resolution of Monad @@ -17,7 +19,7 @@ open import Level --open import Category.HomReasoning open import HomReasoning -open import cat-utility +open import Definitions open import Category.Cat module kleisli { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } diff -r 71049ed05151 -r 45de2b31bf02 src/limit-to.agda --- a/src/limit-to.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/limit-to.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,9 +1,11 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Category -- https://github.com/konn/category-agda open import Level module limit-to where -open import cat-utility +open import Definitions open import HomReasoning open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality hiding ([_]) diff -r 71049ed05151 -r 45de2b31bf02 src/maybeCat.agda --- a/src/maybeCat.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/maybeCat.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,20 +1,27 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Category -- https://github.com/konn/category-agda open import Level -module maybeCat where +module maybeCat { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where -open import cat-utility +open import Definitions open import HomReasoning open import Relation.Binary open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality hiding (sym) + open import Data.Maybe +open import Data.Empty open Functor -record MaybeHom { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A ) (b : Obj A ) : Set (ℓ ⊔ c₂) where - field - hom : Maybe ( Hom A a b ) +data MaybeHom { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) : (a b : Maybe (Obj A )) → Set (ℓ ⊔ c₂) where + hom : {a b : Obj A} → (f : Hom A a b ) → MaybeHom A (just a) (just b) + non-hom1 : {b : Obj A} → MaybeHom A (just b) nothing + non-hom2 : {b : Obj A} → MaybeHom A nothing (just b) + non-hom3 : {b : Obj A} → MaybeHom A nothing nothing open MaybeHom @@ -27,8 +34,11 @@ MaybeHomId : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } (a : Obj A ) → MaybeHom A a a MaybeHomId {_} {_} {_} {A} a = record { hom = just ( id1 A a) } -_[_≡≡_] : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } → Rel (Maybe (Hom A a b)) (c₂ ⊔ ℓ) -_[_≡≡_] A = Eq ( Category._≈_ A ) +_[_≡≡_] : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } → Rel (Maybe (Hom A a b)) ℓ +_[_≡≡_] A f g with f | g +... | nothing | _ = Lift _ ⊥ +... | _ | nothing = Lift _ ⊥ +... | just f | just g = A [ f ≈ g ] module ≡≡-Reasoning { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) where @@ -78,7 +88,7 @@ MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂) MaybeCat { c₁} {c₂} {ℓ} ( A ) = record { - Obj = Obj A ; + Obj = Maybe (Obj A) ; Hom = λ a b → MaybeHom A a b ; _o_ = _+_ ; _≈_ = λ a b → _[_≡≡_] { c₁} {c₂} {ℓ} A (hom a) (hom b) ; diff -r 71049ed05151 -r 45de2b31bf02 src/pullback.agda --- a/src/pullback.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/pullback.agda Sat Oct 07 19:43:31 2023 +0900 @@ -4,12 +4,13 @@ -- Shinji KONO ---- +{-# OPTIONS --cubical-compatible --safe #-} open import Category -- https://github.com/konn/category-agda open import Level module pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ') ( Γ : Functor I A ) where open import HomReasoning -open import cat-utility +open import Definitions -- -- Pullback from equalizer and product diff -r 71049ed05151 -r 45de2b31bf02 src/system-t.agda --- a/src/system-t.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/system-t.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,4 +1,7 @@ -module system-t where +{-# OPTIONS --cubical-compatible --safe #-} + +module system-t (U : Set) (V : Set) (v : V) (u : U) where + open import Relation.Binary.PropositionalEquality record _×_ ( U : Set ) ( V : Set ) : Set where @@ -11,11 +14,6 @@ open _×_ -postulate U : Set -postulate V : Set - -postulate v : V -postulate u : U f : U → V f = λ u → v diff -r 71049ed05151 -r 45de2b31bf02 src/universal-mapping.agda --- a/src/universal-mapping.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/universal-mapping.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --cubical-compatible --safe #-} module universal-mapping where -- Shinji KONO @@ -5,7 +6,7 @@ open import Category -- https://github.com/konn/category-agda open import Level open import HomReasoning -open import cat-utility +open import Definitions open import Category.Cat open Functor diff -r 71049ed05151 -r 45de2b31bf02 src/yoneda.agda --- a/src/yoneda.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/yoneda.agda Sat Oct 07 19:43:31 2023 +0900 @@ -5,11 +5,12 @@ -- Nat(h_a,F) -- Shinji KONO ---- +-- {-# OPTIONS --cubical-compatible #-} -open import Category -- https://github.com/konn/category-agda open import Level -open import Category.Sets -open import cat-utility +open import Category.Sets hiding (_==_) +open import Category +open import Definitions module yoneda { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (I : Set c₁) ( small : Small A I ) where open import HomReasoning @@ -30,11 +31,11 @@ ; _≈_ = _==_ ; Id = Yid ; isCategory = record { - isEquivalence = record {refl = refl ; trans = λ {i} {j} {k} → trans1 {_} {_} {i} {j} {k} ; sym = λ {i j} → sym1 {_} {_} {i} {j}} - ; identityL = refl - ; identityR = refl + isEquivalence = record {refl = ? ; trans = λ {i} {j} {k} → trans1 {_} {_} {i} {j} {k} ; sym = λ {i j} → sym1 {_} {_} {i} {j}} + ; identityL = ? + ; identityR = ? ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} - ; associative = refl + ; associative = ? } } where open ≈-Reasoning (Sets {c₂}) YObj : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) @@ -45,7 +46,7 @@ Yid : {a : YObj } → YHom a a Yid {a} = record { TMap = λ a → λ x → x ; isNTrans = isNTrans1 {a} } where isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (λ a → λ x → x ) - isNTrans1 {a} = record { commute = refl } + isNTrans1 {a} = record { commute = ? } _+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c _+_ {a} {b} {c} f g = @@ -94,6 +95,9 @@ -- ---- +import Axiom.Extensionality.Propositional +postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ + y-tmap : ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → FObj (y-obj a) x → FObj (y-obj b ) x y-tmap a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b ) @@ -103,9 +107,9 @@ lemma-y-obj4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) → Sets [ Sets [ FMap (y-obj b) g o y-tmap a b f a₁ ] ≈ Sets [ y-tmap a b f b₁ o FMap (y-obj a) g ] ] - lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin - A [ A [ f o x ] o g ] ≈↑⟨ assoc ⟩ - A [ f o A [ x o g ] ] ∎ ) ) + lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = ? -- let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin + -- A [ A [ f o x ] o g ] ≈↑⟨ assoc ⟩ + -- A [ f o A [ x o g ] ] ∎ ) ) isNTrans1 : {a b : Obj A } → (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) (y-obj b) (y-tmap a b f ) isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f } @@ -125,20 +129,20 @@ ; ≈-cong = ≈-cong } } where ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-map f ≈ y-map g ] - ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning A in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] ) - extensionality A ( λ h → ≈-≡ A ( begin - A [ f o h ] ≈⟨ resp refl-hom eq ⟩ - A [ g o h ] ∎ ) ) + ≈-cong {a} {b} {f} {g} eq = ? -- let open ≈-Reasoning A in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] ) + -- extensionality A ( λ h → ≈-≡ A ( begin + -- A [ f o h ] ≈⟨ resp refl-hom eq ⟩ + -- A [ g o h ] ∎ ) ) identity : {a : Obj A} → SetsAop [ y-map (id1 A a) ≈ id1 SetsAop (y-obj a ) ] - identity {a} = let open ≈-Reasoning A in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x) - extensionality A ( λ g → ≈-≡ A ( begin - A [ id1 A a o g ] ≈⟨ idL ⟩ - g ∎ ) ) + identity {a} = ? -- let open ≈-Reasoning A in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x) + -- extensionality A ( λ g → ≈-≡ A ( begin + -- A [ id1 A a o g ] ≈⟨ idL ⟩ + -- g ∎ ) ) distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-map (A [ g o f ]) ≈ SetsAop [ y-map g o y-map f ] ] - distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning A in -- (λ x g₁ → (A [ (A [ g o f] o g₁ ]))) ≡ (λ x x₁ → A [ g o A [ f o x₁ ] ] ) - extensionality A ( λ h → ≈-≡ A ( begin - A [ A [ g o f ] o h ] ≈↑⟨ assoc ⟩ - A [ g o A [ f o h ] ] ∎ ) ) + distr1 {a} {b} {c} {f} {g} = ? -- let open ≈-Reasoning A in -- (λ x g₁ → (A [ (A [ g o f] o g₁ ]))) ≡ (λ x x₁ → A [ g o A [ f o x₁ ] ] ) + -- extensionality A ( λ h → ≈-≡ A ( begin + -- A [ A [ g o f ] o h ] ≈↑⟨ assoc ⟩ + -- A [ g o A [ f o h ] ] ∎ ) ) ------ -- @@ -184,7 +188,7 @@ commute1 : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} (g : Hom A a₁ a) → (Sets [ FMap F f o FMap F g ]) x ≡ FMap F (A [ g o f ] ) x commute1 g = let open ≈-Reasoning (Sets) in - cong ( λ f → f x ) ( sym ( distr F ) ) + cong ( λ f → f x ) ? -- ( sym ( distr F ) ) commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} → Sets [ Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap {a} {F} {x} b o FMap (y-obj a) f ] ] commute {a₁} {b} {f} = let open ≈-Reasoning (Sets) in @@ -192,7 +196,7 @@ Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈⟨⟩ Sets [ FMap F f o (λ ( g : Hom A a₁ a ) → ( FMap F g ) x) ] - ≈⟨ extensionality A ( λ (g : Hom A a₁ a) → commute1 {a₁} {b} {f} g ) ⟩ + ≈⟨ ? ⟩ -- extensionality A ( λ (g : Hom A a₁ a) → commute1 {a₁} {b} {f} g ) ⟩ Sets [ (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap (y-obj a) f ] ≈⟨⟩ Sets [ F2Natmap {a} {F} {x} b o FMap (y-obj a) f ] @@ -216,13 +220,13 @@ F2Nat→Nat2F : {a : Obj A } → {F : Obj SetsAop } → (fa : FObj F a) → Nat2F {a} {F} (F2Nat {a} {F} fa) ≡ fa -F2Nat→Nat2F {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) ( +F2Nat→Nat2F {a} {F} fa = ? -- let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) ( -- FMap F (Category.Category.Id A) fa ≡ fa - begin - ( FMap F (id1 A _ )) - ≈⟨ IsFunctor.identity (isFunctor F) ⟩ - id1 Sets (FObj F a) - ∎ ) + -- begin + -- ( FMap F (id1 A _ )) + -- ≈⟨ IsFunctor.identity (isFunctor F) ⟩ + -- id1 Sets (FObj F a) + -- ∎ ) ≡-cong = Relation.Binary.PropositionalEquality.cong @@ -230,16 +234,16 @@ -- FMap F g o TMap ha a ≈ TMap ha b o FMap (y-obj {a}) g Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop } → (ha : Hom SetsAop (y-obj a) F) → SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ] -Nat2F→F2Nat {a} {F} ha {b} = let open ≡-Reasoning in begin - TMap (F2Nat {a} {F} (Nat2F {a} {F} ha)) b ≡⟨⟩ - (λ g → FMap F g (TMap ha a (id1 A _))) ≡⟨ extensionality A (λ g → ( begin - FMap F g (TMap ha a (id1 A _)) ≡⟨ ≡-cong (λ f → f (id1 A _)) (IsNTrans.commute (isNTrans ha)) ⟩ - TMap ha b (FMap (y-obj a) g (id1 A _)) ≡⟨⟩ - TMap ha b ( A [ id1 A _ o g ] ) ≡⟨ ≡-cong ( TMap ha b ) ( ≈-≡ A (≈-Reasoning.idL A)) ⟩ - TMap ha b g ∎ )) ⟩ - TMap ha b - ∎ - +Nat2F→F2Nat {a} {F} ha {b} = ? -- let open ≡-Reasoning in begin +-- TMap (F2Nat {a} {F} (Nat2F {a} {F} ha)) b ≡⟨⟩ +-- (λ g → FMap F g (TMap ha a (id1 A _))) ≡⟨ extensionality A (λ g → ( begin +-- FMap F g (TMap ha a (id1 A _)) ≡⟨ ≡-cong (λ f → f (id1 A _)) (IsNTrans.commute (isNTrans ha)) ⟩ +-- TMap ha b (FMap (y-obj a) g (id1 A _)) ≡⟨⟩ +-- TMap ha b ( A [ id1 A _ o g ] ) ≡⟨ ≡-cong ( TMap ha b ) ( ≈-≡ A (≈-Reasoning.idL A)) ⟩ +-- TMap ha b g ∎ )) ⟩ +-- TMap ha b +-- ∎ +-- -- Yoneda's Lemma -- Yoneda Functor is full and faithfull -- that is FMapp Yoneda is injective and surjective @@ -247,7 +251,7 @@ -- λ b g → (A Category.o f₁) g YonedaLemma1 : {a a' : Obj A } {f : FObj (FObj YonedaFunctor a) a' } → SetsAop [ F2Nat {a'} {FObj YonedaFunctor a} f ≈ FMap YonedaFunctor f ] -YonedaLemma1 {a} {a'} {f} = refl +YonedaLemma1 {a} {a'} {f} = ? -- refl YonedaIso0 : {a a' : Obj A } {f : FObj (FObj YonedaFunctor a) a' } → Nat2F ( FMap YonedaFunctor f ) ≡ f @@ -293,7 +297,7 @@ TMap (FMap YonedaFunctor f) b g ∎ ) where open ≡-Reasoning f-u : {a a' b : Obj A } (f : FObj (FObj YonedaFunctor a') a ) → Sets [ f ^ ≈ TMap (FMap YonedaFunctor f ) b ] -f-u = f-unique +f-u = ? -- f-unique -- faithful (injective ) Yoneda-injective : {a b b' : Obj A } → {x y : Obj SetsAop} → (g h : Hom A b b' ) (f : Hom A a b ) @@ -306,7 +310,7 @@ h ∎ where ylem11 : SetsAop [ FMap YonedaFunctor g ≈ FMap YonedaFunctor h ] → A [ Nat2F (FMap YonedaFunctor g) ≈ Nat2F (FMap YonedaFunctor h) ] ylem11 yg=yh with yg=yh {b} - ... | eq = ≈-Reasoning.≈←≡ A ( cong (λ k → k (id1 A b)) eq ) + ... | eq = ≈-Reasoning.≈←≡ A ( cong (λ k → k (id1 A b)) ? ) open ≈-Reasoning A -- full (surjective)