Rename inv-con and con-inv to left/right-transpose-eq-concat (#730

)

Similarly, `inv-con-htpy` and `con-inv-htpy` are renamed to
`left/right-transpose-htpy-concat`.

src/elementary-number-theory/universal-property-integers.lagda.md

@@ -167,17 +167,18 @@ abstract
             ( refl-htpy))
         ( is-contr-is-equiv'
           ( Σ (Id (pr1 s zero-ℤ) p0) (λ α → Id α (pr1 (pr2 s))))
-          ( tot (λ α → con-inv refl α (pr1 (pr2 s))))
+          ( tot (λ α → right-transpose-eq-concat refl α (pr1 (pr2 s))))
           ( is-equiv-tot-is-fiberwise-equiv
-            ( λ α → is-equiv-con-inv refl α (pr1 (pr2 s))))
+            ( λ α → is-equiv-right-transpose-eq-concat refl α (pr1 (pr2 s))))
           ( is-contr-total-path' (pr1 (pr2 s))))
         ( pair (pr1 (pr2 s)) (inv (right-inv (pr1 (pr2 s)))))
         ( is-contr-is-equiv'
           ( Σ ( ( k : ℤ) → Id (pr1 s (succ-ℤ k)) (pr1 (pS k) (pr1 s k)))
               ( λ β → β ~ (pr2 (pr2 s))))
-          ( tot (λ β → con-inv-htpy refl-htpy β (pr2 (pr2 s))))
+          ( tot (λ β → right-transpose-htpy-concat refl-htpy β (pr2 (pr2 s))))
           ( is-equiv-tot-is-fiberwise-equiv
-            ( λ β → is-equiv-con-inv-htpy refl-htpy β (pr2 (pr2 s))))
+            ( λ β →
+              is-equiv-right-transpose-htpy-concat refl-htpy β (pr2 (pr2 s))))
           ( is-contr-total-htpy' (pr2 (pr2 s)))))
 
 abstract

src/foundation-core/coherently-invertible-maps.lagda.md

@@ -117,7 +117,7 @@ module _
       ( f ·l is-retraction-inv-has-inverse H)
     coherence-inv-has-inverse H x =
       inv
-        ( inv-con
+        ( left-transpose-eq-concat
           ( pr1 (pr2 H) (f (inv-has-inverse H (f x))))
           ( ap f (pr2 (pr2 H) x))
           ( ( ap f (pr2 (pr2 H) (inv-has-inverse H (f x)))) ∙

src/foundation-core/equivalences.lagda.md

@@ -569,7 +569,7 @@ module _
                 ( inv (ap-comp f (map-inv-is-equiv H) p))
                 ( inv (coherence-map-inv-is-equiv H y))))) ∙
           ( inv
-            ( inv-con
+            ( left-transpose-eq-concat
               ( ap f (is-retraction-map-inv-is-equiv H x))
               ( p)
               ( ( ap (f ∘ map-inv-is-equiv H) p) ∙

src/foundation-core/homotopies.lagda.md

@@ -191,17 +191,19 @@ module _
   (H : f ~ g) (K : g ~ h) (L : f ~ h) (M : (H ∙h K) ~ L)
   where
 
-  inv-con-htpy : K ~ ((inv-htpy H) ∙h L)
-  inv-con-htpy x = inv-con (H x) (K x) (L x) (M x)
+  left-transpose-htpy-concat : K ~ ((inv-htpy H) ∙h L)
+  left-transpose-htpy-concat x =
+    left-transpose-eq-concat (H x) (K x) (L x) (M x)
 
-  inv-htpy-inv-con-htpy : ((inv-htpy H) ∙h L) ~ K
-  inv-htpy-inv-con-htpy = inv-htpy inv-con-htpy
+  inv-htpy-left-transpose-htpy-concat : ((inv-htpy H) ∙h L) ~ K
+  inv-htpy-left-transpose-htpy-concat = inv-htpy left-transpose-htpy-concat
 
-  con-inv-htpy : H ~ (L ∙h (inv-htpy K))
-  con-inv-htpy x = con-inv (H x) (K x) (L x) (M x)
+  right-transpose-htpy-concat : H ~ (L ∙h (inv-htpy K))
+  right-transpose-htpy-concat x =
+    right-transpose-eq-concat (H x) (K x) (L x) (M x)
 
-  inv-htpy-con-inv-htpy : (L ∙h (inv-htpy K)) ~ H
-  inv-htpy-con-inv-htpy = inv-htpy con-inv-htpy
+  inv-htpy-right-transpose-htpy-concat : (L ∙h (inv-htpy K)) ~ H
+  inv-htpy-right-transpose-htpy-concat = inv-htpy right-transpose-htpy-concat
 ```
 
 ### Associativity of concatenation of homotopies

src/foundation-core/identity-types.lagda.md

@@ -176,18 +176,19 @@ module _
 ### Transposing inverses
 
 ```agda
-inv-con :
+left-transpose-eq-concat :
   {l : Level} {A : UU l} {x y : A} (p : x ＝ y) {z : A} (q : y ＝ z)
   (r : x ＝ z) → ((p ∙ q) ＝ r) → q ＝ ((inv p) ∙ r)
-inv-con refl q r s = s
+left-transpose-eq-concat refl q r s = s
 
-con-inv :
+right-transpose-eq-concat :
   {l : Level} {A : UU l} {x y : A} (p : x ＝ y) {z : A} (q : y ＝ z)
   (r : x ＝ z) → ((p ∙ q) ＝ r) → p ＝ (r ∙ (inv q))
-con-inv p refl r s = ((inv right-unit) ∙ s) ∙ (inv right-unit)
+right-transpose-eq-concat p refl r s = ((inv right-unit) ∙ s) ∙ (inv right-unit)
 ```
 
-The fact that `inv-con` and `con-inv` are equivalences is recorded in
+The fact that `left-transpose-eq-concat` and `right-transpose-eq-concat` are
+equivalences is recorded in
 [`foundation.identity-types`](foundation.identity-types.md).
 
 ### Concatenation is injective

src/foundation/commuting-cubes-of-maps.lagda.md

@@ -69,13 +69,13 @@ coherence-htpy-parallel-cone-coherence-cube-maps
       ( inv-htpy (h ·l back-left))
       ( _)
       ( left-whisk-inv-htpy h back-left)) ∙h
-    ( inv-htpy-inv-con-htpy (h ·l back-left) _ _
+    ( inv-htpy-left-transpose-htpy-concat (h ·l back-left) _ _
       ( ( (inv-htpy-assoc-htpy (h ·l back-left) (front-left ·r f') _) ∙h
           ( ( inv-htpy-assoc-htpy
               ( (h ·l back-left) ∙h (front-left ·r f'))
               ( hD ·l top)
               ( (inv-htpy front-right) ·r g')) ∙h
-            ( inv-htpy-con-inv-htpy _ (front-right ·r g') _
+            ( inv-htpy-right-transpose-htpy-concat _ (front-right ·r g') _
               ( (assoc-htpy (bottom ·r hA) _ _) ∙h (inv-htpy c))))) ∙h
         ( ap-concat-htpy (bottom ·r hA) _ _ inv-htpy-right-unit-htpy))))
 ```

src/foundation/equivalences.lagda.md

@@ -125,7 +125,7 @@ module _
         ( ap (map-equiv e) (map-eq-transpose-equiv' p)))
       ( ( distributive-inv-concat (is-section-map-inv-equiv e y) p) ∙
         ( ( inv
-            ( con-inv
+            ( right-transpose-eq-concat
               ( ap (map-equiv e) (inv (map-eq-transpose-equiv' p)))
               ( is-section-map-inv-equiv e y)
               ( inv p)

src/foundation/homotopies.lagda.md

@@ -203,19 +203,24 @@ module _
   (H : f ~ g) (K : g ~ h) (L : f ~ h)
   where
 
-  is-equiv-inv-con-htpy : is-equiv (inv-con-htpy H K L)
-  is-equiv-inv-con-htpy =
-    is-equiv-map-Π _ (λ x → is-equiv-inv-con (H x) (K x) (L x))
-
-  equiv-inv-con-htpy : ((H ∙h K) ~ L) ≃ (K ~ ((inv-htpy H) ∙h L))
-  equiv-inv-con-htpy = pair (inv-con-htpy H K L) is-equiv-inv-con-htpy
-
-  is-equiv-con-inv-htpy : is-equiv (con-inv-htpy H K L)
-  is-equiv-con-inv-htpy =
-    is-equiv-map-Π _ (λ x → is-equiv-con-inv (H x) (K x) (L x))
-
-  equiv-con-inv-htpy : ((H ∙h K) ~ L) ≃ (H ~ (L ∙h (inv-htpy K)))
-  equiv-con-inv-htpy = pair (con-inv-htpy H K L) is-equiv-con-inv-htpy
+  is-equiv-left-transpose-htpy-concat :
+    is-equiv (left-transpose-htpy-concat H K L)
+  is-equiv-left-transpose-htpy-concat =
+    is-equiv-map-Π _ (λ x → is-equiv-left-transpose-eq-concat (H x) (K x) (L x))
+
+  equiv-left-transpose-htpy-concat : ((H ∙h K) ~ L) ≃ (K ~ ((inv-htpy H) ∙h L))
+  equiv-left-transpose-htpy-concat =
+    pair (left-transpose-htpy-concat H K L) is-equiv-left-transpose-htpy-concat
+
+  is-equiv-right-transpose-htpy-concat :
+    is-equiv (right-transpose-htpy-concat H K L)
+  is-equiv-right-transpose-htpy-concat =
+    is-equiv-map-Π _
+      ( λ x → is-equiv-right-transpose-eq-concat (H x) (K x) (L x))
+
+  equiv-right-transpose-htpy-concat : ((H ∙h K) ~ L) ≃ (H ~ (L ∙h (inv-htpy K)))
+  pr1 equiv-right-transpose-htpy-concat = right-transpose-htpy-concat H K L
+  pr2 equiv-right-transpose-htpy-concat = is-equiv-right-transpose-htpy-concat
 ```
 
 ### Computing dependent-identifications in the type family `eq-value` of dependent functions

src/foundation/identity-types.lagda.md

@@ -215,31 +215,35 @@ module _
   where
 
   abstract
-    is-equiv-inv-con :
-      (p : x ＝ y) (q : y ＝ z) (r : x ＝ z) → is-equiv (inv-con p q r)
-    is-equiv-inv-con refl q r = is-equiv-id
+    is-equiv-left-transpose-eq-concat :
+      (p : x ＝ y) (q : y ＝ z) (r : x ＝ z) →
+      is-equiv (left-transpose-eq-concat p q r)
+    is-equiv-left-transpose-eq-concat refl q r = is-equiv-id
 
-  equiv-inv-con :
+  equiv-left-transpose-eq-concat :
     (p : x ＝ y) (q : y ＝ z) (r : x ＝ z) →
     ((p ∙ q) ＝ r) ≃ (q ＝ ((inv p) ∙ r))
-  pr1 (equiv-inv-con p q r) = inv-con p q r
-  pr2 (equiv-inv-con p q r) = is-equiv-inv-con p q r
+  pr1 (equiv-left-transpose-eq-concat p q r) = left-transpose-eq-concat p q r
+  pr2 (equiv-left-transpose-eq-concat p q r) =
+    is-equiv-left-transpose-eq-concat p q r
 
   abstract
-    is-equiv-con-inv :
-      (p : x ＝ y) (q : y ＝ z) (r : x ＝ z) → is-equiv (con-inv p q r)
-    is-equiv-con-inv p refl r =
+    is-equiv-right-transpose-eq-concat :
+      (p : x ＝ y) (q : y ＝ z) (r : x ＝ z) →
+      is-equiv (right-transpose-eq-concat p q r)
+    is-equiv-right-transpose-eq-concat p refl r =
       is-equiv-comp
         ( concat' p (inv right-unit))
         ( concat (inv right-unit) r)
         ( is-equiv-concat (inv right-unit) r)
         ( is-equiv-concat' p (inv right-unit))
 
-  equiv-con-inv :
+  equiv-right-transpose-eq-concat :
     (p : x ＝ y) (q : y ＝ z) (r : x ＝ z) →
     ((p ∙ q) ＝ r) ≃ (p ＝ (r ∙ (inv q)))
-  pr1 (equiv-con-inv p q r) = con-inv p q r
-  pr2 (equiv-con-inv p q r) = is-equiv-con-inv p q r
+  pr1 (equiv-right-transpose-eq-concat p q r) = right-transpose-eq-concat p q r
+  pr2 (equiv-right-transpose-eq-concat p q r) =
+    is-equiv-right-transpose-eq-concat p q r
 ```
 
 ### Computing transport in the type family of identifications with a fixed target

src/foundation/pullbacks.lagda.md

@@ -270,7 +270,7 @@ module _
             ( (Hf (p' z)) ∙ (H' z))
             ( inv (Hg (q' z))))) ∙
         ( inv
-          ( con-inv
+          ( right-transpose-eq-concat
             ( (H z) ∙ (ap g (Hq z)))
             ( Hg (q' z))
             ( ( ap f (Hp z)) ∙ ((Hf (p' z)) ∙ (H' z)))

src/foundation/unital-binary-operations.lagda.md

@@ -79,7 +79,7 @@ module _
   pr1 (pr2 (coherent-unit-laws-unit-laws (pair H K))) x =
     ( inv (ap (μ x) (K e))) ∙ (( ap (μ x) (H e)) ∙ (K x))
   pr2 (pr2 (coherent-unit-laws-unit-laws (pair H K))) =
-    inv-con
+    left-transpose-eq-concat
       ( ap (μ e) (K e))
       ( H e)
       ( (ap (μ e) (H e)) ∙ (K e))

src/structured-types/initial-pointed-type-equipped-with-automorphism.lagda.md

@@ -147,7 +147,7 @@ coh-aut-htpy-map-ℤ-Pointed-Type-With-Aut :
       ℤ-Pointed-Type-With-Aut X h k))
 coh-aut-htpy-map-ℤ-Pointed-Type-With-Aut X h (inl zero-ℕ) =
   inv
-    ( inv-con
+    ( left-transpose-eq-concat
       ( is-section-map-inv-equiv
         ( aut-Pointed-Type-With-Aut X)
         ( point-Pointed-Type-With-Aut X))
@@ -166,7 +166,7 @@ coh-aut-htpy-map-ℤ-Pointed-Type-With-Aut X h (inl zero-ℕ) =
             ℤ-Pointed-Type-With-Aut X h neg-one-ℤ))))
 coh-aut-htpy-map-ℤ-Pointed-Type-With-Aut X h (inl (succ-ℕ k)) =
   inv
-    ( inv-con
+    ( left-transpose-eq-concat
       ( is-section-map-inv-equiv
         ( aut-Pointed-Type-With-Aut X)
         ( map-ℤ-Pointed-Type-With-Aut X (inl k)))

src/structured-types/pointed-equivalences.lagda.md

@@ -199,7 +199,7 @@ module _
             ( inv (preserves-point-pointed-map f))))
         ( equiv-tot
           ( λ p →
-            ( ( equiv-con-inv
+            ( ( equiv-right-transpose-eq-concat
                 ( ap (map-pointed-map f) p)
                 ( preserves-point-pointed-map f)
                 ( is-section-map-inv-is-equiv H (point-Pointed-Type B))) ∘e

src/structured-types/pointed-homotopies.lagda.md

@@ -62,8 +62,12 @@ module _
       ( refl-htpy)
       ( inv (right-inv (preserves-point-function-pointed-Π f)))
       ( λ g → equiv-funext)
-      ( λ p → equiv-con-inv refl p (preserves-point-function-pointed-Π f) ∘e
-              equiv-inv (preserves-point-function-pointed-Π f) p)
+      ( λ p →
+        ( equiv-right-transpose-eq-concat
+          ( refl)
+          ( p)
+          ( preserves-point-function-pointed-Π f)) ∘e
+        ( equiv-inv (preserves-point-function-pointed-Π f) p))
 
   eq-htpy-pointed-Π :
     (g : pointed-Π A B) → (htpy-pointed-Π g) → Id f g

src/synthetic-homotopy-theory/26-descent.lagda.md

@@ -101,7 +101,7 @@ pullback-property-dependent-pullback-property-pushout
         ( λ h → right-unit ∙
           ( ( ap eq-htpy
               ( eq-htpy (λ s →
-                inv-con
+                left-transpose-eq-concat
                   ( tr-constant-type-family (H s) (h (i (f s))))
                   ( ap h (H s))
                   ( apd h (H s))

src/synthetic-homotopy-theory/multiplication-circle.lagda.md

@@ -77,7 +77,12 @@ dependent-identification-Mul-Π-𝕊¹ {x} refl q r H u =
   eq-htpy-pointed-map
     ( q)
     ( r)
-    ( pair H (con-inv (H base-𝕊¹) (pr2 r) (pr2 q) (inv (inv right-unit ∙ u))))
+    ( ( H) ,
+      (right-transpose-eq-concat
+        ( H base-𝕊¹)
+        ( pr2 r)
+        ( pr2 q)
+        ( inv (inv right-unit ∙ u))))
 
 eq-id-id-𝕊¹-Pointed-Type :
   Id (tr Mul-Π-𝕊¹ loop-𝕊¹ id-pointed-map) id-pointed-map

src/synthetic-homotopy-theory/pushouts.lagda.md

@@ -196,7 +196,7 @@ module _
     ( ( compute-inl-cogap (f s) ∙ coherence-square-cocone f g c s) ∙
       ( inv (compute-inr-cogap (g s))))
   compute-glue-cogap s =
-    con-inv
+    right-transpose-eq-concat
       ( ap (cogap f g c) (glue-pushout f g s))
       ( compute-inr-cogap (g s))
       ( compute-inl-cogap (f s) ∙ coherence-square-cocone f g c s)

src/synthetic-homotopy-theory/universal-cover-circle.lagda.md

@@ -321,7 +321,7 @@ map-dependent-identification-contraction-total-space'
           ( is-equiv-map-equiv (equiv-contraction-total-space c x e))
           ( h))) ∙
       ( ( eq-htpy
-          ( con-inv-htpy h
+          ( right-transpose-htpy-concat h
             ( segment-Σ refl f e e' H)
             ( precomp-Π
               ( map-equiv f)
@@ -350,7 +350,7 @@ equiv-dependent-identification-contraction-total-space' :
 equiv-dependent-identification-contraction-total-space'
   c {x} {.x} refl f e e' H h h' =
   ( inv-equiv
-    ( equiv-con-inv-htpy h
+    ( equiv-right-transpose-htpy-concat h
       ( segment-Σ refl f e e' H)
       ( precomp-Π
         ( map-equiv f)