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

open import Util.HoTT.HLevel.Core
open import Util.Prelude


infix  4 _<_
infixl 4 _∙_


mutual
  data Ctx : Set where
    [] : Ctx
    _∙_ : (Δ : Ctx) (n : Size Δ)  Ctx


  data Var : (Δ : Ctx)  Set where
    zero :  {Δ n}  Var (Δ  n)
    suc :  {Δ n} (x : Var Δ)  Var (Δ  n)


  data Size : (Δ : Ctx)  Set where
    var :  {Δ} (x : Var Δ)  Size Δ
     zero :  {Δ}  Size Δ
    suc :  {Δ} (n : Size Δ)  Size Δ


pattern  = suc 


variable
  Δ Ω Δ′ Ω′ Δ″ Ω″ : Ctx
  x y z : Var Δ
  n m o p b n′ m′ o′ p′ b′ : Size Δ


wk : Size Δ  Size (Δ  n)
wk (var x) = var (suc x)
wk  = 
wk zero = zero
wk (suc m) = suc (wk m)


bound : Var Δ  Size Δ
bound (zero {Δ} {n}) = wk n
bound (suc x) = wk (bound x)


data _<_ {Δ} : (n m : Size Δ)  Set where
  var : n  bound x  var x < n
  zero<suc : zero < suc n
  zero<∞ : zero < 
  suc<suc : (n<m : n < m)  suc n < suc m
  suc<∞ : (n<∞ : n < )  suc n < 
  <-trans : n < m  m < o  n < o
  <suc : n < suc n


data _≤_ {Δ} : (n m : Size Δ)  Set where
  reflexive : n  m  n  m
  <→≤ : n < m  n  m


pattern ≤-refl = reflexive refl

pattern v0 = var zero
pattern v1 = var (suc zero)
pattern v2 = var (suc (suc zero))


abstract
  n<m→n<Sm : n < m  n < suc m
  n<m→n<Sm n<m = <-trans n<m <suc


  n≤m→n<Sm : n  m  n < suc m
  n≤m→n<Sm ≤-refl = <suc
  n≤m→n<Sm (<→≤ n<m) = n<m→n<Sm n<m


  var<suc : var x  n  var x < suc n
  var<suc = n≤m→n<Sm


  ∞<suc :   n   < suc n
  ∞<suc = n≤m→n<Sm


  Sn<m→n<m : suc n < m  n < m
  Sn<m→n<m (suc<suc n<m) = <-trans n<m <suc
  Sn<m→n<m (suc<∞ n<∞) = n<∞
  Sn<m→n<m (<-trans Sn<o o<m) = <-trans (Sn<m→n<m Sn<o) o<m
  Sn<m→n<m <suc = <-trans <suc (suc<suc <suc)


  suc-inj-Var : Var.suc {n = n} x  suc y  x  y
  suc-inj-Var refl = refl


  suc≡-prop-Var : (p : Var.suc {n = n} x  suc y)  p  cong suc (suc-inj-Var p)
  suc≡-prop-Var refl = refl


  Var-IsSet : (p q : x  y)  p  q
  Var-IsSet {x = zero} {zero} refl refl = refl
  Var-IsSet {x = suc x} {suc .x} p refl
    = trans (suc≡-prop-Var p) (cong (cong suc) (Var-IsSet _ _))


  suc-inj-Size : Size.suc n  suc m  n  m
  suc-inj-Size refl = refl


  suc≡-prop-Size : (p : Size.suc n  suc m)  p  cong suc (suc-inj-Size p)
  suc≡-prop-Size refl = refl


  var-inj-Size : Size.var x  var y  x  y
  var-inj-Size refl = refl


  var≡-prop-Size : (p : Size.var x  var y)  p  cong var (var-inj-Size p)
  var≡-prop-Size refl = refl


  Size-IsSet : (p q : n  m)  p  q
  Size-IsSet {n = var x} {var .x} p refl
    = trans (var≡-prop-Size p) (cong (cong var) (Var-IsSet _ _))
  Size-IsSet {n = } {} refl refl = refl
  Size-IsSet {n = zero} {zero} refl refl = refl
  Size-IsSet {n = suc n} {suc .n} p refl
    = trans (suc≡-prop-Size p) (cong (cong suc) (Size-IsSet _ _))


  wk-resp-< : n < m  wk {n = o} n < wk m
  wk-resp-< (var p) = var (cong wk p)
  wk-resp-< zero<suc = zero<suc
  wk-resp-< zero<∞ = zero<∞
  wk-resp-< (suc<suc n<m) = suc<suc (wk-resp-< n<m)
  wk-resp-< (suc<∞ n<∞) = suc<∞ (wk-resp-< n<∞)
  wk-resp-< (<-trans n<o o<m) = <-trans (wk-resp-< n<o) (wk-resp-< o<m)
  wk-resp-< <suc = <suc