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

open import lib.Base
open import lib.PathGroupoid
open import lib.PathFunctor
open import lib.path-seq.Concat
open import lib.path-seq.Reasoning

module lib.path-seq.Inversion {i} {A : Type i} where

seq-! : {a a' : A} → a =-= a' → a' =-= a
seq-! [] = []
seq-! (p ◃∙ s) = seq-! s ∙▹ ! p

seq-!-∙▹ : {a a' a'' : A} (s : a =-= a') (q : a' == a'')
  → seq-! (s ∙▹ q) == ! q ◃∙ seq-! s
seq-!-∙▹ [] q = idp
seq-!-∙▹ (p ◃∙ s) q = ap (_∙▹ ! p) (seq-!-∙▹ s q)

seq-!-seq-! : {a a' : A} (s : a =-= a')
  → seq-! (seq-! s) == s
seq-!-seq-! [] = idp
seq-!-seq-! (p ◃∙ s) =
  seq-! (seq-! s ∙▹ ! p)
    =⟨ seq-!-∙▹ (seq-! s) (! p) ⟩
  ! (! p) ◃∙ seq-! (seq-! s)
    =⟨ ap2 _◃∙_ (!-! p) (seq-!-seq-! s) ⟩
  p ◃∙ s =∎

!-∙-seq : {a a' : A} (s : a =-= a')
  → ! (↯ s) ◃∎ =ₛ seq-! s
!-∙-seq [] = =ₛ-in idp
!-∙-seq (p ◃∙ s) =
  ! (↯ (p ◃∙ s)) ◃∎
    =ₛ₁⟨ ap ! (↯-∙∙ (p ◃∎) s) ⟩
  ! (p ∙ ↯ s) ◃∎
    =ₛ⟨ =ₛ-in {t = ! (↯ s) ◃∙ ! p ◃∎} (!-∙ p (↯ s)) ⟩
  ! (↯ s) ◃∙ ! p ◃∎
    =ₛ⟨  &  & !-∙-seq s ⟩
  seq-! s ∙▹ ! p ∎ₛ

∙-!-seq : {a a' : A} (s : a =-= a')
  → seq-! s =ₛ ! (↯ s) ◃∎
∙-!-seq s = !ₛ (!-∙-seq s)

!-=ₛ : {a a' : A} {s t : a =-= a'} (e : s =ₛ t)
  → seq-! s =ₛ seq-! t
!-=ₛ {s = s} {t = t} e =
  seq-! s
    =ₛ⟨ ∙-!-seq s ⟩
  ! (↯ s) ◃∎
    =ₛ₁⟨ ap ! (=ₛ-out e) ⟩
  ! (↯ t) ◃∎
    =ₛ⟨ !-∙-seq t ⟩
  seq-! t ∎ₛ

seq-!-inv-l : {a a' : A} (s : a =-= a')
  → seq-! s ∙∙ s =ₛ []
seq-!-inv-l s = =ₛ-in $
  ↯ (seq-! s ∙∙ s)
    =⟨ ↯-∙∙ (seq-! s) s ⟩
  ↯ (seq-! s) ∙ ↯ s
    =⟨ ap (_∙ ↯ s) (=ₛ-out (∙-!-seq s)) ⟩
  ! (↯ s) ∙ ↯ s
    =⟨ !-inv-l (↯ s) ⟩
  idp =∎

seq-!-inv-r : {a a' : A} (s : a =-= a')
  → s ∙∙ seq-! s =ₛ []
seq-!-inv-r s = =ₛ-in $
  ↯ (s ∙∙ seq-! s)
    =⟨ ↯-∙∙ s (seq-! s) ⟩
  ↯ s ∙ ↯ (seq-! s)
    =⟨ ap (↯ s ∙_) (=ₛ-out (∙-!-seq s)) ⟩
  ↯ s ∙ ! (↯ s)
    =⟨ !-inv-r (↯ s) ⟩
  idp =∎