From 1c6d9ad2b5a65d6c2922c48c71d9ecbddb9fbf4c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 3 Apr 2018 11:36:09 +0200 Subject: [PATCH] Rename identity in category to ascii-name --- src/Cat/Categories/Cat.agda | 42 ++++---- src/Cat/Categories/Cube.agda | 2 +- src/Cat/Categories/Fam.agda | 12 +-- src/Cat/Categories/Free.agda | 10 +- src/Cat/Categories/Fun.agda | 109 ++++++++++++-------- src/Cat/Categories/Rel.agda | 2 +- src/Cat/Categories/Sets.agda | 8 +- src/Cat/Category.agda | 72 ++++++------- src/Cat/Category/Exponential.agda | 4 +- src/Cat/Category/Functor.agda | 10 +- src/Cat/Category/Monad.agda | 34 +++--- src/Cat/Category/Monad/Kleisli.agda | 80 +++++++------- src/Cat/Category/Monad/Monoidal.agda | 10 +- src/Cat/Category/NaturalTransformation.agda | 8 +- src/Cat/Category/Product.agda | 14 +-- src/Cat/Category/Yoneda.agda | 2 +- 16 files changed, 221 insertions(+), 198 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 3021268..a5d986e 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -15,10 +15,10 @@ open import Cat.Categories.Fun -- The category of categories module _ (ℓ ℓ' : Level) where RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') - RawCategory.Object RawCat = Category ℓ ℓ' - RawCategory.Arrow RawCat = Functor - RawCategory.𝟙 RawCat = Functors.identity - RawCategory._∘_ RawCat = F[_∘_] + RawCategory.Object RawCat = Category ℓ ℓ' + RawCategory.Arrow RawCat = Functor + RawCategory.identity RawCat = Functors.identity + RawCategory._∘_ RawCat = F[_∘_] -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors, -- however, form a groupoid! Therefore there is no (1-)category of @@ -48,8 +48,8 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where Obj = ℂ.Object × 𝔻.Object Arr : Obj → Obj → Set ℓ' Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ] - 𝟙 : {o : Obj} → Arr o o - 𝟙 = ℂ.𝟙 , 𝔻.𝟙 + identity : {o : Obj} → Arr o o + identity = ℂ.identity , 𝔻.identity _∘_ : {a b c : Obj} → Arr b c → @@ -58,16 +58,16 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where _∘_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]} rawProduct : RawCategory ℓ ℓ' - RawCategory.Object rawProduct = Obj - RawCategory.Arrow rawProduct = Arr - RawCategory.𝟙 rawProduct = 𝟙 - RawCategory._∘_ rawProduct = _∘_ + RawCategory.Object rawProduct = Obj + RawCategory.Arrow rawProduct = Arr + RawCategory.identity rawProduct = identity + RawCategory._∘_ rawProduct = _∘_ open RawCategory rawProduct arrowsAreSets : ArrowsAreSets arrowsAreSets = setSig {sA = ℂ.arrowsAreSets} {sB = λ x → 𝔻.arrowsAreSets} - isIdentity : IsIdentity 𝟙 + isIdentity : IsIdentity identity isIdentity = Σ≡ (fst ℂ.isIdentity) (fst 𝔻.isIdentity) , Σ≡ (snd ℂ.isIdentity) (snd 𝔻.isIdentity) @@ -202,14 +202,14 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where module _ {c : Functor ℂ 𝔻 × ℂ.Object} where open Σ c renaming (proj₁ to F ; proj₂ to C) - ident : fmap {c} {c} (identityNT F , ℂ.𝟙 {A = snd c}) ≡ 𝔻.𝟙 + ident : fmap {c} {c} (identityNT F , ℂ.identity {A = snd c}) ≡ 𝔻.identity ident = begin - fmap {c} {c} (Category.𝟙 (object ⊗ ℂ) {c}) ≡⟨⟩ - fmap {c} {c} (idN F , ℂ.𝟙) ≡⟨⟩ - 𝔻 [ identityTrans F C ∘ F.fmap ℂ.𝟙 ] ≡⟨⟩ - 𝔻 [ 𝔻.𝟙 ∘ F.fmap ℂ.𝟙 ] ≡⟨ 𝔻.leftIdentity ⟩ - F.fmap ℂ.𝟙 ≡⟨ F.isIdentity ⟩ - 𝔻.𝟙 ∎ + fmap {c} {c} (Category.identity (object ⊗ ℂ) {c}) ≡⟨⟩ + fmap {c} {c} (idN F , ℂ.identity) ≡⟨⟩ + 𝔻 [ identityTrans F C ∘ F.fmap ℂ.identity ] ≡⟨⟩ + 𝔻 [ 𝔻.identity ∘ F.fmap ℂ.identity ] ≡⟨ 𝔻.leftIdentity ⟩ + F.fmap ℂ.identity ≡⟨ F.isIdentity ⟩ + 𝔻.identity ∎ where module F = Functor F @@ -278,16 +278,16 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where transpose : Functor 𝔸 object eq : F[ eval ∘ (parallelProduct transpose (Functors.identity {ℂ = ℂ})) ] ≡ F -- eq : F[ :eval: ∘ {!!} ] ≡ F - -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F + -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (identity Catℓ {o = ℂ})) ] ≡ F -- eq' : (Catℓ [ :eval: ∘ -- (record { product = product } HasProducts.|×| transpose) - -- (𝟙 Catℓ) + -- (identity Catℓ) -- ]) -- ≡ F -- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758` -- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [ - -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose = + -- :eval: ∘ (parallelProduct F~ (identity Catℓ {o = ℂ}))] ≡ F) catTranspose = -- transpose , eq -- We don't care about filling out the holes below since they are anyways hidden diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda index f338343..5322b16 100644 --- a/src/Cat/Categories/Cube.agda +++ b/src/Cat/Categories/Cube.agda @@ -67,7 +67,7 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo) Raw.Object Rawℂ = FiniteDecidableSubset Raw.Arrow Rawℂ = Hom - Raw.𝟙 Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} } + Raw.identity Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} } Raw._∘_ Rawℂ = {!!} postulate IsCategoryℂ : IsCategory Rawℂ diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda index 5ffde56..ff4fafc 100644 --- a/src/Cat/Categories/Fam.agda +++ b/src/Cat/Categories/Fam.agda @@ -11,9 +11,9 @@ module _ (ℓa ℓb : Level) where Object = Σ[ hA ∈ hSet ℓa ] (proj₁ hA → hSet ℓb) Arr : Object → Object → Set (ℓa ⊔ ℓb) Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → proj₁ (B x) → proj₁ (B' (f x))) - 𝟙 : {A : Object} → Arr A A - proj₁ 𝟙 = λ x → x - proj₂ 𝟙 = λ b → b + identity : {A : Object} → Arr A A + proj₁ identity = λ x → x + proj₂ identity = λ b → b _∘_ : {a b c : Object} → Arr b c → Arr a b → Arr a c (g , g') ∘ (f , f') = g Function.∘ f , g' Function.∘ f' @@ -21,16 +21,16 @@ module _ (ℓa ℓb : Level) where RawFam = record { Object = Object ; Arrow = Arr - ; 𝟙 = λ { {A} → 𝟙 {A = A}} + ; identity = λ { {A} → identity {A = A}} ; _∘_ = λ {a b c} → _∘_ {a} {b} {c} } - open RawCategory RawFam hiding (Object ; 𝟙) + open RawCategory RawFam hiding (Object ; identity) isAssociative : IsAssociative isAssociative = Σ≡ refl refl - isIdentity : IsIdentity λ { {A} → 𝟙 {A} } + isIdentity : IsIdentity λ { {A} → identity {A} } isIdentity = (Σ≡ refl refl) , Σ≡ refl refl open import Cubical.NType.Properties diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index 1d262dd..29d6bbe 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -27,10 +27,10 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where module ℂ = Category ℂ RawFree : RawCategory ℓa (ℓa ⊔ ℓb) - RawCategory.Object RawFree = ℂ.Object - RawCategory.Arrow RawFree = Path ℂ.Arrow - RawCategory.𝟙 RawFree = empty - RawCategory._∘_ RawFree = concatenate + RawCategory.Object RawFree = ℂ.Object + RawCategory.Arrow RawFree = Path ℂ.Arrow + RawCategory.identity RawFree = empty + RawCategory._∘_ RawFree = concatenate open RawCategory RawFree @@ -52,7 +52,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ident-l : ∀ {A} {B} {p : Path ℂ.Arrow A B} → concatenate empty p ≡ p ident-l = refl - isIdentity : IsIdentity 𝟙 + isIdentity : IsIdentity identity isIdentity = ident-l , ident-r open Univalence isIdentity diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 791ddc6..1cd2e0a 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -1,28 +1,28 @@ -{-# OPTIONS --allow-unsolved-metas --cubical #-} +{-# OPTIONS --allow-unsolved-metas --cubical --caching #-} module Cat.Categories.Fun where open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor +import Cat.Category.NaturalTransformation + as NaturalTransformation module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where - import Cat.Category.NaturalTransformation ℂ 𝔻 - as NaturalTransformation - open NaturalTransformation public hiding (module Properties) - open NaturalTransformation.Properties + open NaturalTransformation ℂ 𝔻 public hiding (module Properties) + open NaturalTransformation.Properties ℂ 𝔻 private module ℂ = Category ℂ module 𝔻 = Category 𝔻 -- Functor categories. Objects are functors, arrows are natural transformations. raw : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd') - RawCategory.Object raw = Functor ℂ 𝔻 - RawCategory.Arrow raw = NaturalTransformation - RawCategory.𝟙 raw {F} = identity F - RawCategory._∘_ raw {F} {G} {H} = NT[_∘_] {F} {G} {H} + RawCategory.Object raw = Functor ℂ 𝔻 + RawCategory.Arrow raw = NaturalTransformation + RawCategory.identity raw {F} = identity F + RawCategory._∘_ raw {F} {G} {H} = NT[_∘_] {F} {G} {H} - open RawCategory raw + open RawCategory raw hiding (identity) open Univalence (λ {A} {B} {f} → isIdentity {F = A} {B} {f}) module _ (F : Functor ℂ 𝔻) where @@ -32,7 +32,7 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C open Σ center renaming (proj₂ to isoF) module _ (cG : Σ[ G ∈ Object ] (F ≅ G)) where - open Σ cG renaming (proj₁ to G ; proj₂ to isoG) + open Σ cG renaming (proj₁ to G ; proj₂ to isoG) module G = Functor G open Σ isoG renaming (proj₁ to θNT ; proj₂ to invθNT) open Σ invθNT renaming (proj₁ to ηNT ; proj₂ to areInv) @@ -46,10 +46,10 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C -- g = T[ η ∘ θ ] {!!} ntF : NaturalTransformation F F - ntF = 𝟙 {A = F} + ntF = identity F ntG : NaturalTransformation G G - ntG = 𝟙 {A = G} + ntG = identity G idFunctor = Functors.identity @@ -103,14 +103,14 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C -- The transformation will be the identity on 𝔻. Such an arrow has the -- type `A.omap A → A.omap A`. Which we can coerce to have the type -- `A.omap → B.omap` since `A` and `B` are equal. - coe𝟙 : Transformation A B - coe𝟙 X = coe coerceAB 𝔻.𝟙 + coeidentity : Transformation A B + coeidentity X = coe coerceAB 𝔻.identity module _ {a b : ℂ.Object} (f : ℂ [ a , b ]) where - nat' : 𝔻 [ coe𝟙 b ∘ A.fmap f ] ≡ 𝔻 [ B.fmap f ∘ coe𝟙 a ] + nat' : 𝔻 [ coeidentity b ∘ A.fmap f ] ≡ 𝔻 [ B.fmap f ∘ coeidentity a ] nat' = begin - (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡⟨ {!!} ⟩ - (𝔻 [ B.fmap f ∘ coe𝟙 a ]) ∎ + (𝔻 [ coeidentity b ∘ A.fmap f ]) ≡⟨ {!!} ⟩ + (𝔻 [ B.fmap f ∘ coeidentity a ]) ∎ transs : (i : I) → Transformation A (p i) transs = {!!} @@ -118,26 +118,26 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C natt : (i : I) → Natural A (p i) {!!} natt = {!!} - t : Natural A B coe𝟙 + t : Natural A B coeidentity t = coe c (identityNatural A) where - c : Natural A A (identityTrans A) ≡ Natural A B coe𝟙 + c : Natural A A (identityTrans A) ≡ Natural A B coeidentity c = begin Natural A A (identityTrans A) ≡⟨ (λ x → {!natt ?!}) ⟩ - Natural A B coe𝟙 ∎ + Natural A B coeidentity ∎ -- cong (λ φ → {!Natural A A (identityTrans A)!}) {!!} - k : Natural A A (identityTrans A) → Natural A B coe𝟙 + k : Natural A A (identityTrans A) → Natural A B coeidentity k n {a} {b} f = res where - res : (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡ (𝔻 [ B.fmap f ∘ coe𝟙 a ]) + res : (𝔻 [ coeidentity b ∘ A.fmap f ]) ≡ (𝔻 [ B.fmap f ∘ coeidentity a ]) res = {!!} - nat : Natural A B coe𝟙 + nat : Natural A B coeidentity nat = nat' fromEq : NaturalTransformation A B - fromEq = coe𝟙 , nat + fromEq = coeidentity , nat module _ {A B : Functor ℂ 𝔻} where obverse : A ≡ B → A ≅ B @@ -147,9 +147,9 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C ob = fromEq p re : Arrow B A re = fromEq (sym p) - vr : _∘_ {A = A} {B} {A} re ob ≡ 𝟙 {A} + vr : _∘_ {A = A} {B} {A} re ob ≡ identity A vr = {!!} - rv : _∘_ {A = B} {A} {B} ob re ≡ 𝟙 {B} + rv : _∘_ {A = B} {A} {B} ob re ≡ identity B rv = {!!} isInverse : IsInverseOf {A} {B} ob re isInverse = vr , rv @@ -183,23 +183,42 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C Category.raw Fun = raw Category.isCategory Fun = isCategory --- module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where --- private --- open import Cat.Categories.Sets --- open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ') +module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where + private + open import Cat.Categories.Sets + open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ') + module K = Fun (opposite ℂ) (𝓢𝓮𝓽 ℓ') + module F = Category K.Fun --- -- Restrict the functors to Presheafs. --- rawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ') --- rawPresh = record --- { Object = Presheaf ℂ --- ; Arrow = NaturalTransformation --- ; 𝟙 = λ {F} → identity F --- ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H} --- } --- instance --- isCategory : IsCategory rawPresh --- isCategory = Fun.isCategory _ _ + -- Restrict the functors to Presheafs. + raw : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ') + raw = record + { Object = Presheaf ℂ + ; Arrow = NaturalTransformation + ; identity = λ {F} → identity F + ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H} + } --- Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ') --- Category.raw Presh = rawPresh --- Category.isCategory Presh = isCategory + isCategory : IsCategory raw + isCategory = record + { isAssociative = + λ{ {A} {B} {C} {D} {f} {g} {h} + → F.isAssociative {A} {B} {C} {D} {f} {g} {h} + } + ; isIdentity = + λ{ {A} {B} {f} + → F.isIdentity {A} {B} {f} + } + ; arrowsAreSets = + λ{ {A} {B} + → F.arrowsAreSets {A} {B} + } + ; univalent = + λ{ {A} {B} + → F.univalent {A} {B} + } + } + + Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ') + Category.raw Presh = raw + Category.isCategory Presh = isCategory diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index 5b44601..73d4bff 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -153,7 +153,7 @@ RawRel : RawCategory (lsuc lzero) (lsuc lzero) RawRel = record { Object = Set ; Arrow = λ S R → Subset (S × R) - ; 𝟙 = λ {S} → Diag S + ; identity = λ {S} → Diag S ; _∘_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )} } diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index f4c59fd..8536870 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -60,10 +60,10 @@ module _ {ℓ : Level} {A B : Set ℓ} {a : A} where module _ (ℓ : Level) where private SetsRaw : RawCategory (lsuc ℓ) ℓ - RawCategory.Object SetsRaw = hSet ℓ - RawCategory.Arrow SetsRaw (T , _) (U , _) = T → U - RawCategory.𝟙 SetsRaw = Function.id - RawCategory._∘_ SetsRaw = Function._∘′_ + RawCategory.Object SetsRaw = hSet ℓ + RawCategory.Arrow SetsRaw (T , _) (U , _) = T → U + RawCategory.identity SetsRaw = Function.id + RawCategory._∘_ SetsRaw = Function._∘′_ open RawCategory SetsRaw hiding (_∘_) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 8408cf0..2576ee2 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -12,7 +12,7 @@ -- -- Data -- ---- --- 𝟙; the identity arrow +-- identity; the identity arrow -- _∘_; function composition -- -- Laws @@ -48,10 +48,10 @@ import Function record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where no-eta-equality field - Object : Set ℓa - Arrow : Object → Object → Set ℓb - 𝟙 : {A : Object} → Arrow A A - _∘_ : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C + Object : Set ℓa + Arrow : Object → Object → Set ℓb + identity : {A : Object} → Arrow A A + _∘_ : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C infixl 10 _∘_ _>>>_ @@ -82,7 +82,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B) IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb - IsInverseOf = λ f g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙 + IsInverseOf = λ f g → g ∘ f ≡ identity × f ∘ g ≡ identity Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g @@ -110,10 +110,10 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where Terminal = Σ Object IsTerminal -- | Univalence is indexed by a raw category as well as an identity proof. - module Univalence (isIdentity : IsIdentity 𝟙) where + module Univalence (isIdentity : IsIdentity identity) where -- | The identity isomorphism idIso : (A : Object) → A ≅ A - idIso A = 𝟙 , 𝟙 , isIdentity + idIso A = identity , identity , isIdentity -- | Extract an isomorphism from an equality -- @@ -150,16 +150,16 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc open RawCategory ℂ public field isAssociative : IsAssociative - isIdentity : IsIdentity 𝟙 + isIdentity : IsIdentity identity arrowsAreSets : ArrowsAreSets open Univalence isIdentity public field univalent : Univalent - leftIdentity : {A B : Object} {f : Arrow A B} → 𝟙 ∘ f ≡ f + leftIdentity : {A B : Object} {f : Arrow A B} → identity ∘ f ≡ f leftIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f}) - rightIdentity : {A B : Object} {f : Arrow A B} → f ∘ 𝟙 ≡ f + rightIdentity : {A B : Object} {f : Arrow A B} → f ∘ identity ≡ f rightIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f}) ------------ @@ -171,24 +171,24 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc iso→epi : Isomorphism f → Epimorphism {X = X} f iso→epi (f- , left-inv , right-inv) g₀ g₁ eq = begin g₀ ≡⟨ sym rightIdentity ⟩ - g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩ + g₀ ∘ identity ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩ g₀ ∘ (f ∘ f-) ≡⟨ isAssociative ⟩ (g₀ ∘ f) ∘ f- ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩ (g₁ ∘ f) ∘ f- ≡⟨ sym isAssociative ⟩ g₁ ∘ (f ∘ f-) ≡⟨ cong (_∘_ g₁) right-inv ⟩ - g₁ ∘ 𝟙 ≡⟨ rightIdentity ⟩ + g₁ ∘ identity ≡⟨ rightIdentity ⟩ g₁ ∎ iso→mono : Isomorphism f → Monomorphism {X = X} f iso→mono (f- , left-inv , right-inv) g₀ g₁ eq = begin g₀ ≡⟨ sym leftIdentity ⟩ - 𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩ + identity ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩ (f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩ f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩ f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩ (f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩ - 𝟙 ∘ g₁ ≡⟨ leftIdentity ⟩ + identity ∘ g₁ ≡⟨ leftIdentity ⟩ g₁ ∎ iso→epi×mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f @@ -228,12 +228,12 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc where geq : g ≡ g' geq = begin - g ≡⟨ sym rightIdentity ⟩ - g ∘ 𝟙 ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩ - g ∘ (f ∘ g') ≡⟨ isAssociative ⟩ - (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩ - 𝟙 ∘ g' ≡⟨ leftIdentity ⟩ - g' ∎ + g ≡⟨ sym rightIdentity ⟩ + g ∘ identity ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩ + g ∘ (f ∘ g') ≡⟨ isAssociative ⟩ + (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩ + identity ∘ g' ≡⟨ leftIdentity ⟩ + g' ∎ propUnivalent : isProp Univalent propUnivalent a b i = propPi (λ iso → propIsContr) a b i @@ -274,9 +274,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc Xprop f g = trans (sym (snd Xit f)) (snd Xit g) Yprop : isProp (Arrow Y Y) Yprop f g = trans (sym (snd Yit f)) (snd Yit g) - left : Y→X ∘ X→Y ≡ 𝟙 + left : Y→X ∘ X→Y ≡ identity left = Xprop _ _ - right : X→Y ∘ Y→X ≡ 𝟙 + right : X→Y ∘ Y→X ≡ identity right = Yprop _ _ iso : X ≅ Y iso = X→Y , Y→X , left , right @@ -321,9 +321,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc Xprop f g = trans (sym (snd Xii f)) (snd Xii g) Yprop : isProp (Arrow Y Y) Yprop f g = trans (sym (snd Yii f)) (snd Yii g) - left : Y→X ∘ X→Y ≡ 𝟙 + left : Y→X ∘ X→Y ≡ identity left = Yprop _ _ - right : X→Y ∘ Y→X ≡ 𝟙 + right : X→Y ∘ Y→X ≡ identity right = Xprop _ _ iso : X ≅ Y iso = Y→X , X→Y , right , left @@ -351,18 +351,18 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where -- adverse effects this may have. module Prop = X.Propositionality - isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ] + isIdentity : (λ _ → IsIdentity identity) [ X.isIdentity ≡ Y.isIdentity ] isIdentity = Prop.propIsIdentity X.isIdentity Y.isIdentity - U : ∀ {a : IsIdentity 𝟙} - → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ] + U : ∀ {a : IsIdentity identity} + → (λ _ → IsIdentity identity) [ X.isIdentity ≡ a ] → (b : Univalent a) → Set _ U eqwal univ = (λ i → Univalent (eqwal i)) [ X.univalent ≡ univ ] - P : (y : IsIdentity 𝟙) - → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ y ] → Set _ + P : (y : IsIdentity identity) + → (λ _ → IsIdentity identity) [ X.isIdentity ≡ y ] → Set _ P y eq = ∀ (univ : Univalent y) → U eq univ p : ∀ (b' : Univalent X.isIdentity) → (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ] @@ -426,14 +426,14 @@ module Opposite {ℓa ℓb : Level} where private module ℂ = Category ℂ opRaw : RawCategory ℓa ℓb - RawCategory.Object opRaw = ℂ.Object - RawCategory.Arrow opRaw = Function.flip ℂ.Arrow - RawCategory.𝟙 opRaw = ℂ.𝟙 - RawCategory._∘_ opRaw = Function.flip ℂ._∘_ + RawCategory.Object opRaw = ℂ.Object + RawCategory.Arrow opRaw = Function.flip ℂ.Arrow + RawCategory.identity opRaw = ℂ.identity + RawCategory._∘_ opRaw = Function.flip ℂ._∘_ open RawCategory opRaw - isIdentity : IsIdentity 𝟙 + isIdentity : IsIdentity identity isIdentity = swap ℂ.isIdentity open Univalence isIdentity @@ -530,7 +530,7 @@ module Opposite {ℓa ℓb : Level} where rawInv : Category.raw (opposite (opposite ℂ)) ≡ raw RawCategory.Object (rawInv _) = Object RawCategory.Arrow (rawInv _) = Arrow - RawCategory.𝟙 (rawInv _) = 𝟙 + RawCategory.identity (rawInv _) = identity RawCategory._∘_ (rawInv _) = _∘_ oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ diff --git a/src/Cat/Category/Exponential.agda b/src/Cat/Category/Exponential.agda index 76652d2..4b4f017 100644 --- a/src/Cat/Category/Exponential.agda +++ b/src/Cat/Category/Exponential.agda @@ -16,11 +16,11 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} field uniq : ∀ (A : Object) (f : ℂ [ A × B , C ]) - → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f) + → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.identity ℂ ] ≡ f) IsExponential : (Cᴮ : Object) → ℂ [ Cᴮ × B , C ] → Set (ℓ ⊔ ℓ') IsExponential Cᴮ eval = ∀ (A : Object) (f : ℂ [ A × B , C ]) - → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f) + → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.identity ℂ ] ≡ f) record Exponential : Set (ℓ ⊔ ℓ') where field diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index bbdda14..c4a7346 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -30,7 +30,7 @@ module _ {ℓc ℓc' ℓd ℓd'} fmap : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ omap A , omap B ] IsIdentity : Set _ - IsIdentity = {A : ℂ.Object} → fmap (ℂ.𝟙 {A}) ≡ 𝔻.𝟙 {omap A} + IsIdentity = {A : ℂ.Object} → fmap (ℂ.identity {A}) ≡ 𝔻.identity {omap A} IsDistributive : Set _ IsDistributive = {A B C : ℂ.Object} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} @@ -150,10 +150,10 @@ module _ {ℓ0 ℓ1 ℓ2 ℓ3 ℓ4 ℓ5 : Level} isFunctor : IsFunctor A C raw isFunctor = record { isIdentity = begin - (F.fmap ∘ G.fmap) A.𝟙 ≡⟨ refl ⟩ - F.fmap (G.fmap A.𝟙) ≡⟨ cong F.fmap (G.isIdentity)⟩ - F.fmap B.𝟙 ≡⟨ F.isIdentity ⟩ - C.𝟙 ∎ + (F.fmap ∘ G.fmap) A.identity ≡⟨ refl ⟩ + F.fmap (G.fmap A.identity) ≡⟨ cong F.fmap (G.isIdentity)⟩ + F.fmap B.identity ≡⟨ F.isIdentity ⟩ + C.identity ∎ ; isDistributive = dist } diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 8fc6c56..6383ab0 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -33,10 +33,10 @@ module Kleisli = Cat.Category.Monad.Kleisli -- | The monoidal- and kleisli presentation of monads are equivalent. module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where - open Cat.Category.NaturalTransformation ℂ ℂ + open Cat.Category.NaturalTransformation ℂ ℂ using (NaturalTransformation ; propIsNatural) private module ℂ = Category ℂ - open ℂ using (Object ; Arrow ; 𝟙 ; _∘_ ; _>>>_) + open ℂ using (Object ; Arrow ; identity ; _∘_ ; _>>>_) module M = Monoidal ℂ module K = Kleisli ℂ @@ -84,11 +84,11 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where inv-l = begin joinT X ∘ pureT (R.omap X) ≡⟨⟩ join ∘ pure ≡⟨ proj₁ isInverse ⟩ - 𝟙 ∎ + identity ∎ inv-r = begin joinT X ∘ R.fmap (pureT X) ≡⟨⟩ join ∘ fmap pure ≡⟨ proj₂ isInverse ⟩ - 𝟙 ∎ + identity ∎ back : K.Monad → M.Monad Monoidal.Monad.raw (back m) = backRaw m @@ -103,21 +103,21 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where bindEq {X} {Y} = begin K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩ (λ f → join ∘ fmap f) ≡⟨⟩ - (λ f → bind (f >>> pure) >>> bind 𝟙) ≡⟨ funExt lem ⟩ + (λ f → bind (f >>> pure) >>> bind identity) ≡⟨ funExt lem ⟩ (λ f → bind f) ≡⟨⟩ bind ∎ where lem : (f : Arrow X (omap Y)) - → bind (f >>> pure) >>> bind 𝟙 + → bind (f >>> pure) >>> bind identity ≡ bind f lem f = begin - bind (f >>> pure) >>> bind 𝟙 + bind (f >>> pure) >>> bind identity ≡⟨ isDistributive _ _ ⟩ - bind ((f >>> pure) >>> bind 𝟙) + bind ((f >>> pure) >>> bind identity) ≡⟨ cong bind ℂ.isAssociative ⟩ - bind (f >>> (pure >>> bind 𝟙)) + bind (f >>> (pure >>> bind identity)) ≡⟨ cong (λ φ → bind (f >>> φ)) (isNatural _) ⟩ - bind (f >>> 𝟙) + bind (f >>> identity) ≡⟨ cong bind ℂ.leftIdentity ⟩ bind f ∎ @@ -146,10 +146,10 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where joinEq : ∀ {X} → KM.join ≡ joinT X joinEq {X} = begin KM.join ≡⟨⟩ - KM.bind 𝟙 ≡⟨⟩ - bind 𝟙 ≡⟨⟩ - joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → _ ∘ φ) R.isIdentity ⟩ - joinT X ∘ 𝟙 ≡⟨ ℂ.rightIdentity ⟩ + KM.bind identity ≡⟨⟩ + bind identity ≡⟨⟩ + joinT X ∘ Rfmap identity ≡⟨ cong (λ φ → _ ∘ φ) R.isIdentity ⟩ + joinT X ∘ identity ≡⟨ ℂ.rightIdentity ⟩ joinT X ∎ fmapEq : ∀ {A B} → KM.fmap {A} {B} ≡ Rfmap @@ -161,7 +161,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where Rfmap (f >>> pureT B) >>> joinT B ≡⟨ cong (λ φ → φ >>> joinT B) R.isDistributive ⟩ Rfmap f >>> Rfmap (pureT B) >>> joinT B ≡⟨ ℂ.isAssociative ⟩ joinT B ∘ Rfmap (pureT B) ∘ Rfmap f ≡⟨ cong (λ φ → φ ∘ Rfmap f) (proj₂ isInverse) ⟩ - 𝟙 ∘ Rfmap f ≡⟨ ℂ.leftIdentity ⟩ + identity ∘ Rfmap f ≡⟨ ℂ.leftIdentity ⟩ Rfmap f ∎ ) @@ -183,8 +183,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where joinTEq = funExt (λ X → begin M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩ KM.join ≡⟨⟩ - joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩ - joinT X ∘ 𝟙 ≡⟨ ℂ.rightIdentity ⟩ + joinT X ∘ Rfmap identity ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩ + joinT X ∘ identity ≡⟨ ℂ.rightIdentity ⟩ joinT X ∎) joinNTEq : (λ i → NaturalTransformation F[ Req i ∘ Req i ] (Req i)) diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda index bf79a5f..dc40f1c 100644 --- a/src/Cat/Category/Monad/Kleisli.agda +++ b/src/Cat/Category/Monad/Kleisli.agda @@ -12,11 +12,13 @@ open import Cat.Categories.Fun -- "A monad in the Kleisli form" [voe] module Cat.Category.Monad.Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where -open import Cat.Category.NaturalTransformation ℂ ℂ hiding (propIsNatural) +open import Cat.Category.NaturalTransformation ℂ ℂ + using (NaturalTransformation ; Transformation ; Natural) + private ℓ = ℓa ⊔ ℓb module ℂ = Category ℂ - open ℂ using (Arrow ; 𝟙 ; Object ; _∘_ ; _>>>_) + open ℂ using (Arrow ; identity ; Object ; _∘_ ; _>>>_) -- | Data for a monad. -- @@ -40,7 +42,7 @@ record RawMonad : Set ℓ where -- | Flattening nested monads. join : {A : Object} → ℂ [ omap (omap A) , omap A ] - join = bind 𝟙 + join = bind identity ------------------ -- * Monad laws -- @@ -49,7 +51,7 @@ record RawMonad : Set ℓ where -- There may be better names than what I've chosen here. IsIdentity = {X : Object} - → bind pure ≡ 𝟙 {omap X} + → bind pure ≡ identity {omap X} IsNatural = {X Y : Object} (f : ℂ [ X , omap Y ]) → pure >>> (bind f) ≡ f IsDistributive = {X Y Z : Object} (g : ℂ [ Y , omap Z ]) (f : ℂ [ X , omap Y ]) @@ -67,7 +69,7 @@ record RawMonad : Set ℓ where IsNaturalForeign = {X : Object} → join {X} ∘ fmap join ≡ join ∘ join IsInverse : Set _ - IsInverse = {X : Object} → join {X} ∘ pure ≡ 𝟙 × join {X} ∘ fmap pure ≡ 𝟙 + IsInverse = {X : Object} → join {X} ∘ pure ≡ identity × join {X} ∘ fmap pure ≡ identity record IsMonad (raw : RawMonad) : Set ℓ where open RawMonad raw public @@ -100,9 +102,9 @@ record IsMonad (raw : RawMonad) : Set ℓ where isFunctorR : IsFunctor ℂ ℂ rawR IsFunctor.isIdentity isFunctorR = begin - bind (pure ∘ 𝟙) ≡⟨ cong bind (ℂ.rightIdentity) ⟩ - bind pure ≡⟨ isIdentity ⟩ - 𝟙 ∎ + bind (pure ∘ identity) ≡⟨ cong bind (ℂ.rightIdentity) ⟩ + bind pure ≡⟨ isIdentity ⟩ + identity ∎ IsFunctor.isDistributive isFunctorR {f = f} {g} = begin bind (pure ∘ (g ∘ f)) ≡⟨⟩ @@ -137,29 +139,29 @@ record IsMonad (raw : RawMonad) : Set ℓ where joinN : Natural R² R joinT joinN f = begin join ∘ R².fmap f ≡⟨⟩ - bind 𝟙 ∘ R².fmap f ≡⟨⟩ - R².fmap f >>> bind 𝟙 ≡⟨⟩ - fmap (fmap f) >>> bind 𝟙 ≡⟨⟩ - fmap (bind (f >>> pure)) >>> bind 𝟙 ≡⟨⟩ - bind (bind (f >>> pure) >>> pure) >>> bind 𝟙 + bind identity ∘ R².fmap f ≡⟨⟩ + R².fmap f >>> bind identity ≡⟨⟩ + fmap (fmap f) >>> bind identity ≡⟨⟩ + fmap (bind (f >>> pure)) >>> bind identity ≡⟨⟩ + bind (bind (f >>> pure) >>> pure) >>> bind identity ≡⟨ isDistributive _ _ ⟩ - bind ((bind (f >>> pure) >>> pure) >=> 𝟙) + bind ((bind (f >>> pure) >>> pure) >=> identity) ≡⟨⟩ - bind ((bind (f >>> pure) >>> pure) >>> bind 𝟙) + bind ((bind (f >>> pure) >>> pure) >>> bind identity) ≡⟨ cong bind ℂ.isAssociative ⟩ - bind (bind (f >>> pure) >>> (pure >>> bind 𝟙)) + bind (bind (f >>> pure) >>> (pure >>> bind identity)) ≡⟨ cong (λ φ → bind (bind (f >>> pure) >>> φ)) (isNatural _) ⟩ - bind (bind (f >>> pure) >>> 𝟙) + bind (bind (f >>> pure) >>> identity) ≡⟨ cong bind ℂ.leftIdentity ⟩ bind (bind (f >>> pure)) ≡⟨ cong bind (sym ℂ.rightIdentity) ⟩ - bind (𝟙 >>> bind (f >>> pure)) ≡⟨⟩ - bind (𝟙 >=> (f >>> pure)) + bind (identity >>> bind (f >>> pure)) ≡⟨⟩ + bind (identity >=> (f >>> pure)) ≡⟨ sym (isDistributive _ _) ⟩ - bind 𝟙 >>> bind (f >>> pure) ≡⟨⟩ - bind 𝟙 >>> fmap f ≡⟨⟩ - bind 𝟙 >>> R.fmap f ≡⟨⟩ - R.fmap f ∘ bind 𝟙 ≡⟨⟩ + bind identity >>> bind (f >>> pure) ≡⟨⟩ + bind identity >>> fmap f ≡⟨⟩ + bind identity >>> R.fmap f ≡⟨⟩ + R.fmap f ∘ bind identity ≡⟨⟩ R.fmap f ∘ join ∎ pureNT : NaturalTransformation R⁰ R @@ -173,20 +175,20 @@ record IsMonad (raw : RawMonad) : Set ℓ where isNaturalForeign : IsNaturalForeign isNaturalForeign = begin fmap join >>> join ≡⟨⟩ - bind (join >>> pure) >>> bind 𝟙 + bind (join >>> pure) >>> bind identity ≡⟨ isDistributive _ _ ⟩ - bind ((join >>> pure) >>> bind 𝟙) + bind ((join >>> pure) >>> bind identity) ≡⟨ cong bind ℂ.isAssociative ⟩ - bind (join >>> (pure >>> bind 𝟙)) + bind (join >>> (pure >>> bind identity)) ≡⟨ cong (λ φ → bind (join >>> φ)) (isNatural _) ⟩ - bind (join >>> 𝟙) + bind (join >>> identity) ≡⟨ cong bind ℂ.leftIdentity ⟩ bind join ≡⟨⟩ - bind (bind 𝟙) + bind (bind identity) ≡⟨ cong bind (sym ℂ.rightIdentity) ⟩ - bind (𝟙 >>> bind 𝟙) ≡⟨⟩ - bind (𝟙 >=> 𝟙) ≡⟨ sym (isDistributive _ _) ⟩ - bind 𝟙 >>> bind 𝟙 ≡⟨⟩ + bind (identity >>> bind identity) ≡⟨⟩ + bind (identity >=> identity) ≡⟨ sym (isDistributive _ _) ⟩ + bind identity >>> bind identity ≡⟨⟩ join >>> join ∎ isInverse : IsInverse @@ -194,21 +196,21 @@ record IsMonad (raw : RawMonad) : Set ℓ where where inv-l = begin pure >>> join ≡⟨⟩ - pure >>> bind 𝟙 ≡⟨ isNatural _ ⟩ - 𝟙 ∎ + pure >>> bind identity ≡⟨ isNatural _ ⟩ + identity ∎ inv-r = begin fmap pure >>> join ≡⟨⟩ - bind (pure >>> pure) >>> bind 𝟙 + bind (pure >>> pure) >>> bind identity ≡⟨ isDistributive _ _ ⟩ - bind ((pure >>> pure) >=> 𝟙) ≡⟨⟩ - bind ((pure >>> pure) >>> bind 𝟙) + bind ((pure >>> pure) >=> identity) ≡⟨⟩ + bind ((pure >>> pure) >>> bind identity) ≡⟨ cong bind ℂ.isAssociative ⟩ - bind (pure >>> (pure >>> bind 𝟙)) + bind (pure >>> (pure >>> bind identity)) ≡⟨ cong (λ φ → bind (pure >>> φ)) (isNatural _) ⟩ - bind (pure >>> 𝟙) + bind (pure >>> identity) ≡⟨ cong bind ℂ.leftIdentity ⟩ bind pure ≡⟨ isIdentity ⟩ - 𝟙 ∎ + identity ∎ record Monad : Set ℓ where field diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda index 69f3865..56319c2 100644 --- a/src/Cat/Category/Monad/Monoidal.agda +++ b/src/Cat/Category/Monad/Monoidal.agda @@ -16,8 +16,10 @@ module Cat.Category.Monad.Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb private ℓ = ℓa ⊔ ℓb -open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_) +open Category ℂ using (Object ; Arrow ; identity ; _∘_) open import Cat.Category.NaturalTransformation ℂ ℂ + using (NaturalTransformation ; Transformation ; Natural) + record RawMonad : Set ℓ where field R : EndoFunctor ℂ @@ -47,8 +49,8 @@ record RawMonad : Set ℓ where → joinT X ∘ Rfmap (joinT X) ≡ joinT X ∘ joinT (Romap X) IsInverse : Set _ IsInverse = {X : Object} - → joinT X ∘ pureT (Romap X) ≡ 𝟙 - × joinT X ∘ Rfmap (pureT X) ≡ 𝟙 + → joinT X ∘ pureT (Romap X) ≡ identity + × joinT X ∘ Rfmap (pureT X) ≡ identity IsNatural = ∀ {X Y} f → joinT Y ∘ Rfmap f ∘ pureT X ≡ f IsDistributive = ∀ {X Y Z} (g : Arrow Y (Romap Z)) (f : Arrow X (Romap Y)) → joinT Z ∘ Rfmap g ∘ (joinT Y ∘ Rfmap f) @@ -70,7 +72,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where joinT Y ∘ (R.fmap f ∘ pureT X) ≡⟨ cong (λ φ → joinT Y ∘ φ) (sym (pureN f)) ⟩ joinT Y ∘ (pureT (R.omap Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩ joinT Y ∘ pureT (R.omap Y) ∘ f ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩ - 𝟙 ∘ f ≡⟨ ℂ.leftIdentity ⟩ + identity ∘ f ≡⟨ ℂ.leftIdentity ⟩ f ∎ isDistributive : IsDistributive diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda index a478aee..0b4d784 100644 --- a/src/Cat/Category/NaturalTransformation.agda +++ b/src/Cat/Category/NaturalTransformation.agda @@ -31,7 +31,7 @@ module Cat.Category.NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where -open Category using (Object ; 𝟙) +open Category using (Object) private module ℂ = Category ℂ module 𝔻 = Category 𝔻 @@ -63,14 +63,14 @@ module _ (F G : Functor ℂ 𝔻) where NaturalTransformation≡ eq = lemSig propIsNatural _ _ eq identityTrans : (F : Functor ℂ 𝔻) → Transformation F F -identityTrans F C = 𝟙 𝔻 +identityTrans F C = 𝔻.identity identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F) identityNatural F {A = A} {B = B} f = begin 𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩ - 𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ 𝔻.leftIdentity ⟩ + 𝔻 [ 𝔻.identity ∘ F→ f ] ≡⟨ 𝔻.leftIdentity ⟩ F→ f ≡⟨ sym 𝔻.rightIdentity ⟩ - 𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩ + 𝔻 [ F→ f ∘ 𝔻.identity ] ≡⟨⟩ 𝔻 [ F→ f ∘ identityTrans F A ] ∎ where module F = Functor F diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index 03f6c4a..e956377 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -134,7 +134,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} ( ℂ [ ya ∘ xy ] ≡ xa) × ℂ [ yb ∘ xy ] ≡ xb } - ; 𝟙 = λ{ {A , f , g} → ℂ.𝟙 {A} , ℂ.rightIdentity , ℂ.rightIdentity} + ; identity = λ{ {A , f , g} → ℂ.identity {A} , ℂ.rightIdentity , ℂ.rightIdentity} ; _∘_ = λ { {A , a0 , a1} {B , b0 , b1} {C , c0 , c1} (f , f0 , f1) (g , g0 , g1) → (f ℂ.∘ g) , (begin @@ -169,24 +169,24 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} s0 = ℂ.isAssociative {f = f} {g} {h} - isIdentity : IsIdentity 𝟙 + isIdentity : IsIdentity identity isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity where - leftIdentity : 𝟙 ∘ (f , f0 , f1) ≡ (f , f0 , f1) + leftIdentity : identity ∘ (f , f0 , f1) ≡ (f , f0 , f1) leftIdentity i = l i , lemPropF propEqs l {proj₂ L} {proj₂ R} i where - L = 𝟙 ∘ (f , f0 , f1) + L = identity ∘ (f , f0 , f1) R : Arrow AA BB R = f , f0 , f1 l : proj₁ L ≡ proj₁ R l = ℂ.leftIdentity - rightIdentity : (f , f0 , f1) ∘ 𝟙 ≡ (f , f0 , f1) + rightIdentity : (f , f0 , f1) ∘ identity ≡ (f , f0 , f1) rightIdentity i = l i , lemPropF propEqs l {proj₂ L} {proj₂ R} i where - L = (f , f0 , f1) ∘ 𝟙 + L = (f , f0 , f1) ∘ identity R : Arrow AA BB R = (f , f0 , f1) - l : ℂ [ f ∘ ℂ.𝟙 ] ≡ f + l : ℂ [ f ∘ ℂ.identity ] ≡ f l = ℂ.rightIdentity arrowsAreSets : ArrowsAreSets diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index 1efc90e..afea823 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -52,7 +52,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where isIdentity : IsIdentity isIdentity {c} = lemSig prp _ _ eq where - eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (presheaf c) + eq : (λ C x → ℂ [ ℂ.identity ∘ x ]) ≡ identityTrans (presheaf c) eq = funExt λ A → funExt λ B → ℂ.leftIdentity prp = F.naturalIsProp _ _ {F = presheaf c} {presheaf c}