# Transposing identifications along retractions

Content created by Egbert Rijke and maybemabeline.

Created on 2024-02-23.

module foundation.transposition-identifications-along-retractions where

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.retractions


## Idea

Consider a map f : A → B and a map g : B → A in the converse direction. Then there is an equivalence

  is-retraction f g ≃ ((x : A) (y : B) → (f x ＝ y) ≃ (x ＝ g y))


In other words, any retracting homotopy g ∘ f ~ id induces a unique family of transposition maps

  f x ＝ y → x ＝ g y


indexed by x : A and y : B.

## Definitions

### Transposing identifications along retractions

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A)
where

eq-transpose-is-retraction :
is-retraction f g → {x : B} {y : A} → x ＝ f y → g x ＝ y
eq-transpose-is-retraction H {x} {y} p = ap g p ∙ H y

eq-transpose-is-retraction' :
is-retraction f g → {x : A} {y : B} → f x ＝ y → x ＝ g y
eq-transpose-is-retraction' H {x} refl = inv (H x)


## Properties

### The map that assings to each retracting homotopy a family of transposition functions of identifications is an equivalence

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A)
where

is-retraction-eq-transpose :
({x : B} {y : A} → x ＝ f y → g x ＝ y) → is-retraction f g
is-retraction-eq-transpose H x = H refl

is-retraction-eq-transpose' :
({x : A} {y : B} → f x ＝ y → x ＝ g y) → is-retraction f g
is-retraction-eq-transpose' H x = inv (H refl)

is-retraction-is-retraction-eq-transpose :
is-retraction-eq-transpose ∘ eq-transpose-is-retraction f g ~ id
is-retraction-is-retraction-eq-transpose H = refl

htpy-is-section-is-retraction-eq-transpose :
(H : {x : B} {y : A} → x ＝ f y → g x ＝ y)
(x : B) (y : A) →
eq-transpose-is-retraction f g (is-retraction-eq-transpose H) {x} {y} ~
H {x} {y}
htpy-is-section-is-retraction-eq-transpose H x y refl = refl

abstract
is-section-is-retraction-eq-transpose :
eq-transpose-is-retraction f g ∘ is-retraction-eq-transpose ~ id
is-section-is-retraction-eq-transpose H =
eq-htpy-implicit
( λ x →
eq-htpy-implicit
( λ y → eq-htpy (htpy-is-section-is-retraction-eq-transpose H x y)))

is-equiv-eq-transpose-is-retraction :
is-equiv (eq-transpose-is-retraction f g)
is-equiv-eq-transpose-is-retraction =
is-equiv-is-invertible
( is-retraction-eq-transpose)
( is-section-is-retraction-eq-transpose)
( is-retraction-is-retraction-eq-transpose)

equiv-eq-transpose-is-retraction :
is-retraction f g ≃ ({x : B} {y : A} → x ＝ f y → g x ＝ y)
equiv-eq-transpose-is-retraction =
( eq-transpose-is-retraction f g , is-equiv-eq-transpose-is-retraction)