Transposing identifications along equivalences

Content created by Egbert Rijke, Fredrik Bakke and maybemabeline.

Created on 2024-02-06.
Last modified on 2024-03-02.

module foundation.transposition-identifications-along-equivalences where
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
open import foundation-core.homotopies


Consider an equivalence e : A ≃ B and two elements x : A and y : B. The transposition is an equivalence

  (e x = y) ≃ (x = e⁻¹ y)

of identity types. There are two ways of constructing this equivalence. One way uses the fact that e⁻¹ is a section of e, from which it follows that

 (e x = y) ≃ (e x = e e⁻¹ y) ≃ (x = e⁻¹ y).

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

      ap e q
  e x ------> e (e⁻¹ y)
     \       /
    p \     / is-section-map-inv-equiv e y
       \   /
        ∨ ∨

commutes. The other way uses the fact that e⁻¹ is a retraction of e, resulting in the equivalence

 (e x = y) ≃ (e⁻¹ e x = e⁻¹ y) ≃ (x = e⁻¹ y) .

These two equivalences are homotopic, as is shown below.


Transposing equalities along equivalences

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B)

  eq-transpose-equiv :
    (x : A) (y : B)  (map-equiv e x  y)  (x  map-inv-equiv e y)
  eq-transpose-equiv x y =
    ( inv-equiv (equiv-ap e x (map-inv-equiv e y))) ∘e
    ( equiv-concat'
      ( map-equiv e x)
      ( inv (is-section-map-inv-equiv e y)))

  map-eq-transpose-equiv :
    {x : A} {y : B}  map-equiv e x  y  x  map-inv-equiv e y
  map-eq-transpose-equiv {x} {y} = map-equiv (eq-transpose-equiv x y)

  map-inv-eq-transpose-equiv :
    {x : A} {y : B}  x  map-inv-equiv e y  map-equiv e x  y
  map-inv-eq-transpose-equiv {x} {y} = map-inv-equiv (eq-transpose-equiv x y)

  eq-transpose-equiv' :
    (x : A) (y : B)  (map-equiv e x  y)  (x  map-inv-equiv e y)
  eq-transpose-equiv' x y =
    ( equiv-concat
      ( inv (is-retraction-map-inv-equiv e x))
      ( map-inv-equiv e y)) ∘e
    ( equiv-ap (inv-equiv e) (map-equiv e x) y)

  map-eq-transpose-equiv' :
    {x : A} {y : B}  map-equiv e x  y  x  map-inv-equiv e y
  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.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B)

  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 =
    ( 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
  map-eq-transpose-equiv-inv {a} {b} = map-equiv (eq-transpose-equiv-inv a b)

  map-inv-eq-transpose-equiv-inv :
    {a : A} {b : B}  map-inv-equiv e b  a  b  map-equiv e a
  map-inv-eq-transpose-equiv-inv {a} {b} =
    map-inv-equiv (eq-transpose-equiv-inv a b)


Computing transposition of reflexivity along equivalences

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B)

  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 =
      ( 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} =
      ( 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.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B)

  compute-map-eq-transpose-equiv :
    {x : A} {y : B} 
    map-eq-transpose-equiv e {x} {y} ~ map-eq-transpose-equiv' e
  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)

The defining commuting triangles of transposed identifications

Transposed identifications fit in commuting triangles with the original identifications.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B)

  triangle-eq-transpose-equiv :
    {x : A} {y : B} (p : map-equiv e x  y) 
      ( 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)) 
    ( 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) 
      ( 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 =
      ( 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) 
      ( 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)
      ( 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)
      ( is-retraction-map-inv-equiv e x)
      ( ap (map-inv-equiv e) p)
  triangle-eq-transpose-equiv-inv' {x} 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} 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.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B)

  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

Recent changes