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