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

module function.isomorphism.utils where

open import sum
open import equality.core
open import equality.calculus
open import function.core
open import function.isomorphism.core
open import function.isomorphism.coherent
open import function.extensionality.core
open import sets.unit
open import hott.hlevel.core

Σ-split-iso :  {i j}{X : Set i}{Y : X  Set j}
             {a a' : X}{b : Y a}{b' : Y a'}
             (Σ (a  a') λ q  subst Y q b  b')
             ((a , b)  (a' , b'))
Σ-split-iso {Y = Y}{a}{a'}{b}{b'} = iso uncongΣ congΣ H K
  where
    H :  {a a'}{b : Y a}{b' : Y a'}
       (p : Σ (a  a') λ q  subst Y q b  b')
       congΣ (uncongΣ {a = a}{a' = a'}{b = b}{b' = b'} p)  p
    H (refl , refl) = refl

    K : (p : (a , b)  (a' , b'))  uncongΣ (congΣ p)  p
    K = J  u v p  uncongΣ (congΣ p)  p)
           {(a , b)  refl })
          (a , b) (a' , b')

Σ-cong-iso :  {i i' j j'}{X : Set i}{X' : Set i'}
             {Y : X  Set j}{Y' : X'  Set j'}
            (isom : X  X')
            ((x' : X')  Y (invert isom x')  Y' x')
            Σ X Y  Σ X' Y'
Σ-cong-iso {X = X}{X'}{Y}{Y'} isom isom' = trans≅ Σ-iso (Σ-iso' isom')
  where
    isom-c = ≅⇒≅' isom
    γ = proj₂ isom-c
    open _≅_ (proj₁ isom-c)
      renaming ( to to f ; from to g
               ; iso₁ to H; iso₂ to K )

    lem : (x : X')  sym (H (g x))  cong g (K x)  refl
    lem x = cong  z  sym (H (g x))  z) (co-coherence _ γ x)
           right-inverse (H (g x))

    Σ-iso : Σ X Y  Σ X' (Y  g)
    Σ-iso = record
      { to = λ { (x , y)  (f x , subst Y (sym (H x)) y) }
      ; from = λ { (x , y)  (g x , y) }
      ; iso₁ = λ { (x , y)  uncongΣ (H x ,
            subst-hom Y (sym (H x)) (H x) y
           cong  p  subst Y p y) (right-inverse (H x)) ) }
      ; iso₂ = λ { (x , y)  uncongΣ (K x ,
            subst-naturality Y g (K x) _
           (subst-hom Y (sym (H (g x))) (cong g (K x)) y
           cong  p  subst Y p y) (lem x) ) ) } }

    Σ-iso' :  {i j j'}{X : Set i}{Y : X  Set j}{Y' : X  Set j'}
            ((x : X)  Y x  Y' x)
            Σ X Y  Σ X Y'
    Σ-iso' isom = record
      { to = λ { (x , y)  (x , apply (isom x) y) }
      ; from = λ { (x , y')  (x , invert (isom x) y') }
      ; iso₁ = λ { (x , y)  uncongΣ (refl , _≅_.iso₁ (isom x) y) }
      ; iso₂ = λ { (x , y')  uncongΣ (refl , _≅_.iso₂ (isom x) y') } }

Π-cong-iso :  {i i' j j'}{X : Set i}{X' : Set i'}
             {Y : X  Set j}{Y' : X'  Set j'}
            (ext' :  {i j}  Extensionality' i j)
            (isom : X  X')
            ((x' : X')  Y (invert isom x')  Y' x')
            ((x : X)  Y x)
            ((x' : X')  Y' x')
Π-cong-iso {X = X}{X'}{Y}{Y'} ext' isom isom' =
  trans≅ (Π-iso (≅⇒≅' isom)) (Π-iso' isom')
  where
    Π-iso : (isom : X ≅' X')
           ((x : X)  Y x)
           ((x' : X')  Y (invert (proj₁ isom) x'))
    Π-iso (iso f g H K , γ) = record
      { to = λ h x'  h (g x')
      ; from = λ h' x  subst Y (H x) (h' (f x))
      ; iso₁ = λ h  ext' λ x  cong' h (H x)
      ; iso₂ = λ h'  ext' λ x' 
              cong  p  subst Y p _) (sym (γ' x'))
             sym (subst-naturality Y g (K x') _)
             cong' h' (K x') }
      where γ' = co-coherence (iso f g H K) γ

    Π-iso' :  {i j j'}{X : Set i}
             {Y : X  Set j}{Y' : X  Set j'}
            ((x : X)  Y x  Y' x)
            ((x : X)  Y x)
            ((x : X)  Y' x)
    Π-iso' isom = record
      { to = λ h x  apply (isom x) (h x)
      ; from = λ h' x  invert (isom x) (h' x)
      ; iso₁ = λ h  ext' λ x  _≅_.iso₁ (isom x) _
      ; iso₂ = λ h'  ext' λ x  _≅_.iso₂ (isom x) _ }

ΠΣ-swap-iso :  {i j k}{X : Set i}{Y : X  Set j}
             {Z : (x : X)  Y x  Set k}
             ((x : X)  Σ (Y x) λ y  Z x y)
             (Σ ((x : X)  Y x) λ f  ((x : X)  Z x (f x)))
ΠΣ-swap-iso = record
  { to = λ f  (proj₁  f , proj₂  f)
  ; from = λ { (f , g) x  (f x , g x) }
  ; iso₁ = λ _  refl
  ; iso₂ = λ _  refl }

curry-iso :  {i j k}{X : Set i}{Y : X  Set j}
            (Z : (x : X)  Y x  Set k)
           ((xy : Σ X Y)  Z (proj₁ xy) (proj₂ xy))
           ((x : X)  (y : Y x)  Z x y)
curry-iso _ = record
  { to = λ f x y  f (x , y)
  ; from = λ { f (x , y)  f x y }
  ; iso₁ = λ _  refl
  ; iso₂ = λ _  refl }

impl-iso :  {i j}{X : Set i}{Y : X  Set j}
          ((x : X)  Y x)  ({x : X}  Y x)
impl-iso = record
  { to = λ f  f _
  ; from = λ f _  f
  ; iso₁ = λ _  refl
  ; iso₂ = λ _  refl }

Σ-assoc-iso :  {i j k}
              {X : Set i}{Y : X  Set j}
              {Z : (x : X)  Y x  Set k}
             Σ (Σ X Y)  {(x , y)  Z x y})
             Σ X λ x  Σ (Y x) (Z x)
Σ-assoc-iso = record
  { to = λ {((x , y) , z)  (x , y , z) }
  ; from = λ {(x , y , z)  ((x , y) , z) }
  ; iso₁ = λ _  refl
  ; iso₂ = λ _  refl }

×-left-unit :  {i}{X : Set i}  ( × X)  X
×-left-unit = record
  { to = λ {(tt , x)  x }
  ; from = λ x  tt , x
  ; iso₁ = λ _  refl
  ; iso₂ = λ _  refl }

×-right-unit :  {i}{X : Set i}  (X × )  X
×-right-unit = record
  { to = λ {(x , tt)  x }
  ; from = λ x  x , tt
  ; iso₁ = λ _  refl
  ; iso₂ = λ _  refl }

contr-⊤-iso :  {i}{X : Set i}
             contr X  X  
contr-⊤-iso hX = record
  { to = λ x  tt
  ; from = λ { tt  proj₁ hX }
  ; iso₁ = λ x  proj₂ hX x
  ; iso₂ = λ { tt  refl } }

×-comm :  {i j}{X : Set i}{Y : Set j}
        (X × Y)  (Y × X)
×-comm = record
  { to = λ {(x , y)  (y , x)}
  ; from = λ {(y , x)  (x , y)}
  ; iso₁ = λ _  refl
  ; iso₂ = λ _  refl }

-- rewriting lemmas for equations on equalities
sym≡-iso :  {i}{X : Set i}(x y : X)
          (x  y)
          (y  x)
sym≡-iso _ _ = iso sym sym double-inverse double-inverse

move-≡-iso :  {i}{X : Set i}{x y z : X}
            (p : x  y)(q : y  z)(r : x  z)
            (p  q  r)
            (sym p  r  q)
move-≡-iso refl = sym≡-iso