{-# OPTIONS --without-K #-}

module non-coherence where

open import sets.empty
open import equality.core
open import equality.reasoning
open import equality.calculus
open import function
open import function.isomorphism
open import hott.coherence
open import higher.circle

X : Set
X = S¹

P : (x : X) → Set
P x = x ≡ x

loop-coherence : subst (λ z → z ≡ z) loop loop ≡ loop
loop-coherence = begin
    subst (λ z → z ≡ z) loop loop
  ≡⟨ subst-eq₂ loop loop ⟩
    sym loop ⊚ loop ⊚ loop
  ≡⟨ cong (λ z → z ⊚ loop) (right-inverse loop) ⟩
    refl ⊚ loop
  ≡⟨ right-unit loop ⟩
    loop
  ∎
  where
    open ≡-Reasoning

H : (x : X) → x ≡ x
H = elim' P loop loop-coherence

K : (x : X) → x ≡ x
K _ = refl

isom : X ≅ X
isom = iso id id H K

non-coherent : ¬ (isCoherent isom)
non-coherent γ = non-simply-connected absurd
  where
    open ≡-Reasoning

    absurd : loop ≡ refl
    absurd = begin
        loop
      ≡⟨ sym (β-base' P loop loop-coherence) ⟩
        H base
      ≡⟨ sym (cong-id (H base)) ⟩
        cong id (H base)
      ≡⟨ γ base ⟩
        K (id base)
      ≡⟨ refl ⟩
        refl
      ∎