----------------------------------------------------------------------------------------------------

-- first-order renamings

module A202401.FOR {𝓍} {X : Set 𝓍} where

open import A202401.DBI public


----------------------------------------------------------------------------------------------------

infix  _⊑_
data _⊑_ : Rist X → Rist X → Set 𝓍 where
  ∙   : ∀ {Γ} → ∙ ⊑ Γ
  _,_ : ∀ {Γ Γ′ A} (ϱ : Γ ⊑ Γ′) (i : Γ′ ∋ A) → Γ , A ⊑ Γ′

stop : ∙ ⊑ ∙
stop = ∙

wk⊑ : ∀ {B Γ Γ′} → Γ ⊑ Γ′ → Γ ⊑ Γ′ , B
wk⊑ ∙       = ∙
wk⊑ (ϱ , i) = wk⊑ ϱ , wk∋ i

lift⊑ : ∀ {B Γ Γ′} → Γ ⊑ Γ′ → Γ , B ⊑ Γ′ , B
lift⊑ ϱ = wk⊑ ϱ , zero

id⊑ refl⊑ : ∀ {Γ} → Γ ⊑ Γ
id⊑ {∙}    = ∙
id⊑ {Γ , A} = lift⊑ id⊑
refl⊑ = id⊑


----------------------------------------------------------------------------------------------------

ren∋ : ∀ {Γ Γ′ A} → Γ ⊑ Γ′ → Γ ∋ A → Γ′ ∋ A
ren∋ (ϱ , j) zero    = j
ren∋ (ϱ , j) (wk∋ i) = ren∋ ϱ i

eqwkren∋ : ∀ {B Γ Γ′ A} (ϱ : Γ ⊑ Γ′) (i : Γ ∋ A) →
           ren∋ (wk⊑ ϱ) i ≡ (wk∋ {B = B} ∘ ren∋ ϱ) i
eqwkren∋ (ϱ , j) zero    = refl
eqwkren∋ (ϱ , j) (wk∋ i) = eqwkren∋ ϱ i

idren∋ : ∀ {Γ A} (i : Γ ∋ A) → ren∋ id⊑ i ≡ i
idren∋ zero    = refl
idren∋ (wk∋ i) = eqwkren∋ id⊑ i ⋮ wk∋ & idren∋ i

_∘⊑_ : ∀ {Γ Γ′ Γ″} → Γ′ ⊑ Γ″ → Γ ⊑ Γ′ → Γ ⊑ Γ″
ϱ′ ∘⊑ ∙       = ∙
ϱ′ ∘⊑ (ϱ , i) = (ϱ′ ∘⊑ ϱ) , ren∋ ϱ′ i

trans⊑ _○_ : ∀ {Γ Γ′ Γ″} → Γ ⊑ Γ′ → Γ′ ⊑ Γ″ → Γ ⊑ Γ″
trans⊑ = flip _∘⊑_
_○_ = trans⊑

compren∋ : ∀ {Γ Γ′ Γ″ A} (ϱ′ : Γ′ ⊑ Γ″) (ϱ : Γ ⊑ Γ′) (i : Γ ∋ A) →
           ren∋ (ϱ′ ∘⊑ ϱ) i ≡ (ren∋ ϱ′ ∘ ren∋ ϱ) i
compren∋ (ϱ′ , j′) (ϱ , j) zero    = refl
compren∋ (ϱ′ , j′) (ϱ , j) (wk∋ i) = compren∋ (ϱ′ , j′) ϱ i


----------------------------------------------------------------------------------------------------

lid⊑ : ∀ {Γ Γ′} (ϱ : Γ ⊑ Γ′) → id⊑ ∘⊑ ϱ ≡ ϱ
lid⊑ ∙       = refl
lid⊑ (ϱ , i) = _,_ & lid⊑ ϱ ⊗ idren∋ i

eq⊑ : ∀ {B Γ Γ′ Γ″} (ϱ′ : Γ′ ⊑ Γ″) (i′ : Γ″ ∋ B) (ϱ : Γ ⊑ Γ′) →
      (ϱ′ , i′) ∘⊑ wk⊑ ϱ ≡ ϱ′ ∘⊑ ϱ
eq⊑ ϱ′ i′ ∙       = refl
eq⊑ ϱ′ i′ (ϱ , i) = (_, ren∋ ϱ′ i) & eq⊑ ϱ′ i′ ϱ

eqwk⊑ : ∀ {B Γ Γ′ Γ″} (ϱ′ : Γ′ ⊑ Γ″) (ϱ : Γ ⊑ Γ′) →
        lift⊑ ϱ′ ∘⊑ wk⊑ ϱ ≡ wk⊑ {B} (ϱ′ ∘⊑ ϱ)
eqwk⊑ ϱ′ ∙       = refl
eqwk⊑ ϱ′ (ϱ , i) = _,_ & eqwk⊑ ϱ′ ϱ ⊗ eqwkren∋ ϱ′ i

eqlift⊑ : ∀ {B Γ Γ′ Γ″} (ϱ′ : Γ′ ⊑ Γ″) (ϱ : Γ ⊑ Γ′) →
          lift⊑ ϱ′ ∘⊑ lift⊑ ϱ ≡ lift⊑ {B} (ϱ′ ∘⊑ ϱ)
eqlift⊑ ϱ′ ∙       = refl
eqlift⊑ ϱ′ (ϱ , i) = (_, zero) & eqwk⊑ ϱ′ (ϱ , i)

rid⊑ : ∀ {Γ Γ′} (ϱ : Γ ⊑ Γ′) → ϱ ∘⊑ id⊑ ≡ ϱ
rid⊑ ∙       = refl
rid⊑ (ϱ , i) = (_, i) & (eq⊑ ϱ i id⊑ ⋮ rid⊑ ϱ)

ass⊑ : ∀ {Γ Γ′ Γ″ Γ‴} (ϱ″ : Γ″ ⊑ Γ‴) (ϱ′ : Γ′ ⊑ Γ″) (ϱ : Γ ⊑ Γ′) →
       ϱ″ ∘⊑ (ϱ′ ∘⊑ ϱ) ≡ (ϱ″ ∘⊑ ϱ′) ∘⊑ ϱ
ass⊑ ϱ″ ϱ′ ∙       = refl
ass⊑ ϱ″ ϱ′ (ϱ , i) = _,_ & ass⊑ ϱ″ ϱ′ ϱ ⊗ compren∋ ϱ″ ϱ′ i ⁻¹


----------------------------------------------------------------------------------------------------