Chuangjie Xu, November 2014

\begin{code}

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

module CwF.Sets.PiType where

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

\end{code}

Pi-type

\begin{code}

[Π] : {Γ : Cxt} → (A : Type Γ) → Type (Γ ₊ A) → Type Γ
[Π] A B = λ γ → (a : A γ) → B (γ , a)

⋏ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
  → Term (Γ ₊ A) B → Term Γ ([Π] A B)
⋏ v = λ γ a → v (γ , a)

app : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
    → Term Γ ([Π] A B) → (u : Term Γ A) → Term Γ (B [ ⟨ Ι , u ⟩ ]ʸ)
app w u = λ γ → w γ (u γ)

\end{code}

Computational rules

\begin{code}

-- app(λv,u) = v[(1,u)]
EqPT₁ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
        {u : Term Γ A} {v : Term (Γ ₊ A) B}
      → app (⋏ v) u ≡ v [ ⟨ Ι , u ⟩ ]ᵐ
EqPT₁ = refl

-- λ(app(w[p],q)) = w
EqPT₂ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
        {w : Term Γ ([Π] A B)}
      → ⋏ (app (w [ ⓟ ]ᵐ) ⓠ) ≡ w
EqPT₂ = refl

-- (ΠAB)[σ] = Π(A[σ])(B[(σ∘p,q)])
EqPT₃ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
        {Δ : Cxt} {σ : Sub Δ Γ}
      → ([Π] A B) [ σ ]ʸ ≡ [Π] (A [ σ ]ʸ) (B [ ⟨ σ ∘ ⓟ , ⓠ ⟩ ]ʸ)
EqPT₃ = refl

-- (λv)[σ] = λ(v[(σ∘p,q)])
EqPT₄ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
        {v : Term (Γ ₊ A) B} {Δ : Cxt} {σ : Sub Δ Γ}
      → (⋏ v) [ σ ]ᵐ ≡ ⋏ (v [ ⟨ σ ∘ ⓟ , ⓠ ⟩ ]ᵐ)
EqPT₄ = refl

-- app(w,u)[σ] = app(w[σ],u[σ])
EqPT₅ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
        {w : Term Γ ([Π] A B)} {u : Term Γ A} {Δ : Cxt} {σ : Sub Δ Γ}
      → (app w u) [ σ ]ᵐ ≡ app (w [ σ ]ᵐ) (u [ σ ]ᵐ)
EqPT₅ = refl

\end{code}