\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 β†’ r ∘ s ∼ id

is-section : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
is-section s = Ξ£ \r β†’ 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

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-a-prop s
                                        (sections-are-lc s (r , rs))

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 β†’ Ξ£ \x β†’ 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' , p
 where
  p = Ξ» 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

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

\end{code}

Fixities:

\begin{code}

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

\end{code}