Minor modifications to transpositions of identifications along equiva…

…lences (#1033)

src/foundation/transposition-identifications-along-equivalences.lagda.md

@@ -8,8 +8,11 @@ module foundation.transposition-identifications-along-equivalences where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.commuting-triangles-of-identifications
+open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
 open import foundation.whiskering-identifications-concatenation
 
 open import foundation-core.equivalences
@@ -37,7 +40,21 @@ constructing this equivalence. One way uses the fact that `e⁻¹` is a
  (e x ＝ y) ≃ (e x ＝ e e⁻¹ y) ≃ (x ＝ e⁻¹ y).
 ```
 
-The other way uses the fact that `e⁻¹` is a
+In other words, the transpose of an identification `p : e x ＝ y` along `e` is
+the unique identification `q : x ＝ e⁻¹ y` equipped with an identification
+witnessing that the triangle
+
+```text
+      ap e q
+  e x ------> e (e⁻¹ y)
+     \       /
+    p \     / is-section-map-inv-equiv e y
+       \   /
+        ∨ ∨
+         y
+```
+
+commutes. The other way uses the fact that `e⁻¹` is a
 [retraction](foundation-core.retractions.md) of `e`, resulting in the
 equivalence
 
@@ -86,16 +103,17 @@ module _
   map-eq-transpose-equiv' {x} {y} = map-equiv (eq-transpose-equiv' x y)
 ```
 
+### Transposing identifications of reversed identity types along equivalences
+
 It is sometimes useful to consider identifications `y ＝ e x` instead of
 `e x ＝ y`, so we include an inverted equivalence for that as well.
 
 ```agda
   eq-transpose-equiv-inv :
     (x : A) (y : B) → (y ＝ map-equiv e x) ≃ (map-inv-equiv e y ＝ x)
   eq-transpose-equiv-inv x y =
-    ( equiv-inv x (map-inv-equiv e y)) ∘e
-    ( eq-transpose-equiv x y) ∘e
-    ( equiv-inv y (map-equiv e x))
+    ( inv-equiv (equiv-ap e _ _)) ∘e
+    ( equiv-concat (is-section-map-inv-equiv e y) _)
 
   map-eq-transpose-equiv-inv :
     {a : A} {b : B} → b ＝ map-equiv e a → map-inv-equiv e b ＝ a
@@ -109,7 +127,33 @@ It is sometimes useful to consider identifications `y ＝ e x` instead of
 
 ## Properties
 
-### Computation rules for transposing equivalences
+### Computing transposition of reflexivity along equivalences
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
+  where
+
+  compute-refl-eq-transpose-equiv :
+    {x : A} →
+    map-eq-transpose-equiv e refl ＝ inv (is-retraction-map-inv-equiv e x)
+  compute-refl-eq-transpose-equiv =
+    map-eq-transpose-equiv-inv
+      ( equiv-ap e _ (map-inv-equiv e _))
+      ( ap inv (coherence-map-inv-equiv e _) ∙
+        inv (ap-inv (map-equiv e) _))
+
+  compute-refl-eq-transpose-equiv-inv :
+    {x : A} →
+    map-eq-transpose-equiv-inv e refl ＝ is-retraction-map-inv-equiv e x
+  compute-refl-eq-transpose-equiv-inv {x} =
+    map-eq-transpose-equiv-inv
+      ( equiv-ap e _ _)
+      ( ( right-unit) ∙
+        ( coherence-map-inv-equiv e _))
+```
+
+### The two definitions of transposing identifications along equivalences are homotopic
 
 We begin by showing that the two equivalences stated above are homotopic.
 
@@ -118,113 +162,98 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
   where
 
-  htpy-map-eq-transpose-equiv :
+  compute-map-eq-transpose-equiv :
     {x : A} {y : B} →
     map-eq-transpose-equiv e {x} {y} ~ map-eq-transpose-equiv' e
-  htpy-map-eq-transpose-equiv {x} refl =
+  compute-map-eq-transpose-equiv {x} refl =
     ( map-eq-transpose-equiv-inv
       ( equiv-ap e x _)
       ( ( ap inv (coherence-map-inv-equiv e x)) ∙
         ( inv (ap-inv (map-equiv e) (is-retraction-map-inv-equiv e x))))) ∙
     ( inv right-unit)
 ```
 
-Transposing a composition of paths fits into a triangle with a transpose of the
-left factor.
-
-```agda
-  triangle-eq-transpose-equiv-concat :
-    {x : A} {y z : B} (p : map-equiv e x ＝ y) (q : y ＝ z) →
-    ( map-eq-transpose-equiv e (p ∙ q)) ＝
-    ( map-eq-transpose-equiv e p ∙ ap (map-inv-equiv e) q)
-  triangle-eq-transpose-equiv-concat refl refl = inv right-unit
-```
+### The defining commuting triangles of transposed identifications
 
 Transposed identifications fit in
 [commuting triangles](foundation.commuting-triangles-of-identifications.md) with
 the original identifications.
 
 ```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
+  where
+
   triangle-eq-transpose-equiv :
     {x : A} {y : B} (p : map-equiv e x ＝ y) →
-    ( ( ap (map-equiv e) (map-eq-transpose-equiv e p)) ∙
-      ( is-section-map-inv-equiv e y)) ＝
-    ( p)
+    coherence-triangle-identifications'
+      ( p)
+      ( is-section-map-inv-equiv e y)
+      ( ap (map-equiv e) (map-eq-transpose-equiv e p))
   triangle-eq-transpose-equiv {x} {y} p =
     ( right-whisker-concat
       ( is-section-map-inv-equiv
         ( equiv-ap e x (map-inv-equiv e y))
         ( p ∙ inv (is-section-map-inv-equiv e y)))
       ( is-section-map-inv-equiv e y)) ∙
-    ( ( assoc
-        ( p)
-        ( inv (is-section-map-inv-equiv e y))
-        ( is-section-map-inv-equiv e y)) ∙
-      ( ( left-whisker-concat p
-          ( left-inv (is-section-map-inv-equiv e y))) ∙
-        ( right-unit)))
+    ( is-section-inv-concat' (is-section-map-inv-equiv e y) p)
 
   triangle-eq-transpose-equiv-inv :
     {x : A} {y : B} (p : y ＝ map-equiv e x) →
-    ( (is-section-map-inv-equiv e y) ∙ p) ＝
-    ( ap (map-equiv e) (map-eq-transpose-equiv-inv e p))
+    coherence-triangle-identifications'
+      ( ap (map-equiv e) (map-eq-transpose-equiv-inv e p))
+      ( p)
+      ( is-section-map-inv-equiv e y)
   triangle-eq-transpose-equiv-inv {x} {y} p =
-    map-inv-equiv
-      ( equiv-ap
-        ( equiv-inv (map-equiv e (map-inv-equiv e y)) (map-equiv e x))
-        ( (is-section-map-inv-equiv e y) ∙ p)
-        ( ap (map-equiv e) (map-eq-transpose-equiv-inv e p)))
-      ( ( distributive-inv-concat (is-section-map-inv-equiv e y) p) ∙
-        ( ( inv
-            ( right-transpose-eq-concat
-              ( ap (map-equiv e) (inv (map-eq-transpose-equiv-inv e p)))
-              ( is-section-map-inv-equiv e y)
-              ( inv p)
-              ( ( right-whisker-concat
-                  ( ap
-                    ( ap (map-equiv e))
-                    ( inv-inv
-                      ( map-inv-equiv
-                        ( equiv-ap e x (map-inv-equiv e y))
-                        ( ( inv p) ∙
-                          ( inv (is-section-map-inv-equiv e y))))))
-                  ( is-section-map-inv-equiv e y)) ∙
-                ( triangle-eq-transpose-equiv (inv p))))) ∙
-          ( ap-inv (map-equiv e) (map-eq-transpose-equiv-inv e p))))
+    inv
+      ( is-section-map-inv-equiv
+        ( equiv-ap e _ _)
+        ( is-section-map-inv-equiv e y ∙ p))
 
   triangle-eq-transpose-equiv' :
     {x : A} {y : B} (p : map-equiv e x ＝ y) →
-    ( is-retraction-map-inv-equiv e x ∙ map-eq-transpose-equiv e p) ＝
-    ( ap (map-inv-equiv e) p)
+    coherence-triangle-identifications'
+      ( ap (map-inv-equiv e) p)
+      ( map-eq-transpose-equiv e p)
+      ( is-retraction-map-inv-equiv e x)
   triangle-eq-transpose-equiv' {x} refl =
     ( left-whisker-concat
       ( is-retraction-map-inv-equiv e x)
-      ( htpy-map-eq-transpose-equiv refl)) ∙
+      ( compute-map-eq-transpose-equiv e refl)) ∙
     ( is-section-inv-concat (is-retraction-map-inv-equiv e x) refl)
 
   triangle-eq-transpose-equiv-inv' :
     {x : A} {y : B} (p : y ＝ map-equiv e x) →
-    ( map-eq-transpose-equiv-inv e p) ＝
-    ( ap (map-inv-equiv e) p ∙ is-retraction-map-inv-equiv e x)
+    coherence-triangle-identifications
+      ( map-eq-transpose-equiv-inv e p)
+      ( is-retraction-map-inv-equiv e x)
+      ( ap (map-inv-equiv e) p)
   triangle-eq-transpose-equiv-inv' {x} refl =
-    inv
-      ( right-transpose-eq-concat
-        ( is-retraction-map-inv-equiv e x)
-        ( map-eq-transpose-equiv e refl)
-        ( refl)
-        ( triangle-eq-transpose-equiv' refl))
+    compute-refl-eq-transpose-equiv-inv e
 
   right-inverse-eq-transpose-equiv :
     {x : A} {y : B} (p : y ＝ map-equiv e x) →
     ( ( map-eq-transpose-equiv e (inv p)) ∙
       ( ap (map-inv-equiv e) p ∙ is-retraction-map-inv-equiv e x)) ＝
     ( refl)
-  right-inverse-eq-transpose-equiv {x} p =
-    inv
-      ( map-inv-equiv
-        ( equiv-left-transpose-eq-concat'
-          ( refl)
-          ( map-eq-transpose-equiv e (inv p))
-          ( ap (map-inv-equiv e) p ∙ is-retraction-map-inv-equiv e x))
-        ( right-unit ∙ triangle-eq-transpose-equiv-inv' p))
+  right-inverse-eq-transpose-equiv {x} refl =
+    ( right-whisker-concat (compute-refl-eq-transpose-equiv e) _) ∙
+    ( left-inv (is-retraction-map-inv-equiv e _))
+```
+
+### Transposing concatenated identifications along equivalences
+
+Transposing concatenated identifications into a triangle with a transpose of the
+left factor.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
+  where
+
+  triangle-eq-transpose-equiv-concat :
+    {x : A} {y z : B} (p : map-equiv e x ＝ y) (q : y ＝ z) →
+    ( map-eq-transpose-equiv e (p ∙ q)) ＝
+    ( map-eq-transpose-equiv e p ∙ ap (map-inv-equiv e) q)
+  triangle-eq-transpose-equiv-concat refl refl = inv right-unit
 ```