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

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