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  _[_]ʸ
infixl  _[_]ᵐ

_[_]ʸ : {Γ Δ : 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}