\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module UF-Retracts where

open import SpartanMLTT
open import UF-Base
open import UF-Subsingletons
open import AlternativePlus

has-section : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
has-section r = Ξ£ s κž‰ (codomain r β†’ domain r), r ∘ s ∼ id

is-section : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
is-section s = Ξ£ r κž‰ (codomain s β†’ domain s), r ∘ s ∼ id

sections-are-lc : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (s : X β†’ Y)
                β†’ is-section s β†’ left-cancellable s
sections-are-lc s (r , rs) {x} {x'} p = (rs x)⁻¹ βˆ™ ap r p βˆ™ rs x'

retract_of_ : 𝓀 Μ‡ β†’ π“₯ Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡
retract Y of X = Ξ£ r κž‰ (X β†’ Y) , has-section r

retraction : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ retract X of Y β†’ (Y β†’ X)
retraction (r , s , rs) = r

section : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ retract X of Y β†’ (X β†’ Y)
section (r , s , rs) = s

retract-condition : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (ρ : retract X of Y)
                  β†’ retraction ρ ∘ section ρ ∼ id
retract-condition (r , s , rs) = rs

retraction-has-section : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (ρ : retract X of Y)
                       β†’ has-section (retraction ρ)
retraction-has-section (r , h) = h

retract-of-singleton : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                     β†’ retract Y of X
                     β†’ is-singleton X
                     β†’ is-singleton Y
retract-of-singleton (r , s , rs) (c , Ο†) = r c , (Ξ» y β†’ ap r (Ο† (s y)) βˆ™ rs y)

retract-of-prop : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                β†’ retract Y of X
                β†’ is-prop X
                β†’ is-prop Y
retract-of-prop (r , s , rs) = subtype-of-prop-is-prop s (sections-are-lc s (r , rs))

Ξ£-is-set : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
         β†’ is-set X
         β†’ ((x : X) β†’ is-set (A x))
         β†’ is-set (Ξ£ A)
Ξ£-is-set {𝓀} {π“₯} {X} {A} i j {Οƒ} {Ο„} = Ξ³
 where
  S = Ξ£ p κž‰ pr₁ Οƒ ≑ pr₁ Ο„ , transport A p (prβ‚‚ Οƒ) ≑ prβ‚‚ Ο„

  a : is-prop S
  a = Ξ£-is-prop i (Ξ» p β†’ j (pr₁ Ο„))

  b : retract (Οƒ ≑ Ο„) of S
  b = to-Ξ£-≑ , from-Ξ£-≑ , tofrom-Ξ£-≑

  Ξ³ : is-prop (Οƒ ≑ Ο„)
  Ξ³ = retract-of-prop b a

identity-retraction : {X : 𝓀 Μ‡ } β†’ retract X of X
identity-retraction = id , id , Ξ» x β†’ refl

has-section-closed-under-∼ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f g : X β†’ Y)
                           β†’ has-section f
                           β†’ g ∼ f
                           β†’ has-section g
has-section-closed-under-∼ {𝓀} {π“₯} {X} {Y} f g (s , fs) h =
 (s , Ξ» y β†’ g (s y) β‰‘βŸ¨ h (s y) ⟩ f (s y) β‰‘βŸ¨ fs y ⟩ y ∎)

has-section-closed-under-∼' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {f g : X β†’ Y}
                            β†’ has-section f
                            β†’ f ∼ g
                            β†’ has-section g
has-section-closed-under-∼' ise h = has-section-closed-under-∼ _ _ ise (Ξ» x β†’ (h x)⁻¹)

is-section-closed-under-∼ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f g : X β†’ Y)
                          β†’ is-section f
                          β†’  g ∼ f
                          β†’ is-section g
is-section-closed-under-∼ {𝓀} {π“₯} {X} {Y} f g (r , rf) h =
  (r , Ξ» x β†’ r (g x) β‰‘βŸ¨ ap r (h x) ⟩
             r (f x) β‰‘βŸ¨ rf x ⟩
             x       ∎)

is-section-closed-under-∼' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {f g : X β†’ Y}
                           β†’ is-section f
                           β†’ f ∼ g
                           β†’ is-section g
is-section-closed-under-∼' ise h = is-section-closed-under-∼ _ _ ise (Ξ» x β†’ (h x)⁻¹)

\end{code}

Surjection expressed in Curry-Howard logic amounts to retraction.

\begin{code}

has-section' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
has-section' f = (y : codomain f) β†’ Ξ£ x κž‰ domain f , f x ≑ y

retract_Of_ : 𝓀 Μ‡ β†’ π“₯ Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡
retract Y Of X = Ξ£ f κž‰ (X β†’ Y) , has-section' f

retract-of-retract-Of : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ retract Y of X β†’ retract Y Of X
retract-of-retract-Of {𝓀} {π“₯} {X} {Y} ρ = (retraction ρ , hass)
 where
  hass : (y : Y) β†’ Ξ£ x κž‰ X , retraction ρ x ≑ y
  hass y = section ρ y , retract-condition ρ y

retract-Of-retract-of : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ retract Y Of X β†’ retract Y of X
retract-Of-retract-of {𝓀} {π“₯} {X} {Y} (f , hass) = (f , Ο†)
 where
  Ο† : Ξ£ s κž‰ (Y β†’ X) , f ∘ s ∼ id
  Ο† = (Ξ» y β†’ pr₁ (hass y)) , (Ξ» y β†’ prβ‚‚ (hass y))

retracts-compose : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
                 β†’ retract Y of X
                 β†’ retract Z of Y
                 β†’ retract Z of X
retracts-compose (r , s , rs) (r' , s' , rs') =
  r' ∘ r , s ∘ s' , Ξ» z β†’ r' (r (s (s' z))) β‰‘βŸ¨ ap r' (rs (s' z)) ⟩
                          r' (s' z)         β‰‘βŸ¨ rs' z ⟩
                          z                 ∎

Γ—-retract : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ } {B : 𝓣 Μ‡ }
          β†’ retract X of A
          β†’ retract Y of B
          β†’ retract (X Γ— Y) of (A Γ— B)
Γ—-retract {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} {A} {B} (r , s , rs) (t , u , tu) = f , g , fg
 where
  f : A Γ— B β†’ X Γ— Y
  f (a , b) = (r a , t b)

  g : X Γ— Y β†’ A Γ— B
  g (x , y) = s x , u y

  fg : (z : X Γ— Y) β†’ f (g z) ≑ z
  fg (x , y) = to-Γ—-≑ (rs x) (tu y)

+-retract : {X : 𝓀 Μ‡ } {Y : 𝓦 Μ‡ } {A : π“₯ Μ‡ } {B : 𝓣 Μ‡ }
          β†’ retract X of A
          β†’ retract Y of B
          β†’ retract (X + Y) of (A + B)
+-retract {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} {A} {B} (r , s , rs) (t , u , tu) = f , g , fg
 where
  f : A + B β†’ X + Y
  f (inl a) = inl (r a)
  f (inr b) = inr (t b)

  g : X + Y β†’ A + B
  g (inl x) = inl (s x)
  g (inr y) = inr (u y)

  fg : (p : X + Y) β†’ f (g p) ≑ p
  fg (inl x) = ap inl (rs x)
  fg (inr y) = ap inr (tu y)

+'-retract-of-+ : {X Y : 𝓀 Μ‡ }
                β†’ retract (X +' Y) of (X + Y)
+'-retract-of-+ {𝓀} {X} {Y} = f , g , fg
 where
  f : X + Y β†’ X +' Y
  f (inl x) = β‚€ , x
  f (inr y) = ₁ , y

  g : X +' Y β†’ X + Y
  g (β‚€ , x) = inl x
  g (₁ , y) = inr y

  fg : (z : X +' Y) β†’ f (g z) ≑ z
  fg (β‚€ , x) = refl
  fg (₁ , y) = refl

+'-retract : {X Y : 𝓀 Μ‡ } {A B : π“₯ Μ‡ }
           β†’ retract X of A
           β†’ retract Y of B
           β†’ retract (X +' Y) of (A +' B)
+'-retract {𝓀} {π“₯} {X} {Y} {A} {B} (r , s , rs) (t , u , tu) = f , g , fg
 where
  f : A +' B β†’ X +' Y
  f (β‚€ , a) = β‚€ , r a
  f (₁ , b) = ₁ , t b

  g : X +' Y β†’ A +' B
  g (β‚€ , x) = β‚€ , s x
  g (₁ , y) = ₁ , u y

  fg : (p : X +' Y) β†’ f (g p) ≑ p
  fg (β‚€ , x) = ap (Ξ» - β†’ (β‚€ , -)) (rs x)
  fg (₁ , y) = ap (Ξ» - β†’ (₁ , -)) (tu y)

Ξ£-reindex-retract : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : X β†’ 𝓦 Μ‡ } (r : Y β†’ X)
                  β†’ has-section r β†’ retract (Ξ£ A) of (Ξ£ (A ∘ r))
Ξ£-reindex-retract {𝓀} {π“₯} {𝓦} {X} {Y} {A} r (s , rs) = Ξ³ , Ο† , Ξ³Ο†
 where
  Ξ³ : (Ξ£ y κž‰ Y , A (r y)) β†’ Ξ£ A
  Ξ³ (y , a) = (r y , a)

  Ο† : Ξ£ A β†’ Ξ£ y κž‰ Y , A (r y)
  Ο† (x , a) = (s x , back-transport A (rs x) a)

  Ξ³Ο† : (Οƒ : Ξ£ A) β†’ Ξ³ (Ο† Οƒ) ≑ Οƒ
  Ξ³Ο† (x , a) = to-Ξ£-≑ (rs x , p)
   where
    p : transport A (rs x) (back-transport A (rs x) a) ≑ a
    p = back-and-forth-transport (rs x)

Ξ£-retract : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ )
          β†’ ((x : X) β†’ retract (A x) of (B x))
          β†’ retract (Ξ£ A) of (Ξ£ B)
Ξ£-retract {𝓀} {π“₯} {𝓦} {X} A B ρ = NatΞ£ R , NatΞ£ S , rs
 where
  R : (x : X) β†’ B x β†’ A x
  R x = retraction (ρ x)

  S : (x : X) β†’ A x β†’ B x
  S x = section (ρ x)

  RS : (x : X) (a : A x) β†’ R x (S x a) ≑ a
  RS x = retract-condition (ρ x)

  rs : (Οƒ : Ξ£ A) β†’ NatΞ£ R (NatΞ£ S Οƒ) ≑ Οƒ
  rs (x , a) = to-Ξ£-≑' (RS x a)

retract-πŸ™+πŸ™-of-𝟚 : retract πŸ™ + πŸ™ of 𝟚
retract-πŸ™+πŸ™-of-𝟚 = f , (g , fg)
 where
  f : 𝟚 β†’ πŸ™ {𝓀₀} + πŸ™ {𝓀₀}
  f = 𝟚-cases (inl *) (inr *)

  g : πŸ™ + πŸ™ β†’ 𝟚
  g = cases (Ξ» x β†’ β‚€) (Ξ» x β†’ ₁)

  fg : (x : πŸ™ + πŸ™) β†’ f (g x) ≑ x
  fg (inl *) = refl
  fg (inr *) = refl

\end{code}

TODO. Several retractions here are actually equivalences. So some code
should be generalized and moved to an equivalences module. Similarly,
some retracts proved here are also shown as equivalences in other
modules, and hence there is some amount of repetition that should be
removed. This is the result of (1) merging initially independent
developments, and (2) work over many years with uncontrolled growth.

\begin{code}

Ξ£-retractβ‚‚ : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {A : 𝓦 Μ‡ } {B : 𝓣 Μ‡ }
           β†’ retract X of A
           β†’ ((x : X) β†’ retract  (Y x) of B)
           β†’ retract (Ξ£ Y) of (A Γ— B)
Ξ£-retractβ‚‚ {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} {A} {B} (r , s , rs) R = f , g , gf
 where
  Ο† : (x : X) β†’ B β†’ Y x
  Ο† x = retraction (R x)

  Ξ³ : (x : X) β†’ Y x β†’ B
  Ξ³ x = section (R x)

  φγ : (x : X) β†’ (y : Y x) β†’ Ο† x (Ξ³ x y) ≑ y
  φγ x = retract-condition (R x)

  f : A Γ— B β†’ Ξ£ Y
  f (a , b) = r a , Ο† (r a) b

  g : Ξ£ Y β†’ A Γ— B
  g (x , y) = s x , Ξ³ x y

  gf : (z : Ξ£ Y) β†’ f (g z) ≑ z
  gf (x , y) = to-Ξ£-≑ (rs x , l (rs x))
   where
    l : {x' : X} (p : x' ≑ x) β†’ transport Y p (Ο† x' (Ξ³ x y)) ≑ y
    l refl = φγ x y

retract-πŸ™+πŸ™-of-β„• : retract πŸ™ + πŸ™ of β„•
retract-πŸ™+πŸ™-of-β„• = r , s , rs
 where
  r : β„• β†’ πŸ™ + πŸ™
  r zero = inl *
  r (succ _) = inr *

  s : πŸ™ + πŸ™ β†’ β„•
  s (inl *) = zero
  s (inr *) = succ zero

  rs : (z : πŸ™ {𝓀₀} + πŸ™ {𝓀₀}) β†’ r (s z) ≑ z
  rs (inl *) = refl
  rs (inr *) = refl

\end{code}

Added 5th March 2019. Notation for composing retracts. I should have
added this ages ago to make the above proofs more readable.

\begin{code}

_◁_ : 𝓀 Μ‡ β†’ π“₯ Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡
Y ◁ X = retract Y of X

_β—βŸ¨_⟩_ : (X : 𝓀 Μ‡ ) {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } β†’ X ◁ Y β†’ Y ◁ Z β†’ X ◁ Z
_ β—βŸ¨ d ⟩ e = retracts-compose e d

◁-refl : (X : 𝓀 Μ‡ ) β†’ X ◁ X
◁-refl X = identity-retraction {universe-of X} {X}


_β—€ : (X : 𝓀 Μ‡ ) β†’ X ◁ X
_β—€ = ◁-refl

\end{code}

Fixities:

\begin{code}

infix  0 _◁_
infix  1 _β—€
infixr 0 _β—βŸ¨_⟩_

\end{code}

Added 20 February 2020 by Tom de Jong.

\begin{code}

ap-of-section-is-section : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (s : X β†’ Y)
                         β†’ is-section s
                         β†’ (x x' : X) β†’ is-section (ap s {x} {x'})
ap-of-section-is-section {𝓀} {π“₯} {X} {Y} s (r , rs) x x' = ρ , ρap
 where
  ρ : s x ≑ s x' β†’ x ≑ x'
  ρ q = x        β‰‘βŸ¨ (rs x) ⁻¹ ⟩
        r (s x)  β‰‘βŸ¨ ap r q ⟩
        r (s x') β‰‘βŸ¨ rs x' ⟩
        x'       ∎

  ρap : (p : x ≑ x') β†’ ρ (ap s p) ≑ p
  ρap p = ρ (ap s p)                          β‰‘βŸ¨ by-definition ⟩
          (rs x) ⁻¹ βˆ™ (ap r (ap s p) βˆ™ rs x') β‰‘βŸ¨ i ⟩
          (rs x) ⁻¹ βˆ™ ap r (ap s p) βˆ™ rs x'   β‰‘βŸ¨ ii ⟩
          (rs x) ⁻¹ βˆ™ ap (r ∘ s) p βˆ™  rs x'   β‰‘βŸ¨ iii ⟩
          ap id p                             β‰‘βŸ¨ (ap-id-is-id' p)⁻¹ ⟩
          p                                   ∎
   where
    i   = βˆ™assoc ((rs x) ⁻¹) (ap r (ap s p)) (rs x') ⁻¹
    ii  = ap (Ξ» - β†’ (rs x) ⁻¹ βˆ™ - βˆ™ rs x') (ap-ap s r p)
    iii = homotopies-are-natural'' (r ∘ s) id rs {x} {x'} {p}

\end{code}

I would phrase this in terms of fibers, but fiber is defined in UF-Equiv which
imports this file.

\begin{code}

Ξ£-section-retract : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (ρ : Y ◁ Z) (g : X β†’ Y)
                  β†’ (y : Y)
                  β†’ (Ξ£ x κž‰ X , g x ≑ y)
                  ◁ (Ξ£ x κž‰ X , section ρ (g x) ≑ section ρ y)
Ξ£-section-retract {𝓀} {π“₯} {𝓦} {X} {Y} {Z} (r , s , rs) g y =
 Ξ£-retract (Ξ» x β†’ g x ≑ y) (Ξ» x β†’ s (g x) ≑ s y) Ξ³
  where
   Ξ³ : (x : X) β†’ (g x ≑ y) ◁ (s (g x) ≑ s y)
   Ξ³ x = ρ , (Οƒ , ρσ)
    where
     Οƒ : g x ≑ y β†’ s (g x) ≑ s y
     Οƒ = ap s

     ρ : s (g x) ≑ s y β†’ g x ≑ y
     ρ = pr₁ (ap-of-section-is-section s (r , rs) (g x) y)

     ρσ : (p : g x ≑ y) β†’ ρ (Οƒ p) ≑ p
     ρσ = prβ‚‚ (ap-of-section-is-section s ((r , rs)) (g x) y)

\end{code}