Martin Escardo 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes

 https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/HoTT-UF-Agda.html
 https://github.com/martinescardo/HoTT-UF.Agda-Lecture-Notes

\begin{code}

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

module MGS.Retracts where

open import MGS.hlevels public

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

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

retraction : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X ◁ Y β†’ Y β†’ X
retraction (r , s , Ξ·) = r

section : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X ◁ Y β†’ X β†’ Y
section (r , s , Ξ·) = s

retract-equation : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (ρ : X ◁ Y)
                 β†’ retraction ρ ∘ section ρ ∼ 𝑖𝑑 X

retract-equation (r , s , Ξ·) = Ξ·

retraction-has-section : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (ρ : X ◁ Y)
                       β†’ has-section (retraction ρ)

retraction-has-section (r , h) = h

id-◁ : (X : 𝓀 Μ‡ ) β†’ X ◁ X
id-◁ X = 𝑖𝑑 X , 𝑖𝑑 X , refl

_β—βˆ˜_ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } β†’ X ◁ Y β†’ Y ◁ Z β†’ X ◁ Z

(r , s , Ξ·) β—βˆ˜ (r' , s' , Ξ·') = (r ∘ r' , s' ∘ s , Ξ·'')
 where
  Ξ·'' = Ξ» x β†’ r (r' (s' (s x))) ＝⟨ ap r (Ξ·' (s x)) ⟩
              r (s x)           ＝⟨ η x ⟩
              x                 ∎

_β—βŸ¨_⟩_ : (X : 𝓀 Μ‡ ) {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } β†’ X ◁ Y β†’ Y ◁ Z β†’ X ◁ Z
X β—βŸ¨ ρ ⟩ Οƒ = ρ β—βˆ˜ Οƒ

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

Ξ£-retract : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ }
          β†’ ((x : X) β†’ A x ◁  B x) β†’ Ξ£ A ◁ Ξ£ B

Ξ£-retract {𝓀} {π“₯} {𝓦} {X} {A} {B} ρ = NatΞ£ r , NatΞ£ s , Ξ·'
 where
  r : (x : X) β†’ B x β†’ A x
  r x = retraction (ρ x)

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

  Ξ· : (x : X) (a : A x) β†’ r x (s x a) ＝ a
  η x = retract-equation (ρ x)

  Ξ·' : (Οƒ : Ξ£ A) β†’ NatΞ£ r (NatΞ£ s Οƒ) ＝ Οƒ
  η' (x , a) = x , r x (s x a) ＝⟨ to-Σ-＝' (η x a) ⟩
               x , a           ∎

transport-is-retraction : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) {x y : X} (p : x ＝ y)
                        β†’ transport A p ∘ transport A (p ⁻¹) ∼ 𝑖𝑑 (A y)

transport-is-retraction A (refl x) = refl

transport-is-section : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) {x y : X} (p : x ＝ y)
                     β†’ transport A (p ⁻¹) ∘ transport A p ∼ 𝑖𝑑 (A x)

transport-is-section A (refl x) = refl

Ξ£-reindexing-retract : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : X β†’ 𝓦 Μ‡ } (r : Y β†’ X)
                     β†’ has-section r
                     β†’ (Ξ£ x κž‰ X , A x) ◁ (Ξ£ y κž‰ Y , A (r y))

Ξ£-reindexing-retract {𝓀} {π“₯} {𝓦} {X} {Y} {A} r (s , Ξ·) = Ξ³ , Ο† , Ξ³Ο†
 where
  Ξ³ : Ξ£ (A ∘ r) β†’ Ξ£ A
  Ξ³ (y , a) = (r y , a)

  Ο† : Ξ£ A β†’ Ξ£ (A ∘ r)
  Ο† (x , a) = (s x , transport A ((Ξ· x)⁻¹) a)

  Ξ³Ο† : (Οƒ : Ξ£ A) β†’ Ξ³ (Ο† Οƒ) ＝ Οƒ
  Ξ³Ο† (x , a) = p
   where
    p : (r (s x) , transport A ((η x)⁻¹) a) ＝ (x , a)
    p = to-Σ-＝ (η x , transport-is-retraction A (η x) a)

singleton-type : {X : 𝓀 Μ‡ } β†’ X β†’ 𝓀 Μ‡
singleton-type {𝓀} {X} x = Ξ£ y κž‰ X , y ＝ x

singleton-type-center : {X : 𝓀 Μ‡ } (x : X) β†’ singleton-type x
singleton-type-center x = (x , refl x)

singleton-type-centered : {X : 𝓀 Μ‡ } (x : X) (Οƒ : singleton-type x)
                        β†’ singleton-type-center x ＝ Οƒ

singleton-type-centered x (x , refl x) = refl (x , refl x)

singleton-types-are-singletons : (X : 𝓀 Μ‡ ) (x : X)
                               β†’ is-singleton (singleton-type x)

singleton-types-are-singletons X x = singleton-type-center x ,
                                     singleton-type-centered x

retract-of-singleton : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                     β†’ Y ◁ X β†’ is-singleton X β†’ is-singleton Y

retract-of-singleton (r , s , Ξ·) (c , Ο†) = r c , Ξ³
 where
  Ξ³ = Ξ» y β†’ r c     ＝⟨ ap r (Ο† (s y)) ⟩
            r (s y) ＝⟨ η y ⟩
            y       ∎

singleton-type' : {X : 𝓀 Μ‡ } β†’ X β†’ 𝓀 Μ‡
singleton-type' {𝓀} {X} x = Ξ£ y κž‰ X , x ＝ y

singleton-type'-center : {X : 𝓀 Μ‡ } (x : X) β†’ singleton-type' x
singleton-type'-center x = (x , refl x)

singleton-type'-centered : {X : 𝓀 Μ‡ } (x : X) (Οƒ : singleton-type' x)
                         β†’ singleton-type'-center x ＝ Οƒ

singleton-type'-centered x (x , refl x) = refl (x , refl x)

singleton-types'-are-singletons : (X : 𝓀 Μ‡ ) (x : X)
                                β†’ is-singleton (singleton-type' x)

singleton-types'-are-singletons X x = singleton-type'-center x ,
                                      singleton-type'-centered x

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

\end{code}