From 4beb48e066b813166d2ab31c3c4da60e72940488 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 21 Mar 2018 11:46:36 +0100 Subject: [PATCH] Use correct order for left- and right identity Define and use helpers left- and right identity --- src/Cat/Categories/Cat.agda | 8 ++-- src/Cat/Categories/Free.agda | 2 +- src/Cat/Categories/Fun.agda | 10 ++--- src/Cat/Categories/Rel.agda | 8 ++-- src/Cat/Categories/Sets.agda | 44 ++++++++++----------- src/Cat/Category.agda | 24 +++++++---- src/Cat/Category/Monad.agda | 8 ++-- src/Cat/Category/Monad/Kleisli.agda | 12 +++--- src/Cat/Category/Monad/Monoidal.agda | 4 +- src/Cat/Category/NaturalTransformation.agda | 4 +- src/Cat/Category/Yoneda.agda | 2 +- 11 files changed, 65 insertions(+), 61 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index f429985..9038605 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -47,7 +47,7 @@ module _ (β„“ β„“' : Level) where isAssociative : IsAssociative isAssociative {f = F} {G} {H} = assc {F = F} {G = G} {H = H} ident : IsIdentity identity - ident = ident-r , ident-l + ident = ident-l , ident-r -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors, -- however, form a groupoid! Therefore there is no (1-)category of @@ -241,10 +241,10 @@ module CatExponential {β„“ : Level} (β„‚ 𝔻 : Category β„“ β„“) where ident : fmap {c} {c} (NT.identity F , πŸ™ β„‚ {A = projβ‚‚ c}) ≑ πŸ™ 𝔻 ident = begin - fmap {c} {c} (πŸ™ (object βŠ— β„‚) {c}) β‰‘βŸ¨βŸ© - fmap {c} {c} (idN F , πŸ™ β„‚) β‰‘βŸ¨βŸ© + fmap {c} {c} (πŸ™ (object βŠ— β„‚) {c}) β‰‘βŸ¨βŸ© + fmap {c} {c} (idN F , πŸ™ β„‚) β‰‘βŸ¨βŸ© 𝔻 [ identityTrans F C ∘ F.fmap (πŸ™ β„‚)] β‰‘βŸ¨βŸ© - 𝔻 [ πŸ™ 𝔻 ∘ F.fmap (πŸ™ β„‚)] β‰‘βŸ¨ projβ‚‚ 𝔻.isIdentity ⟩ + 𝔻 [ πŸ™ 𝔻 ∘ F.fmap (πŸ™ β„‚)] β‰‘βŸ¨ 𝔻.leftIdentity ⟩ F.fmap (πŸ™ β„‚) β‰‘βŸ¨ F.isIdentity ⟩ πŸ™ 𝔻 ∎ where diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index 9d8d3d4..bda3820 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -55,7 +55,7 @@ module _ {β„“a β„“b : Level} (β„‚ : Category β„“a β„“b) where ident-l = refl isIdentity : IsIdentity πŸ™ - isIdentity = ident-r , ident-l + isIdentity = ident-l , ident-r open Univalence isIdentity diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 9bbb438..14bbdd2 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -45,18 +45,18 @@ module Fun {β„“c β„“c' β„“d β„“d' : Level} (β„‚ : Category β„“c β„“c') (𝔻 : C eq-r : βˆ€ C β†’ (𝔻 [ f' C ∘ identityTrans A C ]) ≑ f' C eq-r C = begin 𝔻 [ f' C ∘ identityTrans A C ] β‰‘βŸ¨βŸ© - 𝔻 [ f' C ∘ 𝔻.πŸ™ ] β‰‘βŸ¨ proj₁ 𝔻.isIdentity ⟩ + 𝔻 [ f' C ∘ 𝔻.πŸ™ ] β‰‘βŸ¨ 𝔻.rightIdentity ⟩ f' C ∎ eq-l : βˆ€ C β†’ (𝔻 [ identityTrans B C ∘ f' C ]) ≑ f' C - eq-l C = projβ‚‚ 𝔻.isIdentity + eq-l C = 𝔻.leftIdentity ident-r : (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≑ f ident-r = lemSig allNatural _ _ (funExt eq-r) ident-l : (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≑ f ident-l = lemSig allNatural _ _ (funExt eq-l) isIdentity - : (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≑ f - Γ— (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≑ f - isIdentity = ident-r , ident-l + : (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≑ f + Γ— (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≑ f + isIdentity = ident-l , ident-r -- Functor categories. Objects are functors, arrows are natural transformations. RawFun : RawCategory (β„“c βŠ” β„“c' βŠ” β„“d βŠ” β„“d') (β„“c βŠ” β„“c' βŠ” β„“d') RawFun = record diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index 1dbed3d..ac645ef 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -76,9 +76,9 @@ module _ {A B : Set} {S : Subset (A Γ— B)} (ab : A Γ— B) where ≃ (a , b) ∈ S equi = backwards Cubical.FromStdLib., isequiv - ident-l : (Ξ£[ a' ∈ A ] (a , a') ∈ Diag A Γ— (a' , b) ∈ S) + ident-r : (Ξ£[ a' ∈ A ] (a , a') ∈ Diag A Γ— (a' , b) ∈ S) ≑ (a , b) ∈ S - ident-l = equivToPath equi + ident-r = equivToPath equi module _ where private @@ -110,9 +110,9 @@ module _ {A B : Set} {S : Subset (A Γ— B)} (ab : A Γ— B) where ≃ ab ∈ S equi = backwards Cubical.FromStdLib., isequiv - ident-r : (Ξ£[ b' ∈ B ] (a , b') ∈ S Γ— (b' , b) ∈ Diag B) + ident-l : (Ξ£[ b' ∈ B ] (a , b') ∈ S Γ— (b' , b) ∈ Diag B) ≑ ab ∈ S - ident-r = equivToPath equi + ident-l = equivToPath equi module _ {A B C D : Set} {S : Subset (A Γ— B)} {R : Subset (B Γ— C)} {Q : Subset (C Γ— D)} (ad : A Γ— D) where private diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index f5af047..ce94104 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -287,39 +287,35 @@ module _ {β„“ : Level} where open Category 𝓒 open import Cubical.Sigma - module _ (0A 0B : Object) where + module _ (hA hB : Object) where + open Ξ£ hA renaming (proj₁ to A ; projβ‚‚ to sA) + open Ξ£ hB renaming (proj₁ to B ; projβ‚‚ to sB) + private - A : Set β„“ - A = proj₁ 0A - sA : isSet A - sA = projβ‚‚ 0A - B : Set β„“ - B = proj₁ 0B - sB : isSet B - sB = projβ‚‚ 0B - 0AΓ—0B : Object - 0AΓ—0B = (A Γ— B) , sigPresSet sA Ξ» _ β†’ sB + productObject : Object + productObject = (A Γ— B) , sigPresSet sA Ξ» _ β†’ sB module _ {X A B : Set β„“} (f : X β†’ A) (g : X β†’ B) where _&&&_ : (X β†’ A Γ— B) _&&&_ x = f x , g x - module _ {0X : Object} where - X = proj₁ 0X - module _ (f : X β†’ A ) (g : X β†’ B) where - lem : proj₁ Function.βˆ˜β€² (f &&& g) ≑ f Γ— projβ‚‚ Function.βˆ˜β€² (f &&& g) ≑ g - proj₁ lem = refl - projβ‚‚ lem = refl - rawProduct : RawProduct 𝓒 0A 0B - RawProduct.object rawProduct = 0AΓ—0B + module _ (hX : Object) where + open Ξ£ hX renaming (proj₁ to X) + module _ (f : X β†’ A ) (g : X β†’ B) where + ump : proj₁ Function.βˆ˜β€² (f &&& g) ≑ f Γ— projβ‚‚ Function.βˆ˜β€² (f &&& g) ≑ g + proj₁ ump = refl + projβ‚‚ ump = refl + + rawProduct : RawProduct 𝓒 hA hB + RawProduct.object rawProduct = productObject RawProduct.proj₁ rawProduct = Data.Product.proj₁ RawProduct.projβ‚‚ rawProduct = Data.Product.projβ‚‚ isProduct : IsProduct 𝓒 _ _ rawProduct - IsProduct.ump isProduct {X = X} f g - = (f &&& g) , lem {0X = X} f g + IsProduct.ump isProduct {X = hX} f g + = (f &&& g) , ump hX f g - product : Product 𝓒 0A 0B + product : Product 𝓒 hA hB Product.raw product = rawProduct Product.isProduct product = isProduct @@ -346,7 +342,7 @@ module _ {β„“a β„“b : Level} (β„‚ : Category β„“a β„“b) where ; fmap = β„‚ [_∘_] } ; isFunctor = record - { isIdentity = funExt Ξ» _ β†’ projβ‚‚ isIdentity + { isIdentity = funExt Ξ» _ β†’ leftIdentity ; isDistributive = funExt Ξ» x β†’ sym isAssociative } } @@ -359,7 +355,7 @@ module _ {β„“a β„“b : Level} (β„‚ : Category β„“a β„“b) where ; fmap = Ξ» f g β†’ β„‚ [ g ∘ f ] } ; isFunctor = record - { isIdentity = funExt Ξ» x β†’ proj₁ isIdentity + { isIdentity = funExt Ξ» x β†’ rightIdentity ; isDistributive = funExt Ξ» x β†’ isAssociative } } diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 834ff47..370da37 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -96,7 +96,7 @@ record RawCategory (β„“a β„“b : Level) : Set (lsuc (β„“a βŠ” β„“b)) where IsIdentity : ({A : Object} β†’ Arrow A A) β†’ Set (β„“a βŠ” β„“b) IsIdentity id = {A B : Object} {f : Arrow A B} - β†’ f ∘ id ≑ f Γ— id ∘ f ≑ f + β†’ id ∘ f ≑ f Γ— f ∘ id ≑ f ArrowsAreSets : Set (β„“a βŠ” β„“b) ArrowsAreSets = βˆ€ {A B : Object} β†’ isSet (Arrow A B) @@ -166,29 +166,37 @@ record IsCategory {β„“a β„“b : Level} (β„‚ : RawCategory β„“a β„“b) : Set (lsuc field univalent : Univalent + leftIdentity : {A B : Object} {f : Arrow A B} β†’ πŸ™ ∘ f ≑ f + leftIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f}) + -- leftIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f}) + + rightIdentity : {A B : Object} {f : Arrow A B} β†’ f ∘ πŸ™ ≑ f + rightIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f}) + -- rightIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f}) + -- Some common lemmas about categories. module _ {A B : Object} {X : Object} (f : Arrow A B) where iso-is-epi : Isomorphism f β†’ Epimorphism {X = X} f iso-is-epi (f- , left-inv , right-inv) gβ‚€ g₁ eq = begin - gβ‚€ β‰‘βŸ¨ sym (fst isIdentity) ⟩ + gβ‚€ β‰‘βŸ¨ sym rightIdentity ⟩ gβ‚€ ∘ πŸ™ β‰‘βŸ¨ 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₁ ∘ πŸ™ β‰‘βŸ¨ fst isIdentity ⟩ + g₁ ∘ πŸ™ β‰‘βŸ¨ rightIdentity ⟩ g₁ ∎ iso-is-mono : Isomorphism f β†’ Monomorphism {X = X} f iso-is-mono (f- , (left-inv , right-inv)) gβ‚€ g₁ eq = begin - gβ‚€ β‰‘βŸ¨ sym (snd isIdentity) ⟩ + gβ‚€ β‰‘βŸ¨ sym leftIdentity ⟩ πŸ™ ∘ 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₁ β‰‘βŸ¨ snd isIdentity ⟩ + πŸ™ ∘ g₁ β‰‘βŸ¨ leftIdentity ⟩ g₁ ∎ iso-is-epi-mono : Isomorphism f β†’ Epimorphism {X = X} f Γ— Monomorphism {X = X} f @@ -201,7 +209,7 @@ record IsCategory {β„“a β„“b : Level} (β„‚ : RawCategory β„“a β„“b) : Set (lsuc module Propositionality {β„“a β„“b : Level} (β„‚ : RawCategory β„“a β„“b) where open RawCategory β„‚ module _ (β„‚ : IsCategory β„‚) where - open IsCategory β„‚ using (isAssociative ; arrowsAreSets ; isIdentity ; Univalent) + open IsCategory β„‚ using (isAssociative ; arrowsAreSets ; Univalent ; leftIdentity ; rightIdentity) open import Cubical.NType open import Cubical.NType.Properties @@ -233,11 +241,11 @@ module Propositionality {β„“a β„“b : Level} (β„‚ : RawCategory β„“a β„“b) where open Cubical.NType.Properties geq : g ≑ g' geq = begin - g β‰‘βŸ¨ sym (fst isIdentity) ⟩ + g β‰‘βŸ¨ sym rightIdentity ⟩ g ∘ πŸ™ β‰‘βŸ¨ cong (Ξ» Ο† β†’ g ∘ Ο†) (sym Ξ΅') ⟩ g ∘ (f ∘ g') β‰‘βŸ¨ isAssociative ⟩ (g ∘ f) ∘ g' β‰‘βŸ¨ cong (Ξ» Ο† β†’ Ο† ∘ g') Ξ· ⟩ - πŸ™ ∘ g' β‰‘βŸ¨ snd isIdentity ⟩ + πŸ™ ∘ g' β‰‘βŸ¨ leftIdentity ⟩ g' ∎ propUnivalent : isProp Univalent diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 3eef523..f6cb1a9 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -124,7 +124,7 @@ module _ {β„“a β„“b : Level} (β„‚ : Category β„“a β„“b) where bind (f >>> (pure >>> bind πŸ™)) β‰‘βŸ¨ cong (Ξ» Ο† β†’ bind (f >>> Ο†)) (isNatural _) ⟩ bind (f >>> πŸ™) - β‰‘βŸ¨ cong bind (projβ‚‚ β„‚.isIdentity) ⟩ + β‰‘βŸ¨ cong bind β„‚.leftIdentity ⟩ bind f ∎ forthRawEq : forthRaw (backRaw m) ≑ K.Monad.raw m @@ -155,7 +155,7 @@ module _ {β„“a β„“b : Level} (β„‚ : Category β„“a β„“b) where KM.bind πŸ™ β‰‘βŸ¨βŸ© bind πŸ™ β‰‘βŸ¨βŸ© joinT X ∘ Rfmap πŸ™ β‰‘βŸ¨ cong (Ξ» Ο† β†’ _ ∘ Ο†) R.isIdentity ⟩ - joinT X ∘ πŸ™ β‰‘βŸ¨ proj₁ β„‚.isIdentity ⟩ + joinT X ∘ πŸ™ β‰‘βŸ¨ β„‚.rightIdentity ⟩ joinT X ∎ fmapEq : βˆ€ {A B} β†’ KM.fmap {A} {B} ≑ Rfmap @@ -167,7 +167,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 β‰‘βŸ¨ projβ‚‚ β„‚.isIdentity ⟩ + πŸ™ ∘ Rfmap f β‰‘βŸ¨ β„‚.leftIdentity ⟩ Rfmap f ∎ ) @@ -192,7 +192,7 @@ module _ {β„“a β„“b : Level} (β„‚ : Category β„“a β„“b) where M.RawMonad.joinT (backRaw (forth m)) X β‰‘βŸ¨βŸ© KM.join β‰‘βŸ¨βŸ© joinT X ∘ Rfmap πŸ™ β‰‘βŸ¨ cong (Ξ» Ο† β†’ joinT X ∘ Ο†) R.isIdentity ⟩ - joinT X ∘ πŸ™ β‰‘βŸ¨ proj₁ β„‚.isIdentity ⟩ + joinT X ∘ πŸ™ β‰‘βŸ¨ β„‚.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 8f96b82..eedbeb7 100644 --- a/src/Cat/Category/Monad/Kleisli.agda +++ b/src/Cat/Category/Monad/Kleisli.agda @@ -104,7 +104,7 @@ record IsMonad (raw : RawMonad) : Set β„“ where isFunctorR : IsFunctor β„‚ β„‚ rawR IsFunctor.isIdentity isFunctorR = begin - bind (pure ∘ πŸ™) β‰‘βŸ¨ cong bind (proj₁ β„‚.isIdentity) ⟩ + bind (pure ∘ πŸ™) β‰‘βŸ¨ cong bind (β„‚.rightIdentity) ⟩ bind pure β‰‘βŸ¨ isIdentity ⟩ πŸ™ ∎ @@ -156,9 +156,9 @@ record IsMonad (raw : RawMonad) : Set β„“ where bind (bind (f >>> pure) >>> (pure >>> bind πŸ™)) β‰‘βŸ¨ cong (Ξ» Ο† β†’ bind (bind (f >>> pure) >>> Ο†)) (isNatural _) ⟩ bind (bind (f >>> pure) >>> πŸ™) - β‰‘βŸ¨ cong bind (projβ‚‚ β„‚.isIdentity) ⟩ + β‰‘βŸ¨ cong bind β„‚.leftIdentity ⟩ bind (bind (f >>> pure)) - β‰‘βŸ¨ cong bind (sym (proj₁ β„‚.isIdentity)) ⟩ + β‰‘βŸ¨ cong bind (sym β„‚.rightIdentity) ⟩ bind (πŸ™ >>> bind (f >>> pure)) β‰‘βŸ¨βŸ© bind (πŸ™ >=> (f >>> pure)) β‰‘βŸ¨ sym (isDistributive _ _) ⟩ @@ -186,10 +186,10 @@ record IsMonad (raw : RawMonad) : Set β„“ where bind (join >>> (pure >>> bind πŸ™)) β‰‘βŸ¨ cong (Ξ» Ο† β†’ bind (join >>> Ο†)) (isNatural _) ⟩ bind (join >>> πŸ™) - β‰‘βŸ¨ cong bind (projβ‚‚ β„‚.isIdentity) ⟩ + β‰‘βŸ¨ cong bind β„‚.leftIdentity ⟩ bind join β‰‘βŸ¨βŸ© bind (bind πŸ™) - β‰‘βŸ¨ cong bind (sym (proj₁ β„‚.isIdentity)) ⟩ + β‰‘βŸ¨ cong bind (sym β„‚.rightIdentity) ⟩ bind (πŸ™ >>> bind πŸ™) β‰‘βŸ¨βŸ© bind (πŸ™ >=> πŸ™) β‰‘βŸ¨ sym (isDistributive _ _) ⟩ bind πŸ™ >>> bind πŸ™ β‰‘βŸ¨βŸ© @@ -212,7 +212,7 @@ record IsMonad (raw : RawMonad) : Set β„“ where bind (pure >>> (pure >>> bind πŸ™)) β‰‘βŸ¨ cong (Ξ» Ο† β†’ bind (pure >>> Ο†)) (isNatural _) ⟩ bind (pure >>> πŸ™) - β‰‘βŸ¨ cong bind (projβ‚‚ β„‚.isIdentity) ⟩ + β‰‘βŸ¨ cong bind β„‚.leftIdentity ⟩ bind pure β‰‘βŸ¨ isIdentity ⟩ πŸ™ ∎ diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda index b969187..52cfc5e 100644 --- a/src/Cat/Category/Monad/Monoidal.agda +++ b/src/Cat/Category/Monad/Monoidal.agda @@ -75,8 +75,8 @@ 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 β‰‘βŸ¨ projβ‚‚ β„‚.isIdentity ⟩ - f ∎ + πŸ™ ∘ f β‰‘βŸ¨ β„‚.leftIdentity ⟩ + f ∎ isDistributive : IsDistributive isDistributive {X} {Y} {Z} g f = sym aux diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda index 2ccef94..82ef983 100644 --- a/src/Cat/Category/NaturalTransformation.agda +++ b/src/Cat/Category/NaturalTransformation.agda @@ -72,8 +72,8 @@ module NaturalTransformation {β„“c β„“c' β„“d β„“d' : Level} identityNatural : (F : Functor β„‚ 𝔻) β†’ Natural F F (identityTrans F) identityNatural F {A = A} {B = B} f = begin 𝔻 [ identityTrans F B ∘ Fβ†’ f ] β‰‘βŸ¨βŸ© - 𝔻 [ πŸ™ 𝔻 ∘ Fβ†’ f ] β‰‘βŸ¨ projβ‚‚ 𝔻.isIdentity ⟩ - Fβ†’ f β‰‘βŸ¨ sym (proj₁ 𝔻.isIdentity) ⟩ + 𝔻 [ πŸ™ 𝔻 ∘ Fβ†’ f ] β‰‘βŸ¨ 𝔻.leftIdentity ⟩ + Fβ†’ f β‰‘βŸ¨ sym 𝔻.rightIdentity ⟩ 𝔻 [ Fβ†’ f ∘ πŸ™ 𝔻 ] β‰‘βŸ¨βŸ© 𝔻 [ Fβ†’ f ∘ identityTrans F A ] ∎ where diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index 9447023..7a1a0bc 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -54,7 +54,7 @@ module _ {β„“ : Level} {β„‚ : Category β„“ β„“} where isIdentity {c} = lemSig (naturalIsProp {F = presheaf c} {presheaf c}) _ _ eq where eq : (Ξ» C x β†’ β„‚ [ β„‚.πŸ™ ∘ x ]) ≑ identityTrans (presheaf c) - eq = funExt Ξ» A β†’ funExt Ξ» B β†’ projβ‚‚ β„‚.isIdentity + eq = funExt Ξ» A β†’ funExt Ξ» B β†’ β„‚.leftIdentity isDistributive : IsDistributive isDistributive {A} {B} {C} {f = f} {g}