-- The purpose of this universe construction is to get some definitional
-- equalities in the model. Specifically, if we define ⟦σ⟧ : ⟦Δ⟧ → ⟦Ω⟧
-- (a functor) for the "canonical" notion of subsitution, then we have
-- ⟦Wk⟧ (δ , m) ≡ δ propositionally, but *not* definitionally. This then
-- complicates proofs involving ⟦Wk⟧, and similar for the other substitutions.

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

open import Relation.Binary using (IsEquivalence ; Setoid)

open import Source.Size
open import Source.Size.Substitution.Canonical as Can using (Sub⊢)
open import Util.Prelude

import Relation.Binary.Reasoning.Setoid as SetoidReasoning


infix   _≈_
infixl  _>>_


data Sub : (Δ Ω : Ctx) → Set where
  Id : Sub Δ Δ
  _>>_ : (σ : Sub Δ Δ′) (τ : Sub Δ′ Ω) → Sub Δ Ω
  Wk : Sub (Δ ∙ n) Δ
  Lift : (σ : Sub Δ Ω) → Sub (Δ ∙ m) (Ω ∙ n)
  Sing : (n : Size Δ) → Sub Δ (Δ ∙ m)
  Skip : Sub (Δ ∙ n ∙ v0) (Δ ∙ n)


⟨_⟩ : Sub Δ Ω → Can.Sub Δ Ω
⟨ Id ⟩ = Can.Id
⟨ σ >> τ ⟩ = ⟨ σ ⟩ Can.>> ⟨ τ ⟩
⟨ Wk ⟩ = Can.Wk
⟨ Lift σ ⟩ = Can.Lift ⟨ σ ⟩
⟨ Sing n ⟩ = Can.Sing n
⟨ Skip ⟩ = Can.Skip


subV : (σ : Sub Δ Ω) (x : Var Ω) → Size Δ
subV σ = Can.subV ⟨ σ ⟩


sub : (σ : Sub Δ Ω) (n : Size Ω) → Size Δ
sub σ = Can.sub ⟨ σ ⟩


pattern Lift′ σ ⊢n = Lift σ ⊢n refl


variable σ τ ι : Sub Δ Ω


data Sub⊢ᵤ : ∀ Δ Ω → Sub Δ Ω → Set where
  Id : Sub⊢ᵤ Δ Δ Id
  comp : (⊢σ : Sub⊢ᵤ Δ Δ′ σ) (⊢τ : Sub⊢ᵤ Δ′ Δ″ τ) → Sub⊢ᵤ Δ Δ″ (σ >> τ)
  Wk : Sub⊢ᵤ (Δ ∙ n) Δ Wk
  Lift : (⊢σ : Sub⊢ᵤ Δ Ω σ) (m≡n[σ] : m ≡ sub σ n)
    → Sub⊢ᵤ (Δ ∙ m) (Ω ∙ n) (Lift σ)
  Sing : (n<m : n < m) → Sub⊢ᵤ Δ (Δ ∙ m) (Sing n)
  Skip : Sub⊢ᵤ (Δ ∙ n ∙ v0) (Δ ∙ n) Skip


syntax Sub⊢ᵤ Δ Ω σ = σ ∶ Δ ⇒ᵤ Ω


⟨⟩-resp-⊢ : σ ∶ Δ ⇒ᵤ Ω → ⟨ σ ⟩ ∶ Δ ⇒ Ω
⟨⟩-resp-⊢ Id = Can.Id⊢
⟨⟩-resp-⊢ (comp ⊢σ ⊢τ) = Can.>>⊢ (⟨⟩-resp-⊢ ⊢σ) (⟨⟩-resp-⊢ ⊢τ)
⟨⟩-resp-⊢ Wk = Can.Wk⊢
⟨⟩-resp-⊢ (Lift ⊢σ m≡n[σ]) = Can.Lift⊢ (⟨⟩-resp-⊢ ⊢σ) m≡n[σ]
⟨⟩-resp-⊢ (Sing n<m) = Can.Sing⊢ n<m
⟨⟩-resp-⊢ Skip = Can.Skip⊢


record _≈_ (σ τ : Sub Δ Ω) : Set where
  constructor ≈⁺
  field ≈⁻ : ⟨ σ ⟩ ≡ ⟨ τ ⟩

open _≈_ public


≈-refl : σ ≈ σ
≈-refl = ≈⁺ refl


≈-sym : σ ≈ τ → τ ≈ σ
≈-sym (≈⁺ p) = ≈⁺ (sym p)


≈-trans : σ ≈ τ → τ ≈ ι → σ ≈ ι
≈-trans (≈⁺ p) (≈⁺ q) = ≈⁺ (trans p q)


≈-isEquivalence : IsEquivalence (_≈_ {Δ} {Ω})
≈-isEquivalence = record { refl = ≈-refl ; sym = ≈-sym ; trans = ≈-trans }


Sub-setoid : (Δ Ω : Ctx) → Setoid 0ℓ 0ℓ
Sub-setoid Δ Ω = record
  { Carrier = Sub Δ Ω
  ; _≈_ = _≈_
  ; isEquivalence = ≈-isEquivalence
  }


module ≈-Reasoning {Δ} {Ω} = SetoidReasoning (Sub-setoid Δ Ω)


abstract
  >>-resp-≈ : {σ σ′ : Sub Δ Δ′} {τ τ′ : Sub Δ′ Δ″}
    → σ ≈ σ′ → τ ≈ τ′ → σ >> τ ≈ σ′ >> τ′
  >>-resp-≈ (≈⁺ p) (≈⁺ q) = ≈⁺ (cong₂ Can._>>_ p q)


  Lift-resp-≈ : σ ≈ τ → Lift {m = m} {n} σ ≈ Lift τ
  Lift-resp-≈ (≈⁺ p) = ≈⁺ (cong Can.Lift p)


  sub-resp-< : σ ∶ Δ ⇒ᵤ Ω → n < m → sub σ n < sub σ m
  sub-resp-< ⊢σ = Can.sub-resp-< (⟨⟩-resp-⊢ ⊢σ)


mutual
  subV′ : Sub Δ Ω → Var Ω → Size Δ
  subV′ Id x = var x
  subV′ (σ >> τ) x = sub′ σ (subV′ τ x)
  subV′ Wk x = var (suc x)
  subV′ (Lift σ) zero = var zero
  subV′ (Lift σ) (suc x) = wk (subV′ σ x)
  subV′ (Sing n) zero = n
  subV′ (Sing n) (suc x) = var x
  subV′ Skip zero = var zero
  subV′ Skip (suc x) = var (suc (suc x))


  sub′ : Sub Δ Ω → Size Ω → Size Δ
  sub′ σ (var x) = subV′ σ x
  sub′ σ ∞ = ∞
  sub′ σ zero = zero
  sub′ σ (suc n) = suc (sub′ σ n)


  abstract
    subV′≡subV : ∀ (σ : Sub Δ Ω) x → subV′ σ x ≡ subV σ x
    subV′≡subV Id x = sym (Can.subV-Id x)
    subV′≡subV (σ >> τ) x
      = trans (sub′≡sub σ (subV′ τ x))
          (trans (cong (sub σ) (subV′≡subV τ x))
            (sym (Can.subV->> ⟨ σ ⟩ ⟨ τ ⟩ x)))
    subV′≡subV Wk x = sym (Can.sub-Wk (var x))
    subV′≡subV (Lift σ) zero = refl
    subV′≡subV (Lift σ) (suc x)
      = trans (cong wk (subV′≡subV σ x)) (sym (Can.subV-Weaken ⟨ σ ⟩ x))
    subV′≡subV (Sing n) zero = refl
    subV′≡subV (Sing n) (suc x) = sym (Can.subV-Id x)
    subV′≡subV Skip zero = refl
    subV′≡subV Skip (suc x) = sym
      (trans (Can.subV-Weaken (Can.Weaken Can.Id) x) (cong wk (Can.sub-Wk (var x))))


    sub′≡sub : ∀ (σ : Sub Δ Ω) n → sub′ σ n ≡ sub σ n
    sub′≡sub σ (var x) = subV′≡subV σ x
    sub′≡sub σ ∞ = refl
    sub′≡sub σ zero = refl
    sub′≡sub σ (suc n) = cong suc (sub′≡sub σ n)