{-# OPTIONS --cubical #-}

module Cubical.Experiments.BrunerieCobordism where

open import Cubical.Foundations.Prelude
open import Cubical.HITs.S2.Base

private
  variable
    ℓ : Level
    A : Type ℓ
    x : A

Ω Ω² Ω³ : (A : Type ℓ) → A → Type ℓ
Ω A x = Path A x x
Ω² A x = Ω (Ω A x) refl
Ω³ A x = Ω (Ω² A x) refl

erp : I → I → I → I
erp t x y = (~ t ∧ x) ∨ (t ∧ y) ∨ (x ∧ y)

dsqInv : {x y : A} (p : x ≡ y) → p ≡ p → Ω² A x
dsqInv {x = x} p r i j =
  hcomp (λ k → λ { (i = i0) → p (j ∧ ~ k)
                 ; (i = i1) → p (j ∧ ~ k)
                 ; (j = i0) → x
                 ; (j = i1) → p (~ k)
                 })
        (r i j)

csq : {x y z : A} (p : x ≡ y) (q : y ≡ z)
  → Ω² A y
  → PathP (λ i → p i ≡ q i) p q
csq p q r i j =
  hcomp (λ k → λ { (i = i0) → p (~ k ∨ j)
                 ; (i = i1) → q (k ∧ j)
                 ; (j = i0) → p (~ k ∨ i)
                 ; (j = i1) → q (k ∧ i)
                 })
        (r i j)

csqInv : {x y z : A} (p : x ≡ y) (q : y ≡ z)
  → PathP (λ i → p i ≡ q i) p q
  → Ω² A y
csqInv p q r i j =
  hcomp (λ k → λ { (i = i0) → p (k ∨ j)
                 ; (i = i1) → q (~ k ∧ j)
                 ; (j = i0) → p (k ∨ i)
                 ; (j = i1) → q (~ k ∧ i)
                 })
        (r i j)

W₂₂' : (p q : Ω² A x) → q ≡ q
W₂₂' p q j a b =
  hcomp (λ i → λ { (j = i0) → q a b
                 ; (j = i1) → q a b
                 ; (a = i0) → p i j
                 ; (a = i1) → p i j
                 ; (b = i0) → p i j
                 ; (b = i1) → p i j
                 })
        (q a b)

EH : (p q : Ω² A x) → PathP (λ i → PathP (λ j → Ω A x) (p i) (p i)) q q
EH {x = x} p q i j k =
  hcomp (λ f → λ { (i = i0) → q j (erp f i0 k)
                 ; (i = i1) → q j (erp f i0 k)
                 ; (j = i0) → p i (erp f i1 k)
                 ; (j = i1) → p i (erp f i1 k)
                 ; (k = i0) → p i (~ f)
                 ; (k = i1) → q j f
                 })
        x

W₂₂'-turned : (p q : Ω² A x) → Path (Ω² A x) q q
W₂₂'-turned {x = x} p q j a b =
  hcomp (λ i → λ { (j = i0) → EH q p a i b
                 ; (j = i1) → EH p q i a b
                 ; (a = i0) → p i b
                 ; (a = i1) → p i b
                 ; (b = i0) → x
                 ; (b = i1) → x
                 })
        (q a b)

hopf : Ω² A x → Ω³ A x
hopf p = csqInv p p (EH p p)

hopfS :  Ω³ S² base
hopfS = hopf surf


-- The examples:

b0 : Ω³ S² base
b0 = dsqInv surf (W₂₂' surf surf)

b1 : Ω³ S² base
b1 = dsqInv surf (W₂₂'-turned surf surf)

b2 : Ω³ S² base
b2 = dsqInv surf (λ i j → hcomp (λ k → λ { (i = i0) → csq surf surf (hopf surf) j k
                                         ; (i = i1) → csq surf surf (hopf surf) k j
                                         ; (j = i0) → surf k
                                         ; (j = i1) → surf k
                                         })
                                (surf j))

b3 : Ω³ S² base
b3 = dsqInv surf (λ i j → hcomp (λ k → λ { (i = i0) → csq refl surf (hopf surf) j k
                                         ; (i = i1) → csq refl surf (hopf surf) k j
                                         ; (j = i0) → refl
                                         ; (j = i1) → surf k
                                         })
                                refl)

b4 : Ω³ S² base
b4 = dsqInv refl (λ i j → hcomp (λ k → λ { (i = i0) → csq refl refl (hopf surf) j k
                                         ; (i = i1) → csq refl refl (hopf surf) k j
                                         ; (j = i0) → refl
                                         ; (j = i1) → refl
                                         })
                                refl)

b5 : Ω³ S² base
b5 = (λ i j → hcomp (λ k → λ { (i = i0) → csq refl refl (hopf surf) j k
                             ; (i = i1) → csq refl refl (hopf surf) k j
                             ; (j = i0) → refl
                             ; (j = i1) → refl
                             })
                    refl)

b6 : Ω³ S² base
b6 = (λ i j → hcomp (λ k → λ { (i = i0) → hopf surf j k
                             ; (i = i1) → hopf surf k j
                             ; (j = i0) → refl
                             ; (j = i1) → refl
                             })
                    refl)

b7 : Ω³ S² base
b7 = (λ i j → hcomp (λ k → λ { (i = i0) → hopf surf (~ k) j
                             ; (i = i1) → hopf surf k j
                             ; (j = i0) → refl
                             ; (j = i1) → refl
                             })
                    (λ _ → base))

b8 : Ω³ S² base
b8 = hopf surf ∙ refl ∙ hopf surf

b9 : Ω³ S² base
b9 = hopf surf ∙ hopf surf