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  _₊_

_₊_ : (Γ : 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}