diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 55d717c..a24abc8 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -18,7 +18,7 @@ module _ (ℓ ℓ' : Level) where RawCategory.Object RawCat = Category ℓ ℓ' RawCategory.Arrow RawCat = Functor RawCategory.identity RawCat = Functors.identity - RawCategory._∘_ RawCat = F[_∘_] + RawCategory._<<<_ RawCat = F[_∘_] -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors, -- however, form a groupoid! Therefore there is no (1-)category of @@ -50,18 +50,18 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ] identity : {o : Obj} → Arr o o identity = ℂ.identity , 𝔻.identity - _∘_ : + _<<<_ : {a b c : Obj} → Arr b c → Arr a b → Arr a c - _∘_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]} + _<<<_ = λ { (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.identity rawProduct = identity - RawCategory._∘_ rawProduct = _∘_ + RawCategory._<<<_ rawProduct = _<<<_ open RawCategory rawProduct diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda index 5322b16..fde96b9 100644 --- a/src/Cat/Categories/Cube.agda +++ b/src/Cat/Categories/Cube.agda @@ -19,7 +19,7 @@ open import Cat.Category.Functor -- See section 6.8 in Huber's thesis for details on how to implement the -- categorical version of CTT -open Category hiding (_∘_) +open Category hiding (_<<<_) open Functor module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where @@ -68,7 +68,7 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where Raw.Object Rawℂ = FiniteDecidableSubset Raw.Arrow Rawℂ = Hom Raw.identity Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} } - Raw._∘_ Rawℂ = {!!} + Raw._<<<_ Rawℂ = {!!} postulate IsCategoryℂ : IsCategory Rawℂ diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda index dd5c757..a0b4d1d 100644 --- a/src/Cat/Categories/Fam.agda +++ b/src/Cat/Categories/Fam.agda @@ -14,15 +14,15 @@ module _ (ℓa ℓb : Level) where identity : {A : Object} → Arr A A fst identity = λ x → x snd 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' + _<<<_ : {a b c : Object} → Arr b c → Arr a b → Arr a c + (g , g') <<< (f , f') = g Function.∘ f , g' Function.∘ f' RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb) RawFam = record { Object = Object ; Arrow = Arr ; identity = λ { {A} → identity {A = A}} - ; _∘_ = λ {a b c} → _∘_ {a} {b} {c} + ; _<<<_ = λ {a b c} → _<<<_ {a} {b} {c} } open RawCategory RawFam hiding (Object ; identity) diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index e6aa4c7..58b777d 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -30,7 +30,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where RawCategory.Object RawFree = ℂ.Object RawCategory.Arrow RawFree = Path ℂ.Arrow RawCategory.identity RawFree = empty - RawCategory._∘_ RawFree = concatenate + RawCategory._<<<_ RawFree = concatenate open RawCategory RawFree diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 48ee817..da71f2c 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -20,7 +20,7 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C RawCategory.Object raw = Functor ℂ 𝔻 RawCategory.Arrow raw = NaturalTransformation RawCategory.identity raw {F} = identity F - RawCategory._∘_ raw {F} {G} {H} = NT[_∘_] {F} {G} {H} + RawCategory._<<<_ raw {F} {G} {H} = NT[_∘_] {F} {G} {H} module _ where open RawCategory raw hiding (identity) @@ -154,9 +154,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 ≡ identity A + vr : _<<<_ {A = A} {B} {A} re ob ≡ identity A vr = {!!} - rv : _∘_ {A = B} {A} {B} ob re ≡ identity B + rv : _<<<_ {A = B} {A} {B} ob re ≡ identity B rv = {!!} isInverse : IsInverseOf {A} {B} ob re isInverse = vr , rv @@ -201,7 +201,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where { Object = Presheaf ℂ ; Arrow = NaturalTransformation ; identity = λ {F} → identity F - ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H} + ; _<<<_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H} } -- isCategory : IsCategory raw diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index 71630e4..71c9044 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -154,7 +154,7 @@ RawRel = record { Object = Set ; Arrow = λ S R → Subset (S × R) ; identity = λ {S} → Diag S - ; _∘_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )} + ; _<<<_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )} } isPreCategory : IsPreCategory RawRel diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 7870fc0..f950339 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -26,11 +26,11 @@ module _ (ℓ : Level) where RawCategory.Object SetsRaw = hSet ℓ RawCategory.Arrow SetsRaw (T , _) (U , _) = T → U RawCategory.identity SetsRaw = Function.id - RawCategory._∘_ SetsRaw = Function._∘′_ + RawCategory._<<<_ SetsRaw = Function._∘′_ module _ where private - open RawCategory SetsRaw hiding (_∘_) + open RawCategory SetsRaw hiding (_<<<_) isIdentity : IsIdentity Function.id fst isIdentity = funExt λ _ → refl @@ -44,7 +44,7 @@ module _ (ℓ : Level) where IsPreCategory.isIdentity isPreCat {A} {B} = isIdentity {A} {B} IsPreCategory.arrowsAreSets isPreCat {A} {B} = arrowsAreSets {A} {B} - open IsPreCategory isPreCat hiding (_∘_) + open IsPreCategory isPreCat hiding (_<<<_) isIso = TypeIsomorphism module _ {hA hB : hSet ℓ} where diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 1818c15..6190052 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -13,7 +13,7 @@ -- Data -- ---- -- identity; the identity arrow --- _∘_; function composition +-- _<<<_; function composition -- -- Laws -- ---- @@ -52,9 +52,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where 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 + _<<<_ : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C - infixl 10 _∘_ _>>>_ + infixl 10 _<<<_ _>>>_ -- | Operations on data @@ -65,7 +65,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where codomain {b = b} _ = b _>>>_ : {A B C : Object} → (Arrow A B) → (Arrow B C) → Arrow A C - f >>> g = g ∘ f + f >>> g = g <<< f -- | Laws about the data @@ -73,17 +73,17 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where -- right-hand-side. IsAssociative : Set (ℓa ⊔ ℓb) IsAssociative = ∀ {A B C D} {f : Arrow A B} {g : Arrow B C} {h : Arrow C D} - → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f + → h <<< (g <<< f) ≡ (h <<< g) <<< f IsIdentity : ({A : Object} → Arrow A A) → Set (ℓa ⊔ ℓb) IsIdentity id = {A B : Object} {f : Arrow A B} - → id ∘ f ≡ f × f ∘ id ≡ f + → id <<< f ≡ f × f <<< id ≡ f ArrowsAreSets : Set (ℓa ⊔ ℓb) ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B) IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb - IsInverseOf = λ f g → g ∘ f ≡ identity × f ∘ g ≡ identity + 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 @@ -93,10 +93,10 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where module _ {A B : Object} where Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓb - Epimorphism {X} f = (g₀ g₁ : Arrow B X) → g₀ ∘ f ≡ g₁ ∘ f → g₀ ≡ g₁ + Epimorphism {X} f = (g₀ g₁ : Arrow B X) → g₀ <<< f ≡ g₁ <<< f → g₀ ≡ g₁ Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb - Monomorphism {X} f = (g₀ g₁ : Arrow X A) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁ + Monomorphism {X} f = (g₀ g₁ : Arrow X A) → f <<< g₀ ≡ f <<< g₁ → g₀ ≡ g₁ IsInitial : Object → Set (ℓa ⊔ ℓb) IsInitial I = {X : Object} → isContr (Arrow I X) @@ -167,10 +167,10 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where arrowsAreSets : ArrowsAreSets open Univalence isIdentity public - leftIdentity : {A B : Object} {f : Arrow A B} → identity ∘ 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 ∘ identity ≡ f + rightIdentity : {A B : Object} {f : Arrow A B} → f <<< identity ≡ f rightIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f}) ------------ @@ -181,26 +181,26 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where module _ {A B : Object} {X : Object} (f : Arrow A B) where iso→epi : Isomorphism f → Epimorphism {X = X} f iso→epi (f- , left-inv , right-inv) g₀ g₁ eq = begin - g₀ ≡⟨ sym rightIdentity ⟩ - 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₁ ∘ identity ≡⟨ rightIdentity ⟩ - g₁ ∎ + g₀ ≡⟨ sym rightIdentity ⟩ + 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₁ <<< 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 ⟩ - 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 ⟩ - identity ∘ g₁ ≡⟨ leftIdentity ⟩ - g₁ ∎ + g₀ ≡⟨ sym leftIdentity ⟩ + 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 ⟩ + identity <<< g₁ ≡⟨ leftIdentity ⟩ + g₁ ∎ iso→epi×mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f iso→epi×mono iso = iso→epi iso , iso→mono iso @@ -210,7 +210,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f) propIsIdentity {id} = propPiImpl (λ _ → propPiImpl λ _ → propPiImpl (λ f → - propSig (arrowsAreSets (id ∘ f) f) λ _ → arrowsAreSets (f ∘ id) f)) + propSig (arrowsAreSets (id <<< f) f) λ _ → arrowsAreSets (f <<< id) f)) propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B)) propArrowIsSet = propPiImpl λ _ → propPiImpl (λ _ → isSetIsProp) @@ -225,12 +225,12 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where where geq : g ≡ g' geq = begin - g ≡⟨ sym rightIdentity ⟩ - g ∘ identity ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩ - g ∘ (f ∘ g') ≡⟨ isAssociative ⟩ - (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩ - identity ∘ g' ≡⟨ leftIdentity ⟩ - g' ∎ + g ≡⟨ sym rightIdentity ⟩ + g <<< identity ≡⟨ cong (λ φ → g <<< φ) (sym ε') ⟩ + g <<< (f <<< g') ≡⟨ isAssociative ⟩ + (g <<< f) <<< g' ≡⟨ cong (λ φ → φ <<< g') η ⟩ + identity <<< g' ≡⟨ leftIdentity ⟩ + g' ∎ propIsInitial : ∀ I → isProp (IsInitial I) propIsInitial I x y i {X} = res X i @@ -266,23 +266,23 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where private trans≅ : Transitive _≅_ trans≅ (f , f~ , f-inv) (g , g~ , g-inv) - = g ∘ f - , f~ ∘ g~ + = g <<< f + , f~ <<< g~ , ( begin - (f~ ∘ g~) ∘ (g ∘ f) ≡⟨ isAssociative ⟩ - (f~ ∘ g~) ∘ g ∘ f ≡⟨ cong (λ φ → φ ∘ f) (sym isAssociative) ⟩ - f~ ∘ (g~ ∘ g) ∘ f ≡⟨ cong (λ φ → f~ ∘ φ ∘ f) (fst g-inv) ⟩ - f~ ∘ identity ∘ f ≡⟨ cong (λ φ → φ ∘ f) rightIdentity ⟩ - f~ ∘ f ≡⟨ fst f-inv ⟩ - identity ∎ + (f~ <<< g~) <<< (g <<< f) ≡⟨ isAssociative ⟩ + (f~ <<< g~) <<< g <<< f ≡⟨ cong (λ φ → φ <<< f) (sym isAssociative) ⟩ + f~ <<< (g~ <<< g) <<< f ≡⟨ cong (λ φ → f~ <<< φ <<< f) (fst g-inv) ⟩ + f~ <<< identity <<< f ≡⟨ cong (λ φ → φ <<< f) rightIdentity ⟩ + f~ <<< f ≡⟨ fst f-inv ⟩ + identity ∎ ) , ( begin - g ∘ f ∘ (f~ ∘ g~) ≡⟨ isAssociative ⟩ - g ∘ f ∘ f~ ∘ g~ ≡⟨ cong (λ φ → φ ∘ g~) (sym isAssociative) ⟩ - g ∘ (f ∘ f~) ∘ g~ ≡⟨ cong (λ φ → g ∘ φ ∘ g~) (snd f-inv) ⟩ - g ∘ identity ∘ g~ ≡⟨ cong (λ φ → φ ∘ g~) rightIdentity ⟩ - g ∘ g~ ≡⟨ snd g-inv ⟩ - identity ∎ + g <<< f <<< (f~ <<< g~) ≡⟨ isAssociative ⟩ + g <<< f <<< f~ <<< g~ ≡⟨ cong (λ φ → φ <<< g~) (sym isAssociative) ⟩ + g <<< (f <<< f~) <<< g~ ≡⟨ cong (λ φ → g <<< φ <<< g~) (snd f-inv) ⟩ + g <<< identity <<< g~ ≡⟨ cong (λ φ → φ <<< g~) rightIdentity ⟩ + g <<< g~ ≡⟨ snd g-inv ⟩ + identity ∎ ) isPreorder : IsPreorder _≅_ isPreorder = record { isEquivalence = equalityIsEquivalence ; reflexive = idToIso _ _ ; trans = trans≅ } @@ -341,7 +341,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where pq : Arrow a b ≡ Arrow a' b' pq i = Arrow (p i) (q i) - 9-1-9 : coe pq f ≡ q* ∘ f ∘ p~ + 9-1-9 : coe pq f ≡ q* <<< f <<< p~ 9-1-9 = transpP {!!} {!!} -- | All projections are propositions. @@ -366,9 +366,9 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where 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 ≡ identity + left : Y→X <<< X→Y ≡ identity left = Xprop _ _ - right : X→Y ∘ Y→X ≡ identity + right : X→Y <<< Y→X ≡ identity right = Yprop _ _ iso : X ≅ Y iso = X→Y , Y→X , left , right @@ -396,9 +396,9 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where 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 ≡ identity + left : Y→X <<< X→Y ≡ identity left = Yprop _ _ - right : X→Y ∘ Y→X ≡ identity + right : X→Y <<< Y→X ≡ identity right = Xprop _ _ iso : X ≅ Y iso = Y→X , X→Y , right , left @@ -497,7 +497,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where _[_,_] = Arrow _[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C - _[_∘_] = _∘_ + _[_∘_] = _<<<_ -- | The opposite category -- @@ -512,7 +512,7 @@ module Opposite {ℓa ℓb : Level} where RawCategory.Object opRaw = ℂ.Object RawCategory.Arrow opRaw = Function.flip ℂ.Arrow RawCategory.identity opRaw = ℂ.identity - RawCategory._∘_ opRaw = ℂ._>>>_ + RawCategory._<<<_ opRaw = ℂ._>>>_ open RawCategory opRaw @@ -561,7 +561,7 @@ module Opposite {ℓa ℓb : Level} where -- inv : AreInverses (ℂ.idToIso A B) f inv-ζ : AreInverses (idToIso A B) ζ - -- recto-verso : ℂ.idToIso A B ∘ f ≡ idFun (A ℂ.≅ B) + -- recto-verso : ℂ.idToIso A B <<< f ≡ idFun (A ℂ.≅ B) inv-ζ = record { verso-recto = funExt (λ x → begin (ζ ⊙ idToIso A B) x ≡⟨⟩ @@ -600,7 +600,7 @@ module Opposite {ℓa ℓb : Level} where RawCategory.Object (rawInv _) = Object RawCategory.Arrow (rawInv _) = Arrow RawCategory.identity (rawInv _) = identity - RawCategory._∘_ (rawInv _) = _∘_ + RawCategory._<<<_ (rawInv _) = _<<<_ oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ oppositeIsInvolution = Category≡ rawInv diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 8ad64fa..85b23e4 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -36,7 +36,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where open Cat.Category.NaturalTransformation ℂ ℂ using (NaturalTransformation ; propIsNatural) private module ℂ = Category ℂ - open ℂ using (Object ; Arrow ; identity ; _∘_ ; _>>>_) + open ℂ using (Object ; Arrow ; identity ; _<<<_ ; _>>>_) module M = Monoidal ℂ module K = Kleisli ℂ @@ -74,21 +74,21 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where backIsMonad : M.IsMonad backRaw M.IsMonad.isAssociative backIsMonad {X} = begin - joinT X ∘ R.fmap (joinT X) ≡⟨⟩ - join ∘ fmap (joinT X) ≡⟨⟩ - join ∘ fmap join ≡⟨ isNaturalForeign ⟩ - join ∘ join ≡⟨⟩ - joinT X ∘ joinT (R.omap X) ∎ + joinT X <<< R.fmap (joinT X) ≡⟨⟩ + join <<< fmap (joinT X) ≡⟨⟩ + join <<< fmap join ≡⟨ isNaturalForeign ⟩ + join <<< join ≡⟨⟩ + joinT X <<< joinT (R.omap X) ∎ M.IsMonad.isInverse backIsMonad {X} = inv-l , inv-r where inv-l = begin - joinT X ∘ pureT (R.omap X) ≡⟨⟩ - join ∘ pure ≡⟨ fst isInverse ⟩ - identity ∎ + joinT X <<< pureT (R.omap X) ≡⟨⟩ + join <<< pure ≡⟨ fst isInverse ⟩ + identity ∎ inv-r = begin - joinT X ∘ R.fmap (pureT X) ≡⟨⟩ - join ∘ fmap pure ≡⟨ snd isInverse ⟩ - identity ∎ + joinT X <<< R.fmap (pureT X) ≡⟨⟩ + join <<< fmap pure ≡⟨ snd isInverse ⟩ + identity ∎ back : K.Monad → M.Monad Monoidal.Monad.raw (back m) = backRaw m @@ -101,11 +101,11 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where → K.RawMonad.bind (forthRaw (backRaw m)) {X} {Y} ≡ K.RawMonad.bind (K.Monad.raw m) bindEq {X} {Y} = begin - K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩ - (λ f → join ∘ fmap f) ≡⟨⟩ + K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩ + (λ f → join <<< fmap f) ≡⟨⟩ (λ f → bind (f >>> pure) >>> bind identity) ≡⟨ funExt lem ⟩ - (λ f → bind f) ≡⟨⟩ - bind ∎ + (λ f → bind f) ≡⟨⟩ + bind ∎ where lem : (f : Arrow X (omap Y)) → bind (f >>> pure) >>> bind identity @@ -139,18 +139,18 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where bindEq : ∀ {X Y} {f : Arrow X (Romap Y)} → KM.bind f ≡ bind f bindEq {X} {Y} {f} = begin - KM.bind f ≡⟨⟩ - joinT Y ∘ Rfmap f ≡⟨⟩ - bind f ∎ + KM.bind f ≡⟨⟩ + joinT Y <<< Rfmap f ≡⟨⟩ + bind f ∎ joinEq : ∀ {X} → KM.join ≡ joinT X joinEq {X} = begin - KM.join ≡⟨⟩ - KM.bind identity ≡⟨⟩ - bind identity ≡⟨⟩ - joinT X ∘ Rfmap identity ≡⟨ cong (λ φ → _ ∘ φ) R.isIdentity ⟩ - joinT X ∘ identity ≡⟨ ℂ.rightIdentity ⟩ - joinT X ∎ + KM.join ≡⟨⟩ + 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 fmapEq {A} {B} = funExt (λ f → begin @@ -160,8 +160,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where Rfmap (f >>> pureT B) >>> joinT B ≡⟨⟩ 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) (snd isInverse) ⟩ - identity ∘ Rfmap f ≡⟨ ℂ.leftIdentity ⟩ + joinT B <<< Rfmap (pureT B) <<< Rfmap f ≡⟨ cong (λ φ → φ <<< Rfmap f) (snd isInverse) ⟩ + 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 identity ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩ - joinT X ∘ identity ≡⟨ ℂ.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 1faf079..55e9cf5 100644 --- a/src/Cat/Category/Monad/Kleisli.agda +++ b/src/Cat/Category/Monad/Kleisli.agda @@ -18,7 +18,7 @@ open import Cat.Category.NaturalTransformation ℂ ℂ private ℓ = ℓa ⊔ ℓb module ℂ = Category ℂ - open ℂ using (Arrow ; identity ; Object ; _∘_ ; _>>>_) + open ℂ using (Arrow ; identity ; Object ; _<<<_ ; _>>>_) -- | Data for a monad. -- @@ -34,7 +34,7 @@ record RawMonad : Set ℓ where -- -- This should perhaps be defined in a "Klesli-version" of functors as well? fmap : ∀ {A B} → ℂ [ A , B ] → ℂ [ omap A , omap B ] - fmap f = bind (pure ∘ f) + fmap f = bind (pure <<< f) -- | Composition of monads aka. the kleisli-arrow. _>=>_ : {A B C : Object} → ℂ [ A , omap B ] → ℂ [ B , omap C ] → ℂ [ A , omap C ] @@ -62,14 +62,14 @@ record RawMonad : Set ℓ where -- This is really a functor law. Should we have a kleisli-representation of -- functors as well and make them a super-class? Fusion = {X Y Z : Object} {g : ℂ [ Y , Z ]} {f : ℂ [ X , Y ]} - → fmap (g ∘ f) ≡ fmap g ∘ fmap f + → fmap (g <<< f) ≡ fmap g <<< fmap f -- In the ("foreign") formulation of a monad `IsNatural`'s analogue here would be: IsNaturalForeign : Set _ - IsNaturalForeign = {X : Object} → join {X} ∘ fmap join ≡ join ∘ join + IsNaturalForeign = {X : Object} → join {X} <<< fmap join ≡ join <<< join IsInverse : Set _ - IsInverse = {X : Object} → join {X} ∘ pure ≡ identity × join {X} ∘ fmap pure ≡ identity + IsInverse = {X : Object} → join {X} <<< pure ≡ identity × join {X} <<< fmap pure ≡ identity record IsMonad (raw : RawMonad) : Set ℓ where open RawMonad raw public @@ -81,18 +81,21 @@ record IsMonad (raw : RawMonad) : Set ℓ where -- | Map fusion is admissable. fusion : Fusion fusion {g = g} {f} = begin - fmap (g ∘ f) ≡⟨⟩ - bind ((f >>> g) >>> pure) ≡⟨ cong bind ℂ.isAssociative ⟩ - bind (f >>> (g >>> pure)) ≡⟨ cong (λ φ → bind (f >>> φ)) (sym (isNatural _)) ⟩ - bind (f >>> (pure >>> (bind (g >>> pure)))) ≡⟨⟩ + fmap (g <<< f) ≡⟨⟩ + bind ((f >>> g) >>> pure) ≡⟨ cong bind ℂ.isAssociative ⟩ + bind (f >>> (g >>> pure)) + ≡⟨ cong (λ φ → bind (f >>> φ)) (sym (isNatural _)) ⟩ + bind (f >>> (pure >>> (bind (g >>> pure)))) + ≡⟨⟩ bind (f >>> (pure >>> fmap g)) ≡⟨⟩ - bind ((fmap g ∘ pure) ∘ f) ≡⟨ cong bind (sym ℂ.isAssociative) ⟩ - bind (fmap g ∘ (pure ∘ f)) ≡⟨ sym distrib ⟩ - bind (pure ∘ g) ∘ bind (pure ∘ f) ≡⟨⟩ - fmap g ∘ fmap f ∎ + bind ((fmap g <<< pure) <<< f) ≡⟨ cong bind (sym ℂ.isAssociative) ⟩ + bind (fmap g <<< (pure <<< f)) ≡⟨ sym distrib ⟩ + bind (pure <<< g) <<< bind (pure <<< f) + ≡⟨⟩ + fmap g <<< fmap f ∎ where - distrib : fmap g ∘ fmap f ≡ bind (fmap g ∘ (pure ∘ f)) - distrib = isDistributive (pure ∘ g) (pure ∘ f) + distrib : fmap g <<< fmap f ≡ bind (fmap g <<< (pure <<< f)) + distrib = isDistributive (pure <<< g) (pure <<< f) -- | This formulation gives rise to the following endo-functor. private @@ -102,15 +105,15 @@ record IsMonad (raw : RawMonad) : Set ℓ where isFunctorR : IsFunctor ℂ ℂ rawR IsFunctor.isIdentity isFunctorR = begin - bind (pure ∘ identity) ≡⟨ cong bind (ℂ.rightIdentity) ⟩ - bind pure ≡⟨ isIdentity ⟩ - identity ∎ + bind (pure <<< identity) ≡⟨ cong bind (ℂ.rightIdentity) ⟩ + bind pure ≡⟨ isIdentity ⟩ + identity ∎ IsFunctor.isDistributive isFunctorR {f = f} {g} = begin - bind (pure ∘ (g ∘ f)) ≡⟨⟩ - fmap (g ∘ f) ≡⟨ fusion ⟩ - fmap g ∘ fmap f ≡⟨⟩ - bind (pure ∘ g) ∘ bind (pure ∘ f) ∎ + bind (pure <<< (g <<< f)) ≡⟨⟩ + fmap (g <<< f) ≡⟨ fusion ⟩ + fmap g <<< fmap f ≡⟨⟩ + bind (pure <<< g) <<< bind (pure <<< f) ∎ -- FIXME Naming! R : EndoFunctor ℂ @@ -129,20 +132,20 @@ record IsMonad (raw : RawMonad) : Set ℓ where pureT A = pure pureN : Natural R⁰ R pureT pureN {A} {B} f = begin - pureT B ∘ R⁰.fmap f ≡⟨⟩ - pure ∘ f ≡⟨ sym (isNatural _) ⟩ - bind (pure ∘ f) ∘ pure ≡⟨⟩ - fmap f ∘ pure ≡⟨⟩ - R.fmap f ∘ pureT A ∎ + pureT B <<< R⁰.fmap f ≡⟨⟩ + pure <<< f ≡⟨ sym (isNatural _) ⟩ + bind (pure <<< f) <<< pure ≡⟨⟩ + fmap f <<< pure ≡⟨⟩ + R.fmap f <<< pureT A ∎ joinT : Transformation R² R joinT C = join joinN : Natural R² R joinT joinN f = begin - join ∘ R².fmap f ≡⟨⟩ - bind identity ∘ R².fmap f ≡⟨⟩ - R².fmap f >>> bind identity ≡⟨⟩ - fmap (fmap f) >>> bind identity ≡⟨⟩ - fmap (bind (f >>> pure)) >>> bind identity ≡⟨⟩ + join <<< R².fmap f ≡⟨⟩ + 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) >=> identity) @@ -155,14 +158,14 @@ record IsMonad (raw : RawMonad) : Set ℓ where ≡⟨ cong bind ℂ.leftIdentity ⟩ bind (bind (f >>> pure)) ≡⟨ cong bind (sym ℂ.rightIdentity) ⟩ - bind (identity >>> bind (f >>> pure)) ≡⟨⟩ + bind (identity >>> bind (f >>> pure)) ≡⟨⟩ bind (identity >=> (f >>> pure)) ≡⟨ sym (isDistributive _ _) ⟩ - bind identity >>> bind (f >>> pure) ≡⟨⟩ - bind identity >>> fmap f ≡⟨⟩ - bind identity >>> R.fmap f ≡⟨⟩ - R.fmap f ∘ bind identity ≡⟨⟩ - R.fmap f ∘ join ∎ + 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 fst pureNT = pureT diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda index 707ea07..fdd739e 100644 --- a/src/Cat/Category/Monad/Monoidal.agda +++ b/src/Cat/Category/Monad/Monoidal.agda @@ -16,7 +16,7 @@ module Cat.Category.Monad.Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb private ℓ = ℓa ⊔ ℓb -open Category ℂ using (Object ; Arrow ; identity ; _∘_) +open Category ℂ using (Object ; Arrow ; identity ; _<<<_) open import Cat.Category.NaturalTransformation ℂ ℂ using (NaturalTransformation ; Transformation ; Natural) @@ -42,19 +42,19 @@ record RawMonad : Set ℓ where Rfmap = Functor.fmap R bind : {X Y : Object} → ℂ [ X , Romap Y ] → ℂ [ Romap X , Romap Y ] - bind {X} {Y} f = joinT Y ∘ Rfmap f + bind {X} {Y} f = joinT Y <<< Rfmap f IsAssociative : Set _ IsAssociative = {X : Object} - → joinT X ∘ Rfmap (joinT X) ≡ joinT X ∘ joinT (Romap X) + → joinT X <<< Rfmap (joinT X) ≡ joinT X <<< joinT (Romap X) IsInverse : Set _ IsInverse = {X : Object} - → joinT X ∘ pureT (Romap X) ≡ identity - × joinT X ∘ Rfmap (pureT X) ≡ identity - IsNatural = ∀ {X Y} f → joinT Y ∘ Rfmap f ∘ pureT X ≡ f + → 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) - ≡ joinT Z ∘ Rfmap (joinT Z ∘ Rfmap g ∘ f) + → joinT Z <<< Rfmap g <<< (joinT Y <<< Rfmap f) + ≡ joinT Z <<< Rfmap (joinT Z <<< Rfmap g <<< f) record IsMonad (raw : RawMonad) : Set ℓ where open RawMonad raw public @@ -68,48 +68,48 @@ record IsMonad (raw : RawMonad) : Set ℓ where isNatural : IsNatural isNatural {X} {Y} f = begin - joinT Y ∘ R.fmap f ∘ pureT X ≡⟨ sym ℂ.isAssociative ⟩ - 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) (fst isInverse) ⟩ - identity ∘ f ≡⟨ ℂ.leftIdentity ⟩ - f ∎ + joinT Y <<< R.fmap f <<< pureT X ≡⟨ sym ℂ.isAssociative ⟩ + 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) (fst isInverse) ⟩ + identity <<< f ≡⟨ ℂ.leftIdentity ⟩ + f ∎ isDistributive : IsDistributive isDistributive {X} {Y} {Z} g f = sym aux where module R² = Functor F[ R ∘ R ] distrib3 : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B} - → R.fmap (a ∘ b ∘ c) - ≡ R.fmap a ∘ R.fmap b ∘ R.fmap c + → R.fmap (a <<< b <<< c) + ≡ R.fmap a <<< R.fmap b <<< R.fmap c distrib3 {a = a} {b} {c} = begin - R.fmap (a ∘ b ∘ c) ≡⟨ R.isDistributive ⟩ - R.fmap (a ∘ b) ∘ R.fmap c ≡⟨ cong (_∘ _) R.isDistributive ⟩ - R.fmap a ∘ R.fmap b ∘ R.fmap c ∎ + R.fmap (a <<< b <<< c) ≡⟨ R.isDistributive ⟩ + R.fmap (a <<< b) <<< R.fmap c ≡⟨ cong (_<<< _) R.isDistributive ⟩ + R.fmap a <<< R.fmap b <<< R.fmap c ∎ aux = begin - joinT Z ∘ R.fmap (joinT Z ∘ R.fmap g ∘ f) - ≡⟨ cong (λ φ → joinT Z ∘ φ) distrib3 ⟩ - joinT Z ∘ (R.fmap (joinT Z) ∘ R.fmap (R.fmap g) ∘ R.fmap f) + joinT Z <<< R.fmap (joinT Z <<< R.fmap g <<< f) + ≡⟨ cong (λ φ → joinT Z <<< φ) distrib3 ⟩ + joinT Z <<< (R.fmap (joinT Z) <<< R.fmap (R.fmap g) <<< R.fmap f) ≡⟨⟩ - joinT Z ∘ (R.fmap (joinT Z) ∘ R².fmap g ∘ R.fmap f) - ≡⟨ cong (_∘_ (joinT Z)) (sym ℂ.isAssociative) ⟩ - joinT Z ∘ (R.fmap (joinT Z) ∘ (R².fmap g ∘ R.fmap f)) + joinT Z <<< (R.fmap (joinT Z) <<< R².fmap g <<< R.fmap f) + ≡⟨ cong (_<<<_ (joinT Z)) (sym ℂ.isAssociative) ⟩ + joinT Z <<< (R.fmap (joinT Z) <<< (R².fmap g <<< R.fmap f)) ≡⟨ ℂ.isAssociative ⟩ - (joinT Z ∘ R.fmap (joinT Z)) ∘ (R².fmap g ∘ R.fmap f) - ≡⟨ cong (λ φ → φ ∘ (R².fmap g ∘ R.fmap f)) isAssociative ⟩ - (joinT Z ∘ joinT (R.omap Z)) ∘ (R².fmap g ∘ R.fmap f) + (joinT Z <<< R.fmap (joinT Z)) <<< (R².fmap g <<< R.fmap f) + ≡⟨ cong (λ φ → φ <<< (R².fmap g <<< R.fmap f)) isAssociative ⟩ + (joinT Z <<< joinT (R.omap Z)) <<< (R².fmap g <<< R.fmap f) ≡⟨ ℂ.isAssociative ⟩ - joinT Z ∘ joinT (R.omap Z) ∘ R².fmap g ∘ R.fmap f + joinT Z <<< joinT (R.omap Z) <<< R².fmap g <<< R.fmap f ≡⟨⟩ - ((joinT Z ∘ joinT (R.omap Z)) ∘ R².fmap g) ∘ R.fmap f - ≡⟨ cong (_∘ R.fmap f) (sym ℂ.isAssociative) ⟩ - (joinT Z ∘ (joinT (R.omap Z) ∘ R².fmap g)) ∘ R.fmap f - ≡⟨ cong (λ φ → φ ∘ R.fmap f) (cong (_∘_ (joinT Z)) (joinN g)) ⟩ - (joinT Z ∘ (R.fmap g ∘ joinT Y)) ∘ R.fmap f - ≡⟨ cong (_∘ R.fmap f) ℂ.isAssociative ⟩ - joinT Z ∘ R.fmap g ∘ joinT Y ∘ R.fmap f + ((joinT Z <<< joinT (R.omap Z)) <<< R².fmap g) <<< R.fmap f + ≡⟨ cong (_<<< R.fmap f) (sym ℂ.isAssociative) ⟩ + (joinT Z <<< (joinT (R.omap Z) <<< R².fmap g)) <<< R.fmap f + ≡⟨ cong (λ φ → φ <<< R.fmap f) (cong (_<<<_ (joinT Z)) (joinN g)) ⟩ + (joinT Z <<< (R.fmap g <<< joinT Y)) <<< R.fmap f + ≡⟨ cong (_<<< R.fmap f) ℂ.isAssociative ⟩ + joinT Z <<< R.fmap g <<< joinT Y <<< R.fmap f ≡⟨ sym (Category.isAssociative ℂ) ⟩ - joinT Z ∘ R.fmap g ∘ (joinT Y ∘ R.fmap f) + joinT Z <<< R.fmap g <<< (joinT Y <<< R.fmap f) ∎ record Monad : Set ℓ where diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index 3aa73ba..caa993f 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -105,8 +105,8 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} × ℂ [ y1 ∘ f ] ≡ x1 } ; identity = λ{ {X , f , g} → ℂ.identity {X} , ℂ.rightIdentity , ℂ.rightIdentity} - ; _∘_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} (f , f0 , f1) (g , g0 , g1) - → (f ℂ.∘ g) + ; _<<<_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} (f , f0 , f1) (g , g0 , g1) + → (f ℂ.<<< g) , (begin ℂ [ c0 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩ ℂ [ ℂ [ c0 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f0 ⟩ @@ -134,9 +134,9 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} isAssociative {A'@(A , a0 , a1)} {B , _} {C , c0 , c1} {D'@(D , d0 , d1)} {ff@(f , f0 , f1)} {gg@(g , g0 , g1)} {hh@(h , h0 , h1)} i = s0 i , lemPropF propEqs s0 {P.snd l} {P.snd r} i where - l = hh ∘ (gg ∘ ff) - r = hh ∘ gg ∘ ff - -- s0 : h ℂ.∘ (g ℂ.∘ f) ≡ h ℂ.∘ g ℂ.∘ f + l = hh <<< (gg <<< ff) + r = hh <<< gg <<< ff + -- s0 : h ℂ.<<< (g ℂ.<<< f) ≡ h ℂ.<<< g ℂ.<<< f s0 : fst l ≡ fst r s0 = ℂ.isAssociative {f = f} {g} {h} @@ -144,18 +144,18 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} isIdentity : IsIdentity identity isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity where - leftIdentity : identity ∘ (f , f0 , f1) ≡ (f , f0 , f1) + leftIdentity : identity <<< (f , f0 , f1) ≡ (f , f0 , f1) leftIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i where - L = identity ∘ (f , f0 , f1) + L = identity <<< (f , f0 , f1) R : Arrow AA BB R = f , f0 , f1 l : fst L ≡ fst R l = ℂ.leftIdentity - rightIdentity : (f , f0 , f1) ∘ identity ≡ (f , f0 , f1) + rightIdentity : (f , f0 , f1) <<< identity ≡ (f , f0 , f1) rightIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i where - L = (f , f0 , f1) ∘ identity + L = (f , f0 , f1) <<< identity R : Arrow AA BB R = (f , f0 , f1) l : ℂ [ f ∘ ℂ.identity ] ≡ f