{-
CANCELLING INVERSES

Some simple but useful auxiliary definitions.
The development could be significantly extended, but the existing
code is sufficient for the current project.
-}


{-# OPTIONS --safe --cubical #-}

open import Cubical.Foundations.Prelude

open import squier.graphclosures
open import squier.polygraphs

-- Here: Level variables are fixed for the whole module.
-- (Note: Would be better to turn them into actual variables.)
module squier.cancelInverses {ℓ₀ ℓ₁ ℓ₂ : Level}
                             (p : 2-polygraph {ℓ₀} {ℓ₁} {ℓ₂}) where

open polygraph-properties p

-- ### Cancelling inverses: Simple but useful properties

cancelsRInv = ∀ {x y} (u : x ↝ y) → (inj u ∷ᵗ rev u ∷ᵗ []ᵗ) ⇒* []ᵗ
cancelsLInv = ∀ {x y} (u : x ↝ y) → (rev u ∷ᵗ inj u ∷ᵗ []ᵗ) ⇒* []ᵗ

-- cancels*RInv is the one we ultimately need
cancels*RInv = ∀ {x y} (u : x ↭* y) → (u ++ᵗ reverse u) ⇔* []ᵗ

-- cancels*LInv can be derived
cancels*LInv = ∀ {x y} (u : x ↭* y) → (reverse u ++ᵗ u) ⇔* []ᵗ

cancelsR2L : cancels*RInv → cancels*LInv
cancelsR2L cri {x} {y} u =
    reverse u ++ᵗ u
      ⇔*⟨ ≡2⇔* (cong (λ u' → reverse u ++ᵗ u') (sym (reverse-reverse u))) ⟩
    reverse u ++ᵗ reverse (reverse u)
      ⇔*⟨ cri (reverse u) ⟩
    []ᵗ
      ⇔*∎

{- TEMPORARILY ABANDONED CODE:
   While the below would be useful in general, it is not required for the
   current project and currently unfinished.
   The goal here was to develop lemmas that show that certain simple
   conditions are sufficient.

module _ (cc : ⇒*isCongrClosed) (cri : cancelsRInv) (cli : cancelsLInv) where

  cancel-step : ∀ {x y} (u : x ↭ y) → (u ∷ᵗ negate u ∷ᵗ []ᵗ) ⇒* []ᵗ
  cancel-step (inj u) = cri u
  cancel-step (rev u) = cli u

  c*ri : cancels*RInv
  c*ri []ᵗ = []ᵗ
  c*ri (s ∷ᵗ u) =
    s ∷ᵗ u ++ᵗ reverse (s ∷ᵗ u)
      ⇔*⟨ []ᵗ ⟩
    s ∷ᵗ (u ++ᵗ reverse u ++ᵗ negate s ∷ᵗ []ᵗ)
      ⇔*⟨ {! subst (λ x → (s ∷ᵗ x) ⇒* (s ∷ᵗ ((u ++ᵗ reverse u) ++ᵗ negate s ∷ᵗ []ᵗ)))
                (++ᵗ-assoc u (reverse u) _)
                []ᵗ !} ⟩
    s ∷ᵗ ((u ++ᵗ reverse u) ++ᵗ negate s ∷ᵗ []ᵗ)
      ⇔*⟨ {! cc (s ∷ᵗ []ᵗ) _ _ (negate s ∷ᵗ []ᵗ) ? !} ⟩ -- (c*ri u)  ⟩
    s ∷ᵗ negate s ∷ᵗ []ᵗ
      ⇔*⟨ {! cancel-step s !} ⟩
    []ᵗ
      ⇔*∎

  {- Probably don't need
  c*li : cancels*LInv
  c*li []ᵗ = []ᵗ
  c*li (s ∷ᵗ u) = {!!}
  -}
-}