Chuangjie Xu, November 2014

\begin{code}

{-# OPTIONS --without-K #-}

module CwF.Sets.TypesAndTerms where

open import Preliminaries.SetsAndFunctions
open import CwF.Sets.Base

\end{code}

Types and Terms

\begin{code}

Type : Cxt  Set₁
Type Γ = Γ  Set

Term : (Γ : Cxt)  Type Γ  Set
Term Γ A = (γ : Γ)  A γ

\end{code}

Substitutions of types and of terms

\begin{code}

infixl 60 _[_]ʸ
infixl 35 _[_]ᵐ

_[_]ʸ : {Γ Δ : Cxt}  Type Γ  Sub Δ Γ  Type Δ
A [ σ  = A  σ

_[_]ᵐ : {Γ Δ : Cxt} {A : Type Γ}  Term Γ A  (σ : Sub Δ Γ)  Term Δ (A [ σ )
u [ σ ]ᵐ = u  σ

\end{code}

Computational rules

\begin{code}

-- A[1] = A
EqSub₀ : ∀{Γ : Cxt}{A : Type Γ}
        A [ Ι   A
EqSub₀ = refl

-- A[σ][τ] = A[σ ∘ τ]
EqSub₁ : ∀{Γ Δ Θ : Cxt}{A : Type Γ}{σ : Sub Δ Γ}{τ : Sub Θ Δ}
        A [ σ  [ τ   A [ σ  τ 
EqSub₁ = refl

-- u[1] = u
EqSub₂ : ∀{Γ : Cxt}{A : Type Γ}{u : Term Γ A}
        u [ Ι ]ᵐ  u
EqSub₂ = refl

-- u[σ][τ] = u[σ ∘ τ]
EqSub₃ : ∀{Γ Δ Θ : Cxt}{A : Type Γ}{u : Term Γ A}{σ : Sub Δ Γ}{τ : Sub Θ Δ}
        u [ σ ]ᵐ [ τ ]ᵐ   u [ σ  τ ]ᵐ
EqSub₃ = refl

\end{code}