Chuangjie Xu, 9 Sep 2014

\begin{code}

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

module CwF.Space.ContextComprehension where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingFunext.Space.Coverage
open import CwF.Space.Preliminaries
open import CwF.Space.Base
open import CwF.Space.TypesAndTerms

\end{code}

Context comprehension

\begin{code}

infixl 50 _₊_

_₊_ : (Γ : Cxt) → Type Γ → Cxt
(Γ , P , gc₁ , gc₂ , gc₃) ₊ (A , Q , ac₁ , ac₂ , ac₃ , _) =
ΣΓA , R , c₁ , c₂ , c₃
where
ΣΓA : Set
ΣΓA = Σ A
R : (₂ℕ → ΣΓA) → Set
R r = Σ \(rP : pr₁ ∘ r ∈ P) → (pr₂ ∘ r) ∈ Q (pr₁ ∘ r) rP
c₁ : ∀(w : ΣΓA) → (λ α → w) ∈ R
c₁ (γ , a) = rP , rQ
where
rP : (λ α → γ) ∈ P
rP = gc₁ γ
rQ : (λ α → a) ∈ Q (λ α → γ) rP
rQ = ac₁ γ a
c₂ : ∀(r : ₂ℕ → ΣΓA) → r ∈ R → ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → r ∘ t ∈ R
c₂ r (rP , rQ) t tC = rtP , rtQ
where
rtP : pr₁ ∘ r ∘ t ∈ P
rtP = gc₂ (pr₁ ∘ r) rP t tC
rtQ : pr₂ ∘ r ∘ t ∈ Q (pr₁ ∘ r ∘ t) rtP
rtQ = ac₂ (pr₁ ∘ r) rP t tC (pr₂ ∘ r) rQ
c₃ : ∀(ρ : ₂ → ₂ℕ → ΣΓA) → (∀(i : ₂) → ρ i ∈ R) → ▢ ρ ∈ R
c₃ ρ fρ = rP , rQ
where
rP : pr₁ ∘ ▢ ρ ∈ P
rP = gc₃ (λ i α → pr₁(ρ i α)) (pr₁ ∘ fρ)
rQ : pr₂ ∘ ▢ ρ ∈ Q (pr₁ ∘ ▢ ρ) rP
rQ = ac₃ (λ i α → pr₁(ρ i α)) (pr₁ ∘ fρ) (λ i α → pr₂(ρ i α)) (pr₂ ∘ fρ)

⟪_,_⟫p : (Γ : Cxt) (A : Type Γ) → Sub (Γ ₊ A) Γ
⟪ Γ , A ⟫p = pr₁ , (λ p pΓA → pr₁ pΓA)

⟪_⟫_[p]ʸ : (Γ : Cxt) → (A : Type Γ) → Type (Γ ₊ A)
⟪ Γ ⟫ A [p]ʸ = ⟪ Γ , Γ ₊ A ⟫ A [ ⟪ Γ , A ⟫p ]ʸ

⟪_,_⟫q : (Γ : Cxt) (A : Type Γ) → Term (Γ ₊ A) (⟪ Γ ⟫ A [p]ʸ)
⟪ Γ , A ⟫q = pr₂ , (λ p pΓA → pr₂ pΓA)

⟪_,_,_⟫⟨_,_⟩ : (Γ Δ : Cxt) (A : Type Γ)
→ (σ : Sub Δ Γ) → Term Δ (⟪ Γ , Δ ⟫ A [ σ ]ʸ)
→ Sub Δ (Γ ₊ A)
⟪ Γ , Δ , A ⟫⟨ (σ , cσ) , (u , cu) ⟩ = (σu , cσu)
where
σu : U Δ → Σ (U A)
σu δ = (σ δ , u δ)
cσu : ∀(p : ₂ℕ → U Δ) (pΔ : p ∈ Probe Δ) → σu ∘ p ∈ Probe (Γ ₊ A)
cσu p pΔ = (cσ p pΔ , cu p pΔ)

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

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

-- (p , q) = 1
EQCC₂ : ∀(Γ : Cxt) (A : Type Γ)
→ ⟪ Γ , Γ ₊ A , A ⟫⟨ ⟪ Γ , A ⟫p , ⟪ Γ , A ⟫q ⟩ ≡ Ι (Γ ₊ A)
EQCC₂ Γ A = refl

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

\end{code}

Substitution by a term

\begin{code}

⟪_,_⟫_[Ι,_]ʸ : (Γ : Cxt) (A : Type Γ)
→ (B : Type (Γ ₊ A)) → Term Γ A → Type Γ
⟪ Γ , A ⟫ B [Ι, u ]ʸ = ⟪ Γ ₊ A , Γ ⟫ B [ ⟪ Γ , Γ , A ⟫⟨ Ι Γ , u ⟩ ]ʸ

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

\end{code}

Partial substitution

\begin{code}

⟪_,_,_⟫_[_∘p,q]ʸ : (Γ Δ : Cxt) (A : Type Γ)
→ Type (Γ ₊ A) → (σ : Sub Δ Γ) → Type (Δ ₊ ⟪ Γ , Δ ⟫ A [ σ ]ʸ)
⟪ Γ , Δ , A ⟫ B [ σ ∘p,q]ʸ =
⟪ Γ ₊ A , ΔA[σ] ⟫ B [ ⟪ Γ , ΔA[σ] , A ⟫⟨ ⟪ Γ , Δ , ΔA[σ] ⟫ σ ○ ⟪ Δ , A[σ] ⟫p , ⟪ Δ , A[σ] ⟫q ⟩ ]ʸ
where
A[σ] : Type Δ
A[σ] = ⟪ Γ , Δ ⟫ A [ σ ]ʸ
ΔA[σ] : Cxt
ΔA[σ] = Δ ₊ A[σ]

⟪_,_,_,_⟫_[_∘p,q]ᵐ : (Γ Δ : Cxt) (A : Type Γ) (B : Type (Γ ₊ A))
→ (Term (Γ ₊ A) B) → (σ : Sub Δ Γ)
→ Term (Δ ₊ ⟪ Γ , Δ ⟫ A [ σ ]ʸ) (⟪ Γ , Δ , A ⟫ B [ σ ∘p,q]ʸ)
⟪ Γ , Δ , A , B ⟫ v [ σ ∘p,q]ᵐ =
⟪ Γ ₊ A , ΔA[σ] , B ⟫ v [ ⟪ Γ , ΔA[σ] , A ⟫⟨ ⟪ Γ , Δ , ΔA[σ] ⟫ σ ○ ⟪ Δ , A[σ] ⟫p , ⟪ Δ , A[σ] ⟫q ⟩ ]ᵐ
where
A[σ] : Type Δ
A[σ] = ⟪ Γ , Δ ⟫ A [ σ ]ʸ
ΔA[σ] : Cxt
ΔA[σ] = Δ ₊ A[σ]

\end{code}