```{-# 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
```