unary-cbv.agda

module unary-cbv(Σ₀ : Set) where
open import Relation.Binary.PropositionalEquality

data Type : Set where
  base : Σ₀ -> Type
  □    : Type -> Type

Sig₁ : Set₁
Sig₁ = Type -> Type -> Set

module ucbv1 (Σv : Sig₁) (Σt : Sig₁) where
  data _⇒v_ : Type -> Type -> Set
  data _⇒t_ : Type -> Type -> Set
  data _⇒v_ where
    base : ∀ {A B C} -> Σv B C -> A ⇒v B -> A ⇒v C
    var  : ∀ {A} -> A ⇒v A
    -- thunk
    □-I  : ∀ {A B} -> A ⇒t B -> A ⇒v □ B
  data _⇒t_ where
    base : ∀ {A B C D} -> Σt B C -> A ⇒v B -> C ⇒t D -> A ⇒t D
    ret  : ∀ {A B} -> A ⇒v B -> A ⇒t B

  tvar : ∀ {A} -> A ⇒t A
  tvar = ret var

  _⟨_⟩v : ∀ {A B C} -> B ⇒v C -> A ⇒v B -> A ⇒v C
  _⟨_⟩t : ∀ {A B C} -> B ⇒t C -> A ⇒v B -> A ⇒t C
  _to_  : ∀ {A B C} -> A ⇒t B -> B ⇒t C -> A ⇒t C
  base f v ⟨ u ⟩v = base f (v ⟨ u ⟩v)
  var ⟨ u ⟩v = u
  □-I t ⟨ u ⟩v = □-I (t ⟨ u ⟩t)
  base p u t ⟨ v ⟩t = base p (u ⟨ v ⟩v) t
  ret u ⟨ v ⟩t = ret (u ⟨ v ⟩v) 
  base p v s to t = base p v (s to t)
  ret v to t = t ⟨ v ⟩t

  subst-v-id-inp : ∀ {A B} (v : A ⇒v B) -> v ⟨ var ⟩v ≡ v
  subst-t-id-inp : ∀ {A B} (t : A ⇒t B) -> t ⟨ var ⟩t ≡ t
  subst-v-id-inp (base x v) = cong (base x) (subst-v-id-inp v)
  subst-v-id-inp var = refl
  subst-v-id-inp (□-I t) = cong □-I (subst-t-id-inp t)

  subst-t-id-inp (base p v t) = cong (\v -> base p v t) (subst-v-id-inp v)
  subst-t-id-inp (ret v) = cong ret (subst-v-id-inp v)

  subst-to-id-inp : ∀ {A B} (t : A ⇒t B) -> ret var to t ≡ t
  subst-to-id-inp t = subst-t-id-inp t

  subst-v-id-outp : ∀ {A B} (v : A ⇒v B) -> var ⟨ v ⟩v ≡ v
  subst-to-id-outp : ∀ {A B} (t : A ⇒t B) -> t to ret var ≡ t
  subst-v-id-outp v = refl
  subst-to-id-outp (base p v t) = cong (\t -> base p v t) (subst-to-id-outp t)
  subst-to-id-outp (ret v) = refl

  subst-v-assoc : ∀ {A0 A1 A2 A3} (v2 : A2 ⇒v A3)(v1 : A1 ⇒v A2)(v0 : A0 ⇒v A1) -> v2 ⟨ v1 ⟨ v0 ⟩v ⟩v ≡ (v2 ⟨ v1 ⟩v) ⟨ v0 ⟩v
  subst-tvv-assoc : ∀ {A0 A1 A2 A3} (t2 : A2 ⇒t A3)(v1 : A1 ⇒v A2)(v0 : A0 ⇒v A1) -> t2 ⟨ v1 ⟨ v0 ⟩v ⟩t ≡ (t2 ⟨ v1 ⟩t) ⟨ v0 ⟩t
  subst-v-assoc (base f v2) v1 v0 = cong (λ v → base f v) (subst-v-assoc v2 v1 v0)
  subst-v-assoc var v1 v0 = refl
  subst-v-assoc (□-I t2) v1 v0 = cong □-I (subst-tvv-assoc t2 v1 v0)

  subst-tvv-assoc (base p v2 t2) v1 v0 = cong (λ v → base p v t2) (subst-v-assoc v2 v1 v0)
  subst-tvv-assoc (ret v2) v1 v0 = cong ret (subst-v-assoc v2 v1 v0)

  subst-ttv-assoc : ∀ {A0 A1 A2 A3} (t2 : A2 ⇒t A3)(t1 : A1 ⇒t A2)(v0 : A0 ⇒v A1) -> (t1 ⟨ v0 ⟩t) to t2 ≡ (t1 to t2) ⟨ v0 ⟩t
  subst-ttv-assoc t2 (base x x₁ t1) v0 = refl
  subst-ttv-assoc t2 (ret v1) v0 = subst-tvv-assoc t2 v1 v0

  subst-to-assoc : ∀ {A0 A1 A2 A3} (t2 : A2 ⇒t A3)(t1 : A1 ⇒t A2)(t0 : A0 ⇒t A1) -> (t0 to t1) to t2 ≡ t0 to (t1 to t2)
  subst-to-assoc t2 t1 (base p v t0) = cong (λ t → base p v t) (subst-to-assoc t2 t1 t0)
  subst-to-assoc t2 t1 (ret v0) = subst-ttv-assoc t2 t1 v0