{-

Theory about isomorphisms

- Definitions of [section] and [retract]
- Definition of isomorphisms ([Iso])
- Any isomorphism is an equivalence ([isoToEquiv])

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Isomorphism where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

private
  variable
     : Level

-- Section and retract
module _ { ℓ'} {A : Type } {B : Type ℓ'} where
  section : (f : A  B)  (g : B  A)  Type ℓ'
  section f g =  b  f (g b)  b

  -- NB: `g` is the retraction!
  retract : (f : A  B)  (g : B  A)  Type 
  retract f g =  a  g (f a)  a

record Iso { ℓ'} (A : Type ) (B : Type ℓ') : Type (ℓ-max  ℓ') where
  constructor iso
  field
    fun : A  B
    inv : B  A
    rightInv : section fun inv
    leftInv : retract fun inv

-- Any iso is an equivalence
module _ { ℓ'} {A : Type } {B : Type ℓ'} (i : Iso A B) where
  open Iso i renaming ( fun to f
                      ; inv to g
                      ; rightInv to s
                      ; leftInv to t)

  private
    module _ (y : B) (x0 x1 : A) (p0 : f x0  y) (p1 : f x1  y) where
      fill0 : I  I  A
      fill0 i = hfill  k  λ { (i = i1)  t x0 k
                               ; (i = i0)  g y })
                      (inS (g (p0 (~ i))))

      fill1 : I  I  A
      fill1 i = hfill  k  λ { (i = i1)  t x1 k
                               ; (i = i0)  g y })
                      (inS (g (p1 (~ i))))

      fill2 : I  I  A
      fill2 i = hfill  k  λ { (i = i1)  fill1 k i1
                               ; (i = i0)  fill0 k i1 })
                      (inS (g y))

      p : x0  x1
      p i = fill2 i i1

      sq : I  I  A
      sq i j = hcomp  k  λ { (i = i1)  fill1 j (~ k)
                              ; (i = i0)  fill0 j (~ k)
                              ; (j = i1)  t (fill2 i i1) (~ k)
                              ; (j = i0)  g y })
                     (fill2 i j)

      sq1 : I  I  B
      sq1 i j = hcomp  k  λ { (i = i1)  s (p1 (~ j)) k
                               ; (i = i0)  s (p0 (~ j)) k
                               ; (j = i1)  s (f (p i)) k
                               ; (j = i0)  s y k })
                      (f (sq i j))

      lemIso : (x0 , p0)  (x1 , p1)
      lemIso i .fst = p i
      lemIso i .snd = λ j  sq1 i (~ j)

  isoToIsEquiv : isEquiv f
  isoToIsEquiv .equiv-proof y .fst .fst = g y
  isoToIsEquiv .equiv-proof y .fst .snd = s y
  isoToIsEquiv .equiv-proof y .snd z = lemIso y (g y) (fst z) (s y) (snd z)


isoToEquiv :  { ℓ'} {A : Type } {B : Type ℓ'}  Iso A B  A  B
isoToEquiv i = _ , isoToIsEquiv i

isoToPath :  {} {A B : Type }  (Iso A B)  A  B
isoToPath {A = A} {B = B} f i =
  Glue B  { (i = i0)  (A , (Iso.fun f , isoToIsEquiv f))
            ; (i = i1)  (B ,  x  x) ,
                              record { equiv-proof = λ y  (y , refl)
                                                          , λ z i  z .snd (~ i)
                                                                  , λ j  z .snd (~ i  j)})})

compIso :  { ℓ' ℓ''} {A : Type } {B : Type ℓ'} {C : Type ℓ''}
           Iso A B  Iso B C  Iso A C
compIso (iso fun inv rightInv leftInv) (iso fun₁ inv₁ rightInv₁ leftInv₁) = iso (fun₁  fun) (inv  inv₁)
         b  cong fun₁ (rightInv (inv₁ b))  (rightInv₁ b))
         a  cong inv (leftInv₁ (fun a) )  leftInv a )