Use correct order for left- and right identity

Define and use helpers left- and right identity

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} (𝟙 (object ⊗ ℂ) {c})        ≡⟨⟩
-      fmap {c} {c} (idN F , 𝟙 ℂ)             ≡⟨⟩
+      fmap {c} {c} (idN F , 𝟙 ℂ)               ≡⟨⟩
       𝔻 [ identityTrans F C ∘ F.fmap (𝟙 ℂ)]    ≡⟨⟩
-      𝔻 [ 𝟙 𝔻 ∘ F.fmap (𝟙 ℂ)]                  ≡⟨ proj₂ 𝔻.isIdentity ⟩
+      𝔻 [ 𝟙 𝔻 ∘ F.fmap (𝟙 ℂ)]                  ≡⟨ 𝔻.leftIdentity ⟩
       F.fmap (𝟙 ℂ)                             ≡⟨ F.isIdentity ⟩
       𝟙 𝔻                                       ∎
       where

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
 

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
-        × (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f
+        × (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f
-      isIdentity = ident-r , ident-l
+      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

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

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 ℓ
+        productObject : Object
-        A = proj₁ 0A
+        productObject = (A × B) , sigPresSet sA λ _ → sB
-        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
 
         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
+        module _ (hX : Object) where
-        RawProduct.object rawProduct = 0A×0B
+          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
+        IsProduct.ump isProduct {X = hX} f g
-          = (f &&& g) , lem {0X = X} 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
       }
     }

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

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))

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 ⟩
       𝟙 ∎
 

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                            ≡⟨ ℂ.leftIdentity ⟩
-    f                         ∎
+    f                                ∎
 
   isDistributive : IsDistributive
   isDistributive {X} {Y} {Z} g f = sym aux

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 ]              ≡⟨ 𝔻.leftIdentity ⟩
-    F→ f                            ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩
+    F→ f                            ≡⟨ sym 𝔻.rightIdentity ⟩
     𝔻 [ F→ f ∘ 𝟙 𝔻 ]               ≡⟨⟩
     𝔻 [ F→ f ∘ identityTrans F A ]  ∎
     where

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}