{-# 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  _[_] _[_]ᵤ
  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
    }