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

-- 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
≡ cong f p
lem-subst-fixpoint {i}{X} f x p = begin
subst (λ x → f x ≡ x) (p ⁻¹) p
≡⟨ lem (f x) (sym p) ⟩
cong f (sym (sym p)) ⊚ p ⊚ sym p
≡⟨ cong (λ z → cong f z ⊚ p ⊚ sym p)
(double-inverse p) ⟩
cong f p ⊚ p ⊚ sym p
≡⟨ associativity (cong f p) p (sym p) ⟩
cong f p ⊚ (p ⊚ sym p)
≡⟨ cong (λ z → cong f p ⊚ z) (left-inverse p) ⟩
cong f p ⊚ refl
≡⟨ left-unit (cong f p) ⟩
cong f p
∎
where
open ≡-Reasoning
lem : (y : X) (q : x ≡ y)
→ subst (λ z → f z ≡ z) q p
≡ cong 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) → cong f (H x) ≡ H (f x)
lem-whiskering f H x = begin
cong f (H x)
≡⟨ sym (lem-subst-fixpoint f x (H x)) ⟩
subst (λ z → f z ≡ z) (sym (H x)) (H x)
≡⟨ cong' 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 ⊚ cong g p ≡ cong 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 → cong g (K z) ≡ H (g z)) (K y) lem
where
open ≡-Reasoning

lem : cong g (K (f (g y)))
≡ H (g (f (g y)))
lem = begin
cong g (K (f (g y)))
≡⟨ cong (cong g) (sym (coherence (g y))) ⟩
cong g (cong f (H (g y)))
≡⟨ cong-hom f g _ ⟩
cong (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)
→ cong f (H (g (f x))) ⊚ K (f x)
≡ cong (f ∘ g) (K (f x)) ⊚ cong f (H x)
lem x = begin
cong f (H (g (f x))) ⊚ K (f x)
≡⟨ cong (λ z → cong f z ⊚ K (f x))
(sym (lem-whiskering (g ∘ f) H x)) ⟩
cong f (cong (g ∘ f) (H x)) ⊚ K (f x)
≡⟨ cong (λ z → z ⊚ K (f x))
(cong-hom (g ∘ f) f (H x)) ⟩
cong (f ∘ g ∘ f) (H x) ⊚ K (f x)
≡⟨ sym (lem-homotopy-nat (λ x → K (f x)) (H x)) ⟩
K (f (g (f x))) ⊚ cong f (H x)
≡⟨ cong (λ z → z ⊚ cong f (H x))
(sym (lem-whiskering (f ∘ g) K (f x))) ⟩
cong (f ∘ g) (K (f x)) ⊚ cong f (H x)
∎

K' : (y : Y) → f (g y) ≡ y
K' y = cong (f ∘ g) (sym (K y))
⊚ cong 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 ⟩
cong (f ∘ g) (sym (K (f x))) ⊚
cong f (H (g (f x))) ⊚ K (f x)
≡⟨ associativity (cong (f ∘ g) (sym (K (f x))))
(cong f (H (g (f x))))
(K (f x)) ⟩
cong (f ∘ g) (sym (K (f x))) ⊚
(cong f (H (g (f x))) ⊚ K (f x))
≡⟨ cong (λ z → cong (f ∘ g) (sym (K (f x))) ⊚ z) (lem x) ⟩
cong (f ∘ g) (sym (K (f x))) ⊚
(cong (f ∘ g) (K (f x)) ⊚ cong f (H x))
≡⟨ cong (λ z → z ⊚ (cong (f ∘ g) (K (f x)) ⊚ cong f (H x)))
(cong-inv (f ∘ g) (K (f x))) ⟩
sym (cong (f ∘ g) (K (f x))) ⊚
(cong (f ∘ g) (K (f x)) ⊚ cong f (H x))
≡⟨ sym (associativity (sym (cong (f ∘ g) (K (f x))))
(cong (f ∘ g) (K (f x)))
(cong f (H x))) ⟩
( sym (cong (f ∘ g) (K (f x))) ⊚
cong (f ∘ g) (K (f x)) ) ⊚
cong f (H x)
≡⟨ cong (λ z → z ⊚ cong f (H x))
(right-inverse (cong (f ∘ g) (K (f x)))) ⟩
refl ⊚ cong f (H x)
≡⟨ right-unit (cong f (H x)) ⟩
cong f (H x)
∎

≅⇒≅' : ∀ {i j} {X : Set i}{Y : Set j} → X ≅ Y → X ≅' Y
≅⇒≅' isom = iso to from iso₁ (proj₁ v) , proj₂ v
where
open _≅_ isom
v = vogt-lemma isom
```