{-
2-POLYGRAPHS AND THEIR PROPERTIES

We implement the notion of 2-polygraph and some relatively simple
lemmas.
-}

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

open import Agda.Primitive
open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
import Cubical.Data.Empty
open import Cubical.Data.Sum
open import Cubical.Data.Nat

{- Note: The library file on wellfoundedness defines its own notion of
   relation. -}

open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded;
            Acc to isAcc;
            Rel to BinRel)

open import Cubical.Data.List.Base hiding (rev)
open import Cubical.Data.List.Properties
open import Cubical.Relation.Nullary.Base


module squier.polygraphs where

open import squier.graphclosures

private variable
  ℓ₀ ℓ₁ ℓ₂ ℓ₃ : Level

-- 2-polygraphs, type-theoretic definition
record 2-polygraph : Type (ℓ-suc (ℓ₀ ⊔ ℓ₁ ⊔ ℓ₂)) where
  field
    Σ₀ : Type ℓ₀
    _↝_ : BinRel Σ₀ ℓ₁
    _⇒_ : {y z : Σ₀} → BinRel (TransReflClosure (SymClosure _↝_) y z) ℓ₂

module polygraph-properties (p : 2-polygraph {ℓ₀} {ℓ₁} {ℓ₂}) where

  Σ₀ =  2-polygraph.Σ₀ p
  _↝_ = 2-polygraph._↝_ p
  _⇒_ = 2-polygraph._⇒_ p

  _↝*_ = TransReflClosure _↝_
  _↭_ = SymClosure _↝_
  _↭*_ = TransReflClosure _↭_

  {- Several auxiliary definitions: Creating a [local] peak or valley
     as a term of type y ↭* z -}

  mkLocalPeak : ∀ {y x z} → (x ↝ y) → (x ↝ z) → y ↭* z
  mkLocalPeak s t =  (rev s) ∷ᵗ (inj t) ∷ᵗ []ᵗ

  mkPeak : ∀ {y x z} → (x ↝* y) → (x ↝* z) → y ↭* z
  mkPeak x↝y x↝z = embed⁻ x↝y ++ᵗ embed⁺ x↝z

  mkValley : ∀ {y x' z} → (y ↝* x') → (z ↝* x') → y ↭* z
  mkValley y↝x z↝x = embed⁺ y↝x ++ᵗ (embed⁻ z↝x)

  data isIncreasing : ∀ {x y} → (x ↭* y) → Type (ℓ₀ ⊔ ℓ₁) where
    isIncreasing[]ᵗ : ∀ {x} → isIncreasing ([]ᵗ {a = x})
    isIncreasing∷ᵗ : ∀ {x y z}(s : x ↝ y){u : y ↭* z}
                        → isIncreasing u → isIncreasing (inj s ∷ᵗ u)

  data isDecreasing : ∀ {x y} → (x ↭* y) → Type (ℓ₀ ⊔ ℓ₁) where
    isDecreasing[]ᵗ : ∀ {x} → isDecreasing ([]ᵗ {a = x})
    isDecreasing∷ᵗ : ∀ {x y z}(s : y ↝ x){u : y ↭* z}
                        → isDecreasing u → isDecreasing (rev s ∷ᵗ u)

  _⇒*_ : {y z : Σ₀} → BinRel (y ↭* z) _
  _⇒*_ = TransReflClosure _⇒_

  _⇔_ : {y z : Σ₀} → BinRel (y ↭* z) _
  _⇔_ = SymClosure _⇒_

  _⇔*_ : {y z : Σ₀} → BinRel (y ↭* z) _
  _⇔*_ = TransReflClosure _⇔_

  {- Agda's standard notational trick: "equational reasoning" for
     rewrite sequences -}

  _⇒*⟨_⟩_ : {y z : Σ₀} {v w : y ↭* z}
            → (u : y ↭* z) → (u ⇒* v) → (v ⇒* w) → (u ⇒* w)
  u ⇒*⟨ uv ⟩ vw = uv ++ᵗ vw

  _⇒*∎ : {y z : Σ₀} (u : y ↭* z) → u ⇒* u
  u ⇒*∎ = []ᵗ

  infixr   _⇒*⟨_⟩_
  infix    _⇒*∎

  _⇔*⟨_⟩_ : {y z : Σ₀} {v w : y ↭* z}
            → (u : y ↭* z) → (u ⇔* v) → (v ⇔* w) → (u ⇔* w)
  u ⇔*⟨ uv ⟩ vw = uv ++ᵗ vw

  _⇔*∎ : {y z : Σ₀} (u : y ↭* z) → u ⇔* u
  u ⇔*∎ = []ᵗ

  infixr   _⇔*⟨_⟩_
  infix    _⇔*∎

  -- caveat: an empty reduction sequence is *not* necessarily equal to
  -- []ᵗ.

  ≡2⇔* : ∀ {x y} {u v : x ↭* y} → (u ≡ v) → (u ⇔* v)
  ≡2⇔* {u = u} p = subst (λ w → u ⇔* w) p []ᵗ

  -- having an order. We require transitivity explicitely; of course,
  -- we could omit it and work with the transitive closure whenever
  -- transitivity is required.
  hasOrder : ∀ {ℓ₃} → Type _
  hasOrder {ℓ₃} =
    Σ[ _>_ ∈ BinRel Σ₀ ℓ₃ ]
      (isTransitive _>_)
      ×
      ∀ {y z} → y ↝ z → y > z

  -- A collection of very easy (but useful) lemmas.

  module order (ord : hasOrder {ℓ₃}) where

    _>_ = fst ord
    trans = fst (snd ord)
    ↝2> = snd (snd ord)

    ↝*2≥ : {x z : Σ₀} (x↝*z : x ↝* z) → (lengthᵗ x↝*z ≡ ) ⊎ (x > z)
    ↝*2≥ []ᵗ = inl refl
    ↝*2≥ (x↝y ∷ᵗ y↝*z) with ↝*2≥ y↝*z
    ↝*2≥ {x} {z} (x↝y ∷ᵗ y↝*z) | inl y≡z =
         inr (subst (λ y → x > y) (length≡0 y≡z) (↝2> x↝y))
    ↝*2≥ {x} {z} (x↝y ∷ᵗ y↝*z) | inr y>z =
         inr (trans (↝2> x↝y) y>z)

    {-
    -- maybe don't even need this
    ↝⁺2> : {x z : Σ₀} (x↝*z : x ↝* z) → ¬ (lengthᵗ x↝*z ≡ 0) → x > z
    ↝⁺2> x↝*z length≠0 with ↝*2≥ x↝*z
    ↝⁺2> _ l≠0 | inl l≡0 = Cubical.Data.Empty.rec (l≠0 l≡0)
    ↝⁺2> _ _   | inr x>z = x>z
    -}

  -- a.k.a. "isTerminating"
  isNoetherian : ∀ {ℓ₃} → hasOrder {ℓ₃} → Type _
  isNoetherian (_>_ , _) = isWellFounded λ x y → y > x

  -- ### Closure of 2-morphisms under congruence

  {- "Closure under congurence" means that, if the two-dimensional shape in

                  ___u___
            w₀   /       \    w₁
       x₀ ----- x         y ----- y₀
                 \_______/
                     v

     has a filler, then also the shape

         _________w₀∙u∙w₁_______
        /                       \
       x₀                        y₀
        \_________w₀∙v∙w₁_______/

    Here, w₀, u, v, w₁ are in ⇔*.
    The goal is to prove some simple lemmas that make
    it easy to check the condition in the application.
  -}

  -- standard formulation
  ⇔*isCongrClosed = ∀ {x₀ x y y₀} (w₀ : x₀ ↭* x) (u v : x ↭* y) (w₁ : y ↭* y₀)
                      → (u ⇔* v) → (w₀ ++ᵗ u ++ᵗ w₁) ⇔* (w₀ ++ᵗ v ++ᵗ w₁)

  -- simplified, only one side:
  ⇔*isCongrClosedR = ∀ {x₀ x y} (w₀ : x₀ ↭* x) (u v : x ↭* y)
                      → (u ⇔* v) → (w₀ ++ᵗ u) ⇔* (w₀ ++ᵗ v)

  ⇔*isCongrClosedL = ∀ {x y y₀} (u v : x ↭* y) (w₁ : y ↭* y₀)
                      → (u ⇔* v) → (u ++ᵗ w₁) ⇔* (v ++ᵗ w₁)

  -- of course we get:
  ⇔*cc2ccr : ⇔*isCongrClosed → ⇔*isCongrClosedR
  ⇔*cc2ccr cc w₀ u v α =
    (w₀ ++ᵗ u)
      ⇔*⟨ ≡2⇔* (sym (cong (λ u' → w₀ ++ᵗ u') ++ᵗ[]ᵗ)) ⟩
    (w₀ ++ᵗ u ++ᵗ []ᵗ)
      ⇔*⟨ cc w₀ u v []ᵗ α ⟩
    (w₀ ++ᵗ v ++ᵗ []ᵗ)
      ⇔*⟨ ≡2⇔* (cong (λ v' → w₀ ++ᵗ v') ++ᵗ[]ᵗ) ⟩
    (w₀ ++ᵗ v)
      ⇔*∎

  ⇔*cc2ccl : ⇔*isCongrClosed → ⇔*isCongrClosedL
  ⇔*cc2ccl cc = cc []ᵗ
  {- Long (more readable?) version:
  ⇔*cc2ccl cc u v w₁ α =
    (u ++ᵗ w₁)
      ⇔*⟨ cc []ᵗ u v w₁ α ⟩
    (v ++ᵗ w₁)
      ⇔*∎
  -}


  -- ABANDONED CODE:
  -- The following approaches lead to generalisations or are
  -- improvements, but they are not required for the current
  -- development.

  {-
  -- stronger version:
  ⇒*isCongrClosed = ∀ {x₀ x y y₀} (w₀ : x₀ ↭* x)
                      → (u v : x ↭* y) (w₁ : y ↭* y₀)
                      → (u ⇒* v) → (w₀ ++ᵗ u ++ᵗ w₁) ⇒* (w₀ ++ᵗ v ++ᵗ w₁)

  -- conditions that are actually stronger but easier to check:
  isCC-left = ∀ {x₀ x y} (w₀ : x₀ ↭ x) (u v : x ↭* y)
                → (u ⇒ v) → (w₀ ∷ᵗ u) ⇒ (w₀ ∷ᵗ v)

  -- now, we need only ONE of these two:
  -- "boring" version
  isCC-right = ∀ {x y y₀} (u v : x ↭* y) (w₁ : y ↭ y₀)
                 → (u ⇒ v) → (u ++ᵗ w₁ ∷ᵗ []ᵗ) ⇒ (v ++ᵗ w₁ ∷ᵗ []ᵗ)
  -- maybe more useful?
  isReversable = ∀ {x y} (u v : x ↭* y)
                   → (u ⇒ v) → (reverse u ⇒ reverse v)

  -- We should really use that * is a monad. But probably these arguments
  -- should be factored out anyway in a future improvement.

  module rev-extend-aux (cc-l : isCC-left) (cc-rev : isReversable) where

    add-left : ∀ {x₀ x y} (w : x₀ ↭* x) (u v : x ↭* y)
                → (u ⇒ v) → (w ++ᵗ u) ⇒ (w ++ᵗ v)
    add-left []ᵗ u v u⇒v = u⇒v
    add-left (w₀ ∷ᵗ w) u v u⇒v = cc-l w₀ _ _ (add-left w u v u⇒v)

    cc : ⇒*isCongrClosed
    cc w₀ u v w₁ u⇒v = {!add-left w₀ u v!}

  reversable⇒extendCongrClosed : isCC-left → isReversable → ⇒*isCongrClosed
  reversable⇒extendCongrClosed = rev-extend-aux.cc

  -}