{-# OPTIONS --cubical #-}

open import Cubical.Core.Everything

postulate
  magic : ∀ {ℓ : Level} {X : Type ℓ} → X

refl : ∀ {ℓ : Level} {A : Type ℓ} {x : A} → x ≡ x
refl {x = x} = λ i → x

_∙_ : ∀ {ℓ : Level} {A : Type ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
_∙_ {A = A} {x = x} p q j = hcomp walls bottom where
  walls : ∀ (i : I) → Partial (j ∨ ~ j) A   -- \lor
  walls i (j = i0) = x
  walls i (j = i1) = q i

  bottom : A
  bottom = p j

infixr 80 _∙_

!_ : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x
!_ p i = p (~ i)
infixr 100 !_

{- alternative one: useful in the cubical type theories without "~" -}
!'_ : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x
!'_ = magic

-- i : bottom to top
-- j : left to right
∙-unit-r : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} (p : x ≡ y) → p ≡ p ∙ refl
∙-unit-r {A = A} {x = x} {y = y} p i j = hfill walls (inS bottom) i where
  walls : ∀ (i : I) → Partial (j ∨ ~ j) A
  walls i (j = i0) = x
  walls i (j = i1) = y

  bottom : A
  bottom = p j

-- k : front to back
-- i : left to right
-- j : bottom to top
∙-unit-l : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} (q : x ≡ y) → q ≡ refl ∙ q
∙-unit-l {A = A} {x = x} q k i = hcomp walls (q (~ k ∧ i)) where
  walls : ∀ j → Partial (~ k ∨ ~ i ∨ i) A
  walls j (k = i0) = q i
  walls j (i = i0) = x
  walls j (i = i1) = q (j ∨ ~ k)

-- k : front to back
-- i : left to right
-- j : bottom to top
!-inv-r : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} (p : x ≡ y) → refl ≡ p ∙ (! p)
!-inv-r {A = A} {x = x} q k i = hcomp walls (q (k ∧ i)) where
  walls : ∀ j → Partial (~ k ∨ ~ i ∨ i) A
  walls j (k = i0) = x
  walls j (i = i0) = x
  walls j (i = i1) = q (~ j ∧ k)

-- ~ (~ i) = i, so p (~ (~ i)) = p i, judgmentally
!-! : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} (p : x ≡ y) → ! (! p) ≡ p
!-! p = refl

-- using the fact that ! (! p) = p, judgmentally
!-inv-l : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} (p : x ≡ y) → refl ≡ (! p) ∙ p
!-inv-l p = !-inv-r (! p)

-- this lemmas is useful for ∙-assoc
3-out-of-4 : ∀ {ℓ} {A : Type ℓ}
  → (square₁ : I → I → A)
  → (p : square₁ i1 i0 ≡ square₁ i1 i1) (square₂ : PathP (λ j → Path A (square₁ j i0) (square₁ j i1)) (λ i → square₁ i0 i) p)
  → (λ i → square₁ i1 i) ≡ p
3-out-of-4 α p β = magic

∙-assoc : ∀ {ℓ : Level} {A : Type ℓ} {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
  → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
∙-assoc = magic

postulate
  myhfill : ∀ {ℓ : Level} {A : Type ℓ} {φ : I}
    → (walls : ∀ i → Partial φ A)
    → (bottom : A [ φ ↦ walls i0 ])
    → (i : I) → A

J : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {x : A} (B : (x' : A) → x ≡ x' → Type ℓ₂) (refl* : B x refl)
  {x' : A} (p : x ≡ x') → B x' p
J = magic