Chuangjie Xu, November 2014

\begin{code}

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

module CwF.Sets.SigmaType where

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

\end{code}

Σ-type

\begin{code}

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

<_,_> : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
      → (u : Term Γ A) → Term Γ (B [ ⟨ Ι , u ⟩ ]ʸ) → Term Γ ([Σ] A B)
< u , v > = λ γ → (u γ , v γ)

pr1 : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
    → Term Γ ([Σ] A B) → Term Γ A
pr1 w = pr₁ ∘ w

pr2 : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
    → (w : Term Γ ([Σ] A B)) → Term Γ (B [ ⟨ Ι , pr1 w ⟩ ]ʸ)
pr2 w = pr₂ ∘ w

\end{code}

\begin{code}

⟪_⟫<_,_> : {Γ : Cxt} {A : Type Γ} (B : Type (Γ ₊ A))
         → (u : Term Γ A) → Term Γ (B [ ⟨ Ι , u ⟩ ]ʸ) → Term Γ ([Σ] A B)
⟪ B ⟫< u , v > = < u , v >

⟪_⟫pr1 : {Γ : Cxt} {A : Type Γ} (B : Type (Γ ₊ A))
       → Term Γ ([Σ] A B) → Term Γ A
⟪ B ⟫pr1 = pr1

⟪_⟫pr2 : {Γ : Cxt} {A : Type Γ} (B : Type (Γ ₊ A))
       → (w : Term Γ ([Σ] A B)) → Term Γ (B [ ⟨ Ι , pr1 w ⟩ ]ʸ)
⟪ B ⟫pr2 = pr2

\end{code}

Computational rules

\begin{code}

-- (pr₁(w), pr₂(w)) = w
EqST₁ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
        {w : Term Γ ([Σ] A B)}
      → < pr1 w , pr2 w > ≡ w
EqST₁ = refl

-- pr₁(u,v) = u
EqST₂ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
        {u : Term Γ A} {v : Term Γ (B [ ⟨ Ι , u ⟩ ]ʸ)}
      → ⟪ B ⟫pr1 < u , v > ≡ u
EqST₂ = refl

-- pr₂(u,v) = v
EqST₃ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
        {u : Term Γ A} {v : Term Γ (B [ ⟨ Ι , u ⟩ ]ʸ)}
      → ⟪ B ⟫pr2 < u , v > ≡ v
EqST₃ = refl

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

-- (u,v)[σ] = (u[σ],v[σ])
EqST₅ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
        {u : Term Γ A} {v : Term Γ (B [ ⟨ Ι , u ⟩ ]ʸ)}
        {Δ : Cxt} {σ : Sub Δ Γ}
      → ⟪ B ⟫< u , v > [ σ ]ᵐ ≡ < u [ σ ]ᵐ , v [ σ ]ᵐ >
EqST₅ = refl

-- pr₁(w)[σ] = pr₁(w[σ])
EqST₆ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
        {w : Term Γ ([Σ] A B)} {Δ : Cxt} {σ : Sub Δ Γ}
      → (pr1 w) [ σ ]ᵐ ≡ pr1 (w [ σ ]ᵐ)
EqST₆ = refl

-- pr₂(w)[σ] = pr₂(w[σ])
EqST₇ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A)}
        {w : Term Γ ([Σ] A B)} {Δ : Cxt} {σ : Sub Δ Γ}
      → (pr2 w) [ σ ]ᵐ ≡ pr2 (w [ σ ]ᵐ)
EqST₇ = refl

\end{code}