module A202401.Kit2 where

open import A202401.Kit1 public


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

record RenSubKit1Params : Set₁ where
  constructor kit
  field
    subkit : SubKitParams
  open SubKitParams subkit public
  open SubKit subkit public hiding (subkit)
  field
    lidren  : ∀ {Γ A} (t : Γ ⊢ A) → ren id⊑ t ≡ t
    compren : ∀ {Γ Γ′ Γ″ A} (ϱ′ : Γ′ ⊑ Γ″) (ϱ : Γ ⊑ Γ′) (t : Γ ⊢ A) →
              ren (ϱ′ ∘⊑ ϱ) t ≡ (ren ϱ′ ∘ ren ϱ) t
    --        ren (ϱ ○ ϱ′) t ≡ (ren ϱ′ ∘ ren ϱ) t
    ridren  : ∀ {Γ Γ′ A} (ϱ : Γ ⊑ Γ′) (i : Γ ∋ A) → ren ϱ (var i) ≡ var (ren∋ ϱ i)
    ridsub  : ∀ {Γ Ξ A} (σ : Ξ ⊢§ Γ) (i : Γ ∋ A) → sub σ (var i) ≡ sub∋ σ i

module RenSubKit1 (¶ : RenSubKit1Params) where
  open RenSubKit1Params ¶
  rensubkit1 = ¶

  lidren§ : ∀ {Γ Δ} (τ : Γ ⊢§ Δ) →
            ren§ id⊑ τ ≡ τ
  --        ts ◐ id⊑ ≡ τ
  lidren§ ∙       = refl
  lidren§ (τ , t) = _,_ & lidren§ τ ⊗ lidren t

  -- Kovacs: assₛₑₑ
  compren§ : ∀ {Γ Γ′ Γ″ Δ} (ϱ′ : Γ′ ⊑ Γ″) (ϱ : Γ ⊑ Γ′) (τ : Γ ⊢§ Δ) →
             ren§ (ϱ′ ∘⊑ ϱ) τ ≡ (ren§ ϱ′ ∘ ren§ ϱ) τ
  --         τ ◐ (ϱ ○ ϱ′) ≡ (τ ◐ ϱ) ◐ ϱ′
  compren§ ϱ′ ϱ ∙       = refl
  compren§ ϱ′ ϱ (τ , t) = _,_ & compren§ ϱ′ ϱ τ ⊗ compren ϱ′ ϱ t

  eqwkren : ∀ {B Γ Γ′ A} (ϱ : Γ ⊑ Γ′) (t : Γ ⊢ A) →
            (ren (lift⊑ ϱ) ∘ wk) t ≡ (wk {B} ∘ ren ϱ) t
  eqwkren ϱ t = compren (lift⊑ ϱ) (wk⊑ id⊑) t ⁻¹
              ⋮ (flip ren t ∘ wk⊑) & (rid⊑ ϱ ⋮ lid⊑ ϱ ⁻¹)
              ⋮ compren (wk⊑ id⊑) ϱ t

  eqwkren§ : ∀ {B Γ Γ′ Δ} (ϱ : Γ ⊑ Γ′) (τ : Γ ⊢§ Δ) →
             (ren§ (lift⊑ ϱ) ∘ wk§) τ ≡ (wk§ {B} ∘ ren§ ϱ) τ
  --         (wk§ τ) ◐ (lift⊑ ϱ) ≡ wk§ {B} (τ ◐ ϱ)
  eqwkren§ ϱ ∙       = refl
  eqwkren§ ϱ (τ , t) = _,_ & eqwkren§ ϱ τ ⊗ eqwkren ϱ t

  eqliftren§ : ∀ {B Γ Γ′ Δ} (ϱ : Γ ⊑ Γ′) (τ : Γ ⊢§ Δ) →
               (ren§ (lift⊑ ϱ) ∘ lift§) τ ≡ (lift§ {B} ∘ ren§ ϱ) τ
  --           (lift§ τ) ◐ (lift⊑ ϱ) ≡ lift§ {B} (τ ◐ ϱ)
  eqliftren§ ϱ τ = ((ren§ (lift⊑ ϱ) ∘ wk§) τ ,_) & ridren (lift⊑ ϱ) zero
                 ⋮ (_, var zero) & eqwkren§ ϱ τ

  -- Kovacs: idlₛₑ; not really identity
  ridren§ : ∀ {Γ Γ′} (ϱ : Γ ⊑ Γ′) →
            ren§ ϱ id§ ≡ var§ ϱ
  --        id§ ◐ ϱ ≡ var§ ϱ
  ridren§ stop      = refl
  ridren§ (wk⊑ ϱ)   = (flip ren§ id§ ∘ wk⊑) & lid⊑ ϱ ⁻¹
                    ⋮ compren§ (wk⊑ id⊑) ϱ id§
                    ⋮ wk§ & ridren§ ϱ
  ridren§ (lift⊑ ϱ) = ((ren§ (lift⊑ ϱ) ∘ wk§) id§ ,_) & ridren (lift⊑ ϱ) zero
                    ⋮ (_, var zero) & (eqwkren§ ϱ id§ ⋮ wk§ & ridren§ ϱ)

  -- Kovacs: ∈-ₛ∘ₑ
  eqrensub∋ : ∀ {Γ Ξ Ξ′ A} (ϱ : Ξ ⊑ Ξ′) (σ : Ξ ⊢§ Γ) (i : Γ ∋ A) →
              sub∋ (ren§ ϱ σ) i ≡ (ren ϱ ∘ sub∋ σ) i
  --          sub∋ (σ ◐ ϱ) i ≡ (sub∋ σ ⨾ ren ϱ) i
  eqrensub∋ ϱ (σ , s) zero    = refl
  eqrensub∋ ϱ (σ , s) (wk∋ i) = eqrensub∋ ϱ σ i

  -- Kovacs: ∈-ₑ∘ₛ
  eqsubren∋ : ∀ {Γ Γ′ Ξ A} (σ : Ξ ⊢§ Γ′) (ϱ : Γ ⊑ Γ′) (i : Γ ∋ A) →
              sub∋ (get§ ϱ σ) i ≡ (sub∋ σ ∘ ren∋ ϱ) i
  --          sub∋ (ϱ ◑ σ) i ≡ (ren∋ ϱ ⨾ sub∋ σ) i
  eqsubren∋ ∙       stop      i       = refl
  eqsubren∋ (σ , s) (wk⊑ ϱ)   i       = eqsubren∋ σ ϱ i
  eqsubren∋ (σ , s) (lift⊑ ϱ) zero    = refl
  eqsubren∋ (σ , s) (lift⊑ ϱ) (wk∋ i) = eqsubren∋ σ ϱ i

  -- Kovacs: ∈-idₛ; not really identity
  idsub∋ : ∀ {Γ A} (i : Γ ∋ A) → sub∋ id§ i ≡ var i
  idsub∋ zero    = refl
  idsub∋ (wk∋ i) = eqrensub∋ (wk⊑ id⊑) id§ i
                 ⋮ wk & idsub∋ i
                 ⋮ ridren (wk⊑ id⊑) i
                 ⋮ (var ∘ wk∋) & idren∋ i

  -- Kovacs: ∈-∘ₛ; not really composition
  compsub∋ : ∀ {Γ Ξ Ξ′ A} (σ′ : Ξ′ ⊢§ Ξ) (σ : Ξ ⊢§ Γ) (i : Γ ∋ A) →
             sub∋ (sub§ σ′ σ) i ≡ (sub σ′ ∘ sub∋ σ) i
  --         sub∋ (σ ● σ′) i ≡ (sub∋ σ ⨾ sub σ′) i
  compsub∋ σ′ (σ , s) zero    = refl
  compsub∋ σ′ (σ , s) (wk∋ i) = compsub∋ σ′ σ i

  -- Kovacs: idlₑₛ
  lidget§ : ∀ {Γ Δ} (τ : Γ ⊢§ Δ) →
            get§ id⊑ τ ≡ τ
  --        id⊑ ◑ τ ≡ τ
  lidget§ ∙       = refl
  lidget§ (τ , t) = (_, t) & lidget§ τ

  compget§ : ∀ {Γ Δ Δ′ Δ″} (ϱ : Δ ⊑ Δ′) (ϱ′ : Δ′ ⊑ Δ″) (τ : Γ ⊢§ Δ″) →
             get§ (ϱ′ ∘⊑ ϱ) τ ≡ (get§ ϱ ∘ get§ ϱ′) τ
  --         (ϱ ○ ϱ′) ◑ τ ≡ ϱ ◑ (ϱ′ ◑ τ)
  compget§ ϱ         stop       ∙       = refl
  compget§ ϱ         (wk⊑ ϱ′)   (τ , t) = compget§ ϱ ϱ′ τ
  compget§ (wk⊑ ϱ)   (lift⊑ ϱ′) (τ , t) = compget§ ϱ ϱ′ τ
  compget§ (lift⊑ ϱ) (lift⊑ ϱ′) (τ , t) = (_, t) & compget§ ϱ ϱ′ τ

  -- Kovacs: assₑₛₑ
  eqrenget§ : ∀ {Γ Γ′ Δ Δ′} (ϱ : Γ ⊑ Γ′) (ϱ′ : Δ ⊑ Δ′) (τ : Γ ⊢§ Δ′) →
              (get§ ϱ′ ∘ ren§ ϱ) τ ≡ (ren§ ϱ ∘ get§ ϱ′) τ
  --          ϱ′ ◑ (τ ◐ ϱ) ≡ (ϱ′ ◑ τ) ◐ ϱ
  eqrenget§ ϱ stop       ∙       = refl
  eqrenget§ ϱ (wk⊑ ϱ′)   (τ , t) = eqrenget§ ϱ ϱ′ τ
  eqrenget§ ϱ (lift⊑ ϱ′) (τ , t) = (_, ren ϱ t) & eqrenget§ ϱ ϱ′ τ

  eqwkget§ : ∀ {B Γ Δ Δ′} (ϱ : Δ ⊑ Δ′) (τ : Γ ⊢§ Δ′) →
             (get§ (wk⊑ ϱ) ∘ lift§) τ ≡ (wk§ {B} ∘ get§ ϱ) τ
  --         (wk⊑ ϱ) ◑ (lift§ τ) ≡ wk§ {B} (ϱ ◑ τ)
  eqwkget§ ϱ τ = eqrenget§ (wk⊑ id⊑) ϱ τ

  eqliftget§ : ∀ {B Γ Δ Δ′} (ϱ : Δ ⊑ Δ′) (τ : Γ ⊢§ Δ′) →
               (get§ (lift⊑ ϱ) ∘ lift§) τ ≡ (lift§ {B} ∘ get§ ϱ) τ
  --           (lift⊑ ϱ) ◑ (lift§ τ) ≡ lift§ {B} (ϱ ◑ τ)
  eqliftget§ ϱ τ = (_, var zero) & eqwkget§ ϱ τ

  -- Kovacs: idrₑₛ; not really identity
  ridget§ : ∀ {Γ Γ′} (ϱ : Γ ⊑ Γ′) →
            get§ ϱ id§ ≡ var§ ϱ
  --        ϱ ◑ id§ ≡ var§ ϱ
  ridget§ stop      = refl
  ridget§ (wk⊑ ϱ)   = eqrenget§ (wk⊑ id⊑) ϱ id§ ⋮ wk§ & ridget§ ϱ
  ridget§ (lift⊑ ϱ) = (_, var zero) & (eqrenget§ (wk⊑ id⊑) ϱ id§ ⋮ wk§ & ridget§ ϱ)


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

record RenSubKit2Params : Set₁ where
  constructor kit
  field
    rensubkit1 : RenSubKit1Params
  open RenSubKit1Params rensubkit1 public
  open RenSubKit1 rensubkit1 public hiding (rensubkit1)
  field
    eqrensub : ∀ {Γ Ξ Ξ′ A} (ϱ : Ξ ⊑ Ξ′) (σ : Ξ ⊢§ Γ) (t : Γ ⊢ A) →
               sub (ren§ ϱ σ) t ≡ (ren ϱ ∘ sub σ) t
    --         sub (σ ◐ ϱ) t ≡ (sub σ ⨾ ren ϱ) t
    eqsubren : ∀ {Γ Γ′ Ξ A} (σ : Ξ ⊢§ Γ′) (ϱ : Γ ⊑ Γ′) (t : Γ ⊢ A) →
               sub (get§ ϱ σ) t ≡ (sub σ ∘ ren ϱ) t
    --         sub (ϱ ◑ σ) t ≡ (ren ϱ ⨾ sub σ) t
    lidsub   : ∀ {Γ A} (t : Γ ⊢ A) → sub id§ t ≡ t

module RenSubKit2 (¶ : RenSubKit2Params) where
  open RenSubKit2Params ¶
  rensubkit2 = ¶

  -- Kovacs: assₛₛₑ
  eqrensub§ : ∀ {Γ Ξ Ξ′ Δ} (ϱ : Ξ ⊑ Ξ′) (σ : Ξ ⊢§ Γ) (τ : Γ ⊢§ Δ) →
              sub§ (ren§ ϱ σ) τ ≡ (ren§ ϱ ∘ sub§ σ) τ
  --          τ ● (σ ◐ ϱ) ≡ (τ ● σ) ◐ ϱ
  eqrensub§ ϱ σ ∙       = refl
  eqrensub§ ϱ σ (τ , t) = _,_ & eqrensub§ ϱ σ τ ⊗ eqrensub ϱ σ t

  -- Kovacs: assₛₑₛ
  eqsubren§ : ∀ {Γ Γ′ Ξ Δ} (σ : Ξ ⊢§ Γ′) (ϱ : Γ ⊑ Γ′) (τ : Γ ⊢§ Δ) →
              sub§ (get§ ϱ σ) τ ≡ (sub§ σ ∘ ren§ ϱ) τ
  --          τ ● (ϱ ◑ σ) ≡ (τ ◐ ϱ) ● σ
  eqsubren§ σ ϱ ∙       = refl
  eqsubren§ σ ϱ (τ , t) = _,_ & eqsubren§ σ ϱ τ ⊗ eqsubren σ ϱ t

  -- Kovacs: idrₛ
  lidsub§ : ∀ {Γ Δ} (τ : Γ ⊢§ Δ) →
            sub§ id§ τ ≡ τ
  --        τ ● id§ ≡ τ
  lidsub§ ∙       = refl
  lidsub§ (τ , t) = _,_ & lidsub§ τ ⊗ lidsub t

  eqsub : ∀ {B Γ Ξ A} (σ : Ξ ⊢§ Γ) (s : Ξ ⊢ B) (t : Γ ⊢ A) →
          (sub (σ , s) ∘ wk) t ≡ sub σ t
  eqsub σ s t = eqsubren (σ , s) (wk⊑ id⊑) t ⁻¹
              ⋮ flip sub t & lidget§ σ

  eqsub§ : ∀ {B Γ Ξ Δ} (σ : Ξ ⊢§ Γ) (s : Ξ ⊢ B) (τ : Γ ⊢§ Δ) →
           (sub§ (σ , s) ∘ wk§) τ ≡ sub§ σ τ
  --       (wk§ τ) ● (σ , s) ≡ τ ● σ
  eqsub§ σ s ∙       = refl
  eqsub§ σ s (τ , t) = _,_ & eqsub§ σ s τ ⊗ eqsub σ s t

  eqwksub : ∀ {B Γ Ξ A} (σ : Ξ ⊢§ Γ) (t : Γ ⊢ A) →
            (sub (lift§ σ) ∘ wk) t ≡ (wk {B} ∘ sub σ) t
  eqwksub σ t = eqsubren (lift§ σ) (wk⊑ id⊑) t ⁻¹
              ⋮ flip sub t & (eqwkget§ id⊑ σ ⋮ wk§ & lidget§ σ)
              ⋮ eqrensub (wk⊑ id⊑) σ t

  eqwksub§ : ∀ {B Γ Ξ Δ} (σ : Ξ ⊢§ Γ) (τ : Γ ⊢§ Δ) →
             (sub§ (lift§ σ) ∘ wk§) τ ≡ (wk§ {B} ∘ sub§ σ) τ
  --         (wk§ τ) ● (lift§ σ) ≡ wk§ {B} (τ ● σ)
  eqwksub§ σ ∙       = refl
  eqwksub§ σ (τ , t) = _,_ & eqwksub§ σ τ ⊗ eqwksub σ t

  eqliftsub§ : ∀ {B Γ Ξ Δ} (σ : Ξ ⊢§ Γ) (τ : Γ ⊢§ Δ) →
               (sub§ (lift§ σ) ∘ lift§) τ ≡ (lift§ {B} ∘ sub§ σ) τ
  --           (lift§ τ) ● (lift§ σ) ≡ lift§ {B} (τ ● σ)
  eqliftsub§ σ τ = ((sub§ (lift§ σ) ∘ wk§) τ ,_) & ridsub (lift§ σ) zero
                 ⋮ (_, var zero) & eqwksub§ σ τ

  -- Kovacs: idlₛ
  ridsub§ : ∀ {Γ Ξ} (σ : Ξ ⊢§ Γ) →
            sub§ σ id§ ≡ σ
  --        id§ ● σ ≡ σ
  ridsub§ ∙       = refl
  ridsub§ (σ , s) = ((sub§ (σ , s) ∘ wk§) id§ ,_) & ridsub (σ , s) zero
                  ⋮ (_, s) & (eqsub§ σ s id§ ⋮ ridsub§ σ)


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

record RenSubKit3Params : Set₁ where
  constructor kit
  field
    rensubkit2 : RenSubKit2Params
  open RenSubKit2Params rensubkit2 public
  open RenSubKit2 rensubkit2 public hiding (rensubkit2)
  field
    compsub : ∀ {Γ Ξ Ξ′ A} (σ′ : Ξ′ ⊢§ Ξ) (σ : Ξ ⊢§ Γ) (t : Γ ⊢ A) →
              sub (sub§ σ′ σ) t ≡ (sub σ′ ∘ sub σ) t
    --        sub (σ ● σ′) t ≡ (sub σ ⨾ sub σ′) t

module RenSubKit3 (¶ : RenSubKit3Params) where
  open RenSubKit3Params ¶
  rensubkit3 = ¶

  -- Kovacs: assₛ
  asssub§ : ∀ {Γ Ξ Ξ′ Δ} (σ′ : Ξ′ ⊢§ Ξ) (σ : Ξ ⊢§ Γ) (τ : Γ ⊢§ Δ) →
            (sub§ σ′ ∘ sub§ σ) τ ≡ sub§ (sub§ σ′ σ) τ
  --        (τ ● σ) ● σ′ ≡ τ ● (σ ● σ′)
  asssub§ σ′ σ ∙       = refl
  asssub§ σ′ σ (τ , t) = _,_ & asssub§ σ′ σ τ ⊗ compsub σ′ σ t ⁻¹

  rencut : ∀ {Γ Γ′ A B} (ϱ : Γ ⊑ Γ′) (t₁ : Γ , A ⊢ B) (t₂ : Γ ⊢ A) →
           ren (lift⊑ ϱ) t₁ [ ren ϱ t₂ ] ≡ ren ϱ (t₁ [ t₂ ])
  rencut ϱ t₁ t₂ = eqsubren (id§ , ren ϱ t₂) (lift⊑ ϱ) t₁ ⁻¹
                 ⋮ (flip sub t₁ ∘ (_, ren ϱ t₂)) & (ridget§ ϱ ⋮ ridren§ ϱ ⁻¹)
                 ⋮ eqrensub ϱ (id§ , t₂) t₁

  subcut : ∀ {Γ Ξ A B} (σ : Ξ ⊢§ Γ) (t₁ : Γ , A ⊢ B) (t₂ : Γ ⊢ A) →
           sub (lift§ σ) t₁ [ sub σ t₂ ] ≡ sub σ (t₁ [ t₂ ])
  subcut σ t₁ t₂ = compsub (id§ , sub σ t₂) (lift§ σ) t₁ ⁻¹
                 ⋮ flip sub t₁ &
                     ( _,_ & ( eqsubren§ (id§ , sub σ t₂) (wk⊑ id⊑) σ ⁻¹
                             ⋮ flip sub§ σ & lidget§ id§
                             ⋮ lidsub§ σ
                             ⋮ ridsub§ σ ⁻¹
                             )
                           ⊗ ridsub (id§ , sub σ t₂) zero
                     )
                 ⋮ compsub σ (id§ , t₂) t₁


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