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

open import sum
open import equality.core
open import equality.calculus
open import equality.reasoning
open import function.core
open import function.isomorphism.core
open import function.overloading
open import overloading.core

coherent :  {i j} {X : Set i}{Y : Set j}  X  Y  Set _
coherent f =  x  ap to (iso₁ x)  iso₂ (to x)
  -- this definition says that the two possible proofs that
  --     to (from (to x)) ≡ to x
  -- are equal
  where
    open _≅_ f

coherent' :  {i j} {X : Set i}{Y : Set j}  X  Y  Set _
coherent' f =  y  ap from (iso₂ y)  iso₁ (from y)
  where
    open _≅_ f

-- coherent isomorphisms
_≅'_ :  {i j}  (X : Set i)(Y : Set j)  Set _
X ≅' Y = Σ (X  Y) coherent

instance
  iso'-is-fun :  {i j}{X : Set i}{Y : Set j}
               Coercion (X ≅' Y) (X  Y)
  iso'-is-fun = record
    { coerce = λ isom  apply (proj₁ isom) }

  iso'-is-iso :  {i j}{X : Set i}{Y : Set j}
               Coercion (X ≅' Y) (X  Y)
  iso'-is-iso = record
    { coerce = proj₁ }

-- technical lemma: substiting a fixpoint proof into itself is like
-- applying the function
lem-subst-fixpoint :  {i}{X : Set i}
                     (f : X  X)(x : X)
                     (p : f x  x)
                    subst  x  f x  x) (sym p) p
                    ap f p
lem-subst-fixpoint {i}{X} f x p = begin
    subst  x  f x  x) (p ⁻¹) p
  ≡⟨ lem (f x) (sym p)  
    ap f (sym (sym p)) · p · sym p
  ≡⟨ ap  z  ap f z · p · sym p)
           (double-inverse p) 
    ap f p · p · sym p
  ≡⟨ associativity (ap f p) p (sym p) 
    ap f p · (p · sym p)
  ≡⟨ ap  z  ap f p · z) (left-inverse p) 
    ap f p · refl
  ≡⟨ left-unit (ap f p) 
    ap f p
  
  where
    open ≡-Reasoning
    lem : (y : X) (q : x  y)
         subst  z  f z  z) q p
         ap f (sym q) · p · q
    lem .x refl = sym (left-unit p)

lem-whiskering :  {i} {X : Set i}
                 (f : X  X) (H : (x : X)  f x  x)
                 (x : X)  ap f (H x)  H (f x)
lem-whiskering f H x = begin
    ap f (H x)
  ≡⟨ sym (lem-subst-fixpoint f x (H x)) 
    subst  z  f z  z) (sym (H x)) (H x)
  ≡⟨ ap' H (sym (H x)) 
    H (f x)
  
  where
    open ≡-Reasoning

lem-homotopy-nat :  {i j}{X : Set i}{Y : Set j}
                   {x x' : X}{f g : X  Y}
                   (H : (x : X)  f x  g x) (p : x  x')
                  H x · ap g p  ap f p · H x'
lem-homotopy-nat H refl = left-unit _

co-coherence :  {i j}{X : Set i}{Y : Set j}
               (isom : X  Y)
              coherent isom
              coherent' isom
co-coherence (iso f g H K) coherence y =
  subst  z  ap g (K z)  H (g z)) (K y) lem
  where
    open ≡-Reasoning

    lem : ap g (K (f (g y)))
         H (g (f (g y)))
    lem = begin
        ap g (K (f (g y)))
      ≡⟨ ap (ap g) (sym (coherence (g y))) 
        ap g (ap f (H (g y)))
      ≡⟨ ap-hom f g _ 
        ap (g  f) (H (g y))
      ≡⟨ lem-whiskering (g  f) H (g y) 
        H (g (f (g y)))
      

sym≅' :  {i j}{X : Set i}{Y : Set j}
       X ≅' Y  Y ≅' X
sym≅' (isom , γ) = sym≅ isom , co-coherence isom γ

--- Vogt's lemma. See http://ncatlab.org/nlab/show/homotopy+equivalence
vogt-lemma :  {i j}{X : Set i}{Y : Set j}  (isom : X  Y)
            let open _≅_ isom
              in Σ ((y : Y)  to (from y)  y) λ iso' 
                 coherent (iso to from iso₁ iso')
vogt-lemma {X = X}{Y = Y} isom = K' , γ
  where
    open _≅_ isom
      renaming (to to f ; from to g ; iso₁ to H ; iso₂ to K)

    -- Outline of the proof
    -- --------------------
    --
    -- We want to find a homotopy K' : f g → id such that f K' ≡ H f.
    --
    -- To do so, we first prove that the following diagram of
    -- homotopies:
    --
    --                     f H g f
    --          f g f g f ---------> f g f
    --              |                  |
    --     f g K f  |                  | K f
    --              |                  |
    --              v                  v
    --            f g f -------------> f
    --                       f H
    --
    -- commutes. We then observe that f appears on the right side of
    -- every element in the diagram, except the bottom row, so if we
    -- define:
    --
    --     K' = (f g K) ⁻¹ · (f H g f) · (K f)
    --
    -- we get that K' f must be equal to the bottom row, which is
    -- exactly the required coherence condition.

    open ≡-Reasoning

    -- the diagram above commutes
    lem : (x : X)
         ap f (H (g (f x))) · K (f x)
         ap (f  g) (K (f x)) · ap f (H x)
    lem x = begin
        ap f (H (g (f x))) · K (f x)
      ≡⟨ ap  z  ap f z · K (f x))
              (sym (lem-whiskering (g  f) H x)) 
        ap f (ap (g  f) (H x)) · K (f x)
      ≡⟨ ap  z  z · K (f x))
              (ap-hom (g  f) f (H x)) 
        ap (f  g  f) (H x) · K (f x)
      ≡⟨ sym (lem-homotopy-nat  x  K (f x)) (H x)) 
        K (f (g (f x))) · ap f (H x)
      ≡⟨ ap  z  z · ap f (H x))
              (sym (lem-whiskering (f  g) K (f x))) 
        ap (f  g) (K (f x)) · ap f (H x)
      

    K' : (y : Y)  f (g y)  y
    K' y = ap (f  g) (sym (K y))
         · ap f (H (g y))
         · K y

    iso' = iso f g H K'

    -- now we can just compute using the groupoid laws
    γ : coherent iso'
    γ x = sym $ begin
        K' (f x)
      ≡⟨ refl 
        ap (f  g) (sym (K (f x))) ·
        ap f (H (g (f x))) · K (f x)
      ≡⟨ associativity (ap (f  g) (sym (K (f x))))
               (ap f (H (g (f x))))
               (K (f x)) 
        ap (f  g) (sym (K (f x))) ·
        (ap f (H (g (f x))) · K (f x))
      ≡⟨ ap  z  ap (f  g) (sym (K (f x))) · z) (lem x) 
        ap (f  g) (sym (K (f x))) ·
        (ap (f  g) (K (f x)) · ap f (H x))
      ≡⟨ ap  z  z · (ap (f  g) (K (f x)) · ap f (H x)))
              (ap-inv (f  g) (K (f x))) 
        sym (ap (f  g) (K (f x))) ·
        (ap (f  g) (K (f x)) · ap f (H x))
      ≡⟨ sym (associativity (sym (ap (f  g) (K (f x))))
                       (ap (f  g) (K (f x)))
                       (ap f (H x))) 
        ( sym (ap (f  g) (K (f x))) ·
          ap (f  g) (K (f x)) ) ·
        ap f (H x)
      ≡⟨ ap  z  z · ap f (H x))
               (right-inverse (ap (f  g) (K (f x)))) 
        refl · ap f (H x)
      ≡⟨ right-unit (ap f (H x)) 
        ap f (H x)
      

≅⇒≅' :  {i j} {X : Set i}{Y : Set j}  X  Y  X ≅' Y
≅⇒≅' {X = X}{Y = Y} isom = iso to from iso₁ (proj₁ v) , proj₂ v
  where
    open _≅_ isom
    open import sum
    abstract
      v : Σ ((y : Y)  to (from y)  y) λ iso₂'
         coherent (iso to from iso₁ iso₂')
      v = vogt-lemma isom