{-# OPTIONS --without-K #-}
module function.isomorphism.properties where

open import level
open import sum
open import sets.nat.core
open import equality.core
open import equality.calculus
open import equality.reasoning
open import function.core
open import function.fibration
open import function.overloading
open import function.extensionality.core
open import function.extensionality.proof
open import function.isomorphism.core
open import function.isomorphism.coherent
open import function.isomorphism.lift
open import function.isomorphism.utils
open import function.isomorphism.two-out-of-six
open import hott.equivalence.core
open import hott.equivalence.alternative
open import hott.level.core
open import hott.loop.core
open import sets.unit

iso-adjunction : ∀ {i j}{X : Set i}{Y : Set j}
               → (isom : X ≅ Y)(x : X)(y : Y)
               → (apply isom x ≡ y) ≅ (x ≡ invert isom y)
iso-adjunction {i}{j}{X}{Y} isom x y
  = family-eq-iso total' (λ { (y , x) q → comm' x y q }) (y , x)
  where
    open _≅_ isom
    open ≅-Reasoning

    to-we : weak-equiv to
    to-we = proj₂ (≅⇒≈ isom)

    total' : (Σ (Y × X) λ { (y , x) → to x ≡ y })
           ≅ (Σ (Y × X) λ { (y , x) → x ≡ from y})
    total' = Σ-assoc-iso
           ·≅ ( Σ-ap-iso refl≅ λ y
              → contr-⊤-iso (to-we y)
              ·≅ sym≅ (contr-⊤-iso (singl-contr' (from y))) )
           ·≅ sym≅ Σ-assoc-iso

    comm' : (x : X)(y : Y)(p : to x ≡ y)
          → proj₁ (apply total' ((y , x) , p)) ≡ (y , x)
    comm' x y q = ap (_,_ y) (sym (ap from q) · iso₁ x)

private
  iso≡-lem : ∀ {i j}{X : Set i}{Y : Set j}
           → (isom : X ≅ Y)
           → (x x' : X)
           → weak-equiv (λ (p : x ≡ x') → ap (invert isom) (ap (apply isom) p))
  iso≡-lem {X = X} isom x x' = step₃
    where
      step₁ : ∀ {k}{A : Set k}(a a' : A)
            → weak-equiv {X = a ≡ a'} {Y = a ≡ a'} (ap (λ x → x))
      step₁ a a' = subst weak-equiv (sym (funext ap-id)) (proj₂ (≅⇒≈ refl≅))

      step₂ : weak-equiv (λ (p : x ≡ x') → ap (invert isom ∘ apply isom) p)
      step₂ = subst (λ u → weak-equiv {X = x ≡ x'} (ap u)) (sym (funext (_≅_.iso₁ isom)))
                    (step₁ x x')

      step₃ = subst weak-equiv (sym (funext λ p → ap-hom (apply isom) (invert isom) p)) step₂

iso≡ : ∀ {i j}{X : Set i}{Y : Set j}
     → (isom : X ≅ Y)
     → {x x' : X}
     → (x ≡ x')
     ≅ (apply isom x ≡ apply isom x')
iso≡ isom {x}{x'} = two-out-of-six.f-iso
  (ap (apply isom))
  (ap (invert isom))
  (ap (apply isom))
  (iso≡-lem isom x x')
  (iso≡-lem (sym≅ isom) (apply isom x) (apply isom x'))

private
  abstract
    Ω-iso' : ∀ {i j}{X : Set i}{Y : Set j}(n : ℕ)
           → (φ : X ≅ Y)(x : X)
           → Ω n x ≅ Ω n (apply φ x)
    Ω-iso' {X = X}{Y = Y} zero φ x = φ
    Ω-iso' (suc n) φ x = Ω-iso' n (iso≡ φ) refl

    Ω-iso-β : ∀ {i j}{X : Set i}{Y : Set j}(n : ℕ)
            → (φ : X ≅ Y)(x : X)
            → (p : Ω n x)
            → apply (Ω-iso' n φ x) p ≡ mapΩ n (apply φ) p
    Ω-iso-β zero φ x p = refl
    Ω-iso-β (suc n) φ x p = Ω-iso-β n (iso≡ φ) refl p

Ω-iso : ∀ {i j}{X : Set i}{Y : Set j}(n : ℕ)
      → (φ : X ≅ Y)(x : X)
      → Ω n x ≅ Ω n (apply φ x)
Ω-iso n φ x = ≈⇒≅ ( (λ p → mapΩ n (apply φ) p)
                  , subst weak-equiv eq we)
  where
    abstract
      we : weak-equiv (apply (Ω-iso' n φ x))
      we = proj₂ (≅⇒≈ (Ω-iso' n φ x))

      eq : apply (Ω-iso' n φ x) ≡ mapΩ n (apply φ)
      eq = funext (Ω-iso-β n φ x)

abstract
  subtype-eq : ∀ {i j k}{A : Set i}{P : A → Set j}
             → ((x : A) → h  (P x))
             → {X : Set k}
             → (isom : X ≅ Σ A P)
             → {x y : X}
             → (proj₁ (apply isom x) ≡ proj₁ (apply isom y))
             → x ≡ y
  subtype-eq hP isom p = iso⇒inj isom
    (unapΣ (p , h1⇒prop (hP _) _ _))