Chuangjie Xu, November 2014

\begin{code}

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

module CwF.Sets.ContextComprehension where

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

\end{code}

Operations of context comprehension

\begin{code}

infixl  _₊_

_₊_ : (Γ : Cxt) → Type Γ → Cxt
Γ ₊ A = Σ A

ⓟ : {Γ : Cxt}{A : Type Γ} → Sub (Γ ₊ A) Γ
ⓟ (γ , a) = γ

ⓠ : {Γ : Cxt}{A : Type Γ} → Term (Γ ₊ A) (A [ ⓟ ]ʸ)
ⓠ (γ , a) = a

⟨_,_⟩ : {Γ Δ : Cxt} {A : Type Γ}
      → (σ : Sub Δ Γ) → Term Δ (A [ σ ]ʸ) → Sub Δ (Γ ₊ A)
⟨ σ , u ⟩ = λ δ → (σ δ , u δ)

\end{code}

Operations with explicit arguments

\begin{code}

⟪_⟫ⓟ : {Γ : Cxt}(A : Type Γ) → Sub (Γ ₊ A) Γ
⟪ A ⟫ⓟ = ⓟ

⟪_⟫ⓠ : {Γ : Cxt}(A : Type Γ) → Term (Γ ₊ A) (A [ ⓟ ]ʸ)
⟪ A ⟫ⓠ = ⓠ

⟪_⟫⟨_,_⟩ : {Γ Δ : Cxt} (A : Type Γ)
         → (σ : Sub Δ Γ) → Term Δ (A [ σ ]ʸ) → Sub Δ (Γ ₊ A)
⟪ A ⟫⟨ σ , u ⟩ = ⟨ σ , u ⟩

\end{code}

Computational rules

\begin{code}

-- p∘(σ,u) = σ
EqCC₀ : ∀{Γ Δ : Cxt}{A : Type Γ}{σ : Sub Δ Γ}{u : Term Δ (A [ σ ]ʸ)}
      → ⟪ A ⟫ⓟ ∘ ⟨ σ , u ⟩ ≡ σ
EqCC₀ = refl

-- q[(σ,u)] = q
EqCC₁ : ∀{Γ Δ : Cxt}{A : Type Γ}{σ : Sub Δ Γ}{u : Term Δ (A [ σ ]ʸ)}
      → ⟪ A ⟫ⓠ [ ⟨ σ , u ⟩ ]ᵐ ≡ u
EqCC₁ = refl

-- (p , q) = 1
EqCC₂ : ∀{Γ : Cxt}{A : Type Γ}
      → ⟨ ⟪ A ⟫ⓟ , ⟪ A ⟫ⓠ ⟩ ≡ Ι
EqCC₂ = refl

-- (σ , u) ∘ τ = (σ ∘ τ , u[τ])
EqCC₃ : {Γ Δ Θ : Cxt}{A : Type Γ}{σ : Sub Δ Γ}{u : Term Δ (A [ σ ]ʸ)}{τ : Sub Θ Δ}
      → ⟪ A ⟫⟨ σ , u ⟩ ∘ τ ≡ ⟨ σ ∘ τ , u [ τ ]ᵐ ⟩
EqCC₃ = refl

\end{code}