Chuangjie Xu, November 2014

\begin{code}

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

module CwF.Sets.IdentityType where

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

\end{code}

Identity type

\begin{code}

Id : {Γ : Cxt} → (A : Type Γ) → Type (Γ ₊ A ₊ A [ ⓟ ]ʸ)
Id A ((γ , a) , b) = a ≡ b

Ⓡ : {Γ : Cxt} {A : Type Γ} → Sub (Γ ₊ A) (Γ ₊ A ₊ A [ ⓟ ]ʸ ₊ Id A)
Ⓡ (γ , a) = ((γ , a) , a) , refl

Ⓙ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A ₊ A [ ⓟ ]ʸ ₊ Id A)}
   → Term (Γ ₊ A) (B [ Ⓡ ]ʸ) → Term (Γ ₊ A ₊ A [ ⓟ ]ʸ ₊ Id A) B
Ⓙ {B = B} u (((γ , a) , b) , p) = J (λ x y q → B (((γ , x) , y) , q)) (λ x → u(γ , x)) a b p

\end{code}


\begin{code}

⟪_⟫Ⓡ : {Γ : Cxt} (A : Type Γ) → Sub (Γ ₊ A) (Γ ₊ A ₊ A [ ⓟ ]ʸ ₊ Id A)
⟪ A ⟫Ⓡ = Ⓡ

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

\end{code}

Computational rules

\begin{code}

-- p∘R=(1,q)
EqIT₁ : {Γ : Cxt} {A : Type Γ}
      → ⓟ ∘ ⟪ A ⟫Ⓡ ≡ ⟨ Ι , ⓠ ⟩
EqIT₁ = refl

-- J(u)[R] = u
EqIT₂ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A ₊ A [ ⓟ ]ʸ ₊ Id A)}
        {u : Term (Γ ₊ A) (B [ Ⓡ ]ʸ)}
      → (⟪ B ⟫Ⓙ u) [ Ⓡ ]ᵐ ≡ u
EqIT₂ = refl

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

⟨_∘p,q⟩ : {Γ : Cxt} {A : Type Γ} {Δ : Cxt}
        → (σ : Sub Δ Γ) → Sub (Δ ₊ A [ σ ]ʸ) (Γ ₊ A)
⟨ σ ∘p,q⟩ = ⟨ σ ∘ ⓟ , ⓠ ⟩

-- (J u)[⟨⟨⟨σ∘p,q⟩∘p,q⟩∘p,q⟩] = J(u[⟨σ∘p,q⟩])
EqIT₄ : {Γ : Cxt} {A : Type Γ} {B : Type (Γ ₊ A ₊ A [ ⓟ ]ʸ ₊ Id A)}
        {u : Term (Γ ₊ A) (B [ Ⓡ ]ʸ)} {Δ : Cxt} {σ : Sub Δ Γ}
      → (⟪ B ⟫Ⓙ u) [ ⟨ ⟨ ⟨ σ ∘ ⓟ , ⓠ ⟩ ∘ ⓟ , ⓠ ⟩ ∘ ⓟ , ⓠ ⟩ ]ᵐ
       ≡ Ⓙ (u [ ⟨ σ ∘ ⓟ , ⓠ ⟩ ]ᵐ)
EqIT₄ = refl 

\end{code}