{-# OPTIONS --safe --without-K #-}
module Source.Size.Substitution.Theory where

open import Source.Size
open import Source.Size.Substitution.Canonical as SC using (Sub⊢)
open import Source.Size.Substitution.Universe as SU using (⟨_⟩ ; Sub⊢ᵤ)
open import Util.Prelude


record SubTheory (A : Ctx  Set) : Set where
  infixl 5 _[_] _[_]ᵤ
  field
    _[_] : A Ω  SC.Sub Δ Ω  A Δ
    [Id] :  {Δ} (a : A Δ)  a [ SC.Id ]  a
    [>>] :  {Δ Δ′ Δ″} (σ : SC.Sub Δ Δ′) (τ : SC.Sub Δ′ Δ″) a
       a [ σ SC.>> τ ]  a [ τ ] [ σ ]


  abstract
    [Id]′ :  {Δ} {σ : SC.Sub Δ Δ} a
       σ  SC.Id
       a [ σ ]  a
    [Id]′ a refl = [Id] a


    [>>]′ :  {Δ Δ′ Δ″} (ι : SC.Sub Δ Δ″) (σ : SC.Sub Δ Δ′) (τ : SC.Sub Δ′ Δ″) a
       ι  σ SC.>> τ
       a [ ι ]  a [ τ ] [ σ ]
    [>>]′ ι σ τ a refl = [>>] σ τ a


    [>>]″ :   {Δ Δ′ Δ″} (σ : SC.Sub Δ Δ′) (τ : SC.Sub Δ′ Δ″)
        (σ′ : SC.Sub Δ Ω) (τ′ : SC.Sub Ω Δ″) a
       σ SC.>> τ  σ′ SC.>> τ′
       a [ τ ] [ σ ]  a [ τ′ ] [ σ′ ]
    [>>]″ σ τ σ′ τ′ a eq
      = trans (sym ([>>] σ τ a)) (trans (cong  σ  a [ σ ]) eq) ([>>] σ′ τ′ a))


  _[_]ᵤ : A Ω  SU.Sub Δ Ω  A Δ
  a [ σ ]ᵤ = a [  σ  ]


  abstract
    []ᵤ-resp-≈ :  {Δ Ω} {σ τ : SU.Sub Δ Ω}
       σ SU.≈ τ
        a
       a [ σ ]ᵤ  a [ τ ]ᵤ
    []ᵤ-resp-≈ (SU.≈⁺ p) a = cong  σ  a [ σ ]) p


    [Id]ᵤ :  {Δ} (a : A Δ)  a [ SU.Id ]ᵤ  a
    [Id]ᵤ a = [Id] a


    [Id]ᵤ′ :  {Δ} {σ : SU.Sub Δ Δ} (a : A Δ)
       σ SU.≈ SU.Id
       a [ σ ]ᵤ  a
    [Id]ᵤ′ a (SU.≈⁺ p) = [Id]′ a p


    [>>]ᵤ :  {Δ Δ′ Δ″} (σ : SU.Sub Δ Δ′) (τ : SU.Sub Δ′ Δ″) (a : A Δ″)
       a [ σ SU.>> τ ]ᵤ  a [ τ ]ᵤ [ σ ]ᵤ
    [>>]ᵤ σ τ a = [>>] _ _ _


    [>>]ᵤ′ :  {Δ Δ′ Δ″} (ι : SU.Sub Δ Δ″) (σ : SU.Sub Δ Δ′) (τ : SU.Sub Δ′ Δ″) a
       ι SU.≈ σ SU.>> τ
       a [ ι ]ᵤ  a [ τ ]ᵤ [ σ ]ᵤ
    [>>]ᵤ′ ι σ τ a (SU.≈⁺ p) = [>>]′  ι   σ   τ  a p


    [>>]ᵤ″ :   {Δ Δ′ Δ″} (σ : SU.Sub Δ Δ′) (τ : SU.Sub Δ′ Δ″)
        (σ′ : SU.Sub Δ Ω) (τ′ : SU.Sub Ω Δ″) a
       σ SU.>> τ SU.≈ σ′ SU.>> τ′
       a [ τ ]ᵤ [ σ ]ᵤ  a [ τ′ ]ᵤ [ σ′ ]ᵤ
    [>>]ᵤ″ σ τ σ′ τ′ a (SU.≈⁺ p) = [>>]″  σ   τ   σ′   τ′  a p


open SubTheory {{...}} public


instance
  SubTheory-Size : SubTheory Size
  SubTheory-Size = record
    { _[_] = λ n σ  SC.sub σ n
    ; [Id] = λ n  SC.sub-Id n refl
    ; [>>] = λ σ τ n  SC.sub->> n refl
    }