{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Everything
open import Cubical.Foundations.CartesianKanOps
open import Cubical.Data.Bool
open import Cubical.HITs.S1

module _ where

module MöbiusBoundary where

  boundary : S¹ → Type₀
  boundary base = Bool
  boundary (loop i) = notEq i

  boundary-loop : I → Type₀
  boundary-loop i = boundary (loop i)

  diamond : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) → (λ i → p i ≡ q i) [ p ≡ q ]
  diamond {y = y} p q i j =
    hcomp
      (λ k → λ
        { (i = i0) → p (j ∨ ~ k)
        ; (i = i1) → q (j ∧ k)
        ; (j = i0) → p (i ∨ ~ k)
        ; (j = i1) → q (i ∧ k)
        }) y

  theorem : Σ S¹ boundary ≃ S¹
  theorem = isoToEquiv (iso f g f-g g-f) where

    f' : Bool → base ≡ base
    f' true i = loop i
    f' false i = base

    f'-not : (x : Bool) → f' (not x) i0 ≡ base
    f'-not true = refl
    f'-not false = refl

    f : Σ S¹ boundary → S¹
    f (base , _) = base
    f (loop i , x) = f' (coei→0 boundary-loop i x) i

    g' : ∀ b → Path (Σ S¹ boundary) (base , not b) (base , b)
    g' b i = loop i , coe1→i boundary-loop i b

    g : S¹ → Σ S¹ boundary
    g base = base , true
    g (loop i) = (g' false ∙ g' true) i

    coei→0-coe0→i : ∀ (i : I) (b : Bool) → coei→0 boundary-loop i (coe1→i boundary-loop i b) ≡ not b
    coei→0-coe0→i i b k = coei→0 boundary-loop (i ∧ ~ k) (coe1→i boundary-loop (i ∧ ~ k) b)

    f-g' : (b : Bool) → cong f (g' b) ≡ f' (not b)
    f-g' b k i = f' (coei→0-coe0→i i b k) i

    f-g : ∀ x → f (g x) ≡ x
    f-g base = refl
    f-g (loop i) j = hcomp walls bottom where
      walls : (k : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j) S¹
      walls k (j = i0) = f (compPath-filler (g' false) (g' true) k i)
      walls k (j = i1) = loop i
      walls k (i = i0) = base
      walls k (i = i1) = f-g' true j k

      bottom = f-g' false j i

    g-f-base : (b : Bool) → g base ≡ (base , b)
    g-f-base true = g' false ∙ g' true
    g-f-base false = g' false

    g-f-loop' : (i : I) (x : boundary (loop i)) → g (f (loop i , x)) ≡ (loop i , x)
    g-f-loop' i = coe0→i (λ i → ∀ x → g (f (loop i , x)) ≡ (loop i , x)) i g-f-base

    g-f-fix₁ : ∀ b → g-f-loop' i1 b ≡ g-f-base b
    g-f-fix₁ true =
      g-f-loop' i1 true
        ≡⟨ refl ⟩
      transport (λ i → g (f (g' true i)) ≡ g' true i) (g' false)
        ≡[ j ]⟨ transport (λ i → g (f-g' true j i) ≡ g' true i) (g' false) ⟩
      transport (λ i → g (f' false i) ≡ g' true i) (g' false)
        ≡⟨ refl ⟩
      transport (λ i → (base , true) ≡ g' true i) (g' false)
        ≡⟨ refl ⟩
      g-f-base true
        ∎
    g-f-fix₁ false =
      g-f-loop' i1 false
        ≡⟨ refl ⟩
      transport (λ i → g (f (g' false i)) ≡ g' false i) (g' false ∙ g' true)
        ≡[ j ]⟨ transport (λ i → g (f-g' false j i) ≡ g' false i) (g' false ∙ g' true) ⟩
      transport (λ i → g (f' true i) ≡ g' false i) (g' false ∙ g' true)
        ≡⟨ refl ⟩
      transport (λ i → (g' false ∙ g' true) i ≡ g' false i) (g' false ∙ g' true)
        ≡⟨ 3outof4
            (λ i j → transport-filler (λ i → (g' false ∙ g' true) i ≡ g' false i) (g' false ∙ g' true) i j)
            (g-f-base false)
            (λ i j → diamond (g' false ∙ g' true) (g' false) i j) ⟩
      g-f-base false
        ∎

    g-f : ∀ x → g (f x) ≡ x
    g-f (base , b) = g-f-base b
    g-f (loop i , x) j = hcomp
      (λ k →
        (λ { (i = i0) → g-f-base x j
           ; (i = i1) → g-f-fix₁ x k j
           ; (j = i0) → g (f (loop i , x))
           ; (j = i1) → (loop i , x)
           }))
      (g-f-loop' i x j)