Chuangjie Xu, 9 Sep 2014

\begin{code}

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

module CwF.Space.TypesAndTerms 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

\end{code}

Types and terms

\begin{code}

Type : Cxt → Set₁
Type (Γ , P , gc₁ , gc₂ , gc₃) =
 Σ \(A : Γ → Set) →
   Σ \(Q : (p : ₂ℕ → Γ) → p ∈ P → ((α : ₂ℕ) → A(p α)) → Set) →
      (∀(γ : Γ)(a : A γ) → (λ α → a) ∈ Q (λ α → γ) (gc₁ γ))
    × (∀(p : ₂ℕ → Γ)(pΓ : p ∈ P)(t : ₂ℕ → ₂ℕ)(tC : t ∈ C) →
        (q : (α : ₂ℕ) → A(p α)) → q ∈ Q p pΓ → (q ∘ t) ∈ Q (p ∘ t) (gc₂ p pΓ t tC))
    × (∀(ρ : ₂ → ₂ℕ → Γ)(fρ : ∀(i : ₂) → ρ i ∈ P) →
        (ζ : (i : ₂) → (α : ₂ℕ) → A(ρ i α)) → (∀ i → ζ i ∈ Q (ρ i) (fρ i)) →
        (▣ A ζ) ∈ Q (▢ ρ) (gc₃ ρ fρ))
    × (∀(p : ₂ℕ → Γ){pΓ pΓ' : p ∈ P}
        (q : (α : ₂ℕ) → A(p α)) → q ∈ Q p pΓ → q ∈ Q p pΓ')

Term : (Γ : Cxt) → Type Γ → Set
Term (Γ , P , _) (A , Q , _) =
  Σ \(u : (γ : Γ) → A γ) → ∀(p : ₂ℕ → Γ)(pΓ : p ∈ P) → (u ∘ p) ∈ Q p pΓ


DProbe : {Γ : Cxt} → (A : Type Γ) → _
DProbe (_ , Q , _) = Q

t⑴ : {Γ : Cxt} → (A : Type Γ) → _
t⑴ (_ , _ , c₁ , _) = c₁

t⑵ : {Γ : Cxt} → (A : Type Γ) → _
t⑵ (_ , _ , _ , c₂ , _) = c₂

t⑶ : {Γ : Cxt} → (A : Type Γ) → _
t⑶ (_ , _ , _ , _ , c₃ , _) = c₃

t⑷ : {Γ : Cxt} → (A : Type Γ) → _
t⑷ (_ , _ , _ , _ , _ , c₄) = c₄

\end{code}

Substitutions of types and of terms

\begin{code}

⟪_,_⟫_[_]ʸ : (Γ Δ : Cxt) → Type Γ → Sub Δ Γ → Type Δ
⟪ Γ , Δ ⟫ A [ (σ , cσ) ]ʸ = Aσ , Q , c₁ , c₂ , c₃ , c₄
 where
  Aσ : U Δ → Set
  Aσ δ = U A (σ δ)
  Q : (p : ₂ℕ → U Δ) → p ∈ Probe Δ → ((α : ₂ℕ) → Aσ(p α)) → Set
  Q p pΔ q = q ∈ DProbe A (σ ∘ p) (cσ p pΔ)
  c₁ : ∀(δ : U Δ)(a : Aσ δ) → (λ α → a) ∈ Q (λ α → δ) (s⑴ Δ δ)
  c₁ δ a = goal
   where
    known : (λ α → a) ∈ DProbe A (λ α → σ δ) (s⑴ Γ (σ δ))
    known = t⑴ A (σ δ) a
    goal : (λ α → a) ∈ DProbe A (λ α → σ δ) (cσ (λ α → δ) (s⑴ Δ δ))
    goal = t⑷ A (λ α → σ δ) (λ α → a) known
  c₂ : ∀(p : ₂ℕ → U Δ)(pΔ : p ∈ Probe Δ)(t : ₂ℕ → ₂ℕ)(tC : t ∈ C) →
        (q : (α : ₂ℕ) → Aσ(p α)) → q ∈ Q p pΔ → (q ∘ t) ∈ Q (p ∘ t) (s⑵ Δ p pΔ t tC)
  c₂ p pΔ t tC q qQ = goal
   where
    known : q ∘ t ∈ DProbe A (σ ∘ p ∘ t) (s⑵ Γ (σ ∘ p) (cσ p pΔ) t tC)
    known = t⑵ A (σ ∘ p) (cσ p pΔ) t tC q qQ
    goal : q ∘ t ∈ DProbe A (σ ∘ p ∘ t) (cσ (p ∘ t) (s⑵ Δ p pΔ t tC))
    goal = t⑷ A (σ ∘ p ∘ t) (q ∘ t) known
  c₃ : ∀(ρ : ₂ → ₂ℕ → U Δ)(fρ : ∀(i : ₂) → ρ i ∈ Probe Δ) →
        (ζ : (i : ₂) → (α : ₂ℕ) → Aσ(ρ i α)) → (∀(i : ₂) → ζ i ∈ Q (ρ i) (fρ i)) →
        (▣ Aσ ζ) ∈ Q (▢ ρ) (s⑶ Δ ρ fρ)
  c₃ ρ fρ ζ fζ = goal
   where
    σρ : ₂ → ₂ℕ → U Γ
    σρ i α = σ(ρ i α)
    fσρ : ∀(i : ₂) → σρ i ∈ Probe Γ
    fσρ i = cσ (ρ i) (fρ i)
    known : ▣ (U A) ζ ∈ DProbe A (▢ σρ) (s⑶ Γ σρ fσρ)
    known = t⑶ A σρ fσρ ζ fζ
    goal : ▣ (U A) ζ ∈ DProbe A (▢ σρ) (cσ (▢ ρ) (s⑶ Δ ρ fρ))
    goal = t⑷ A (▢ σρ) (▣ (U A) ζ) known
  c₄ : ∀(p : ₂ℕ → U Δ){pΔ pΔ' : p ∈ Probe Δ}(q : (α : ₂ℕ) → Aσ(p α)) →
        q ∈ Q p pΔ → q ∈ Q p pΔ'
  c₄ p q qQ = t⑷ A (σ ∘ p) q qQ


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

\end{code}

Equations

\begin{code}

-- A[1] = A
EqSub₀ : ∀(Γ : Cxt) (A : Type Γ)
       → U (⟪ Γ , Γ ⟫ A [ Ι Γ ]ʸ) ≡ U A
EqSub₀ Γ A = refl

-- A[σ][τ] = A[σ ∘ τ]
EqSub₁ : ∀(Γ Δ Θ : Cxt) (A : Type Γ) (σ : Sub Δ Γ) (τ : Sub Θ Δ)
       →   U (⟪ Δ , Θ ⟫ (⟪ Γ , Δ ⟫ A [ σ ]ʸ) [ τ ]ʸ)
         ≡ U (⟪ Γ , Θ ⟫ A [ ⟪ Γ , Δ , Θ ⟫ σ ○ τ ]ʸ)
EqSub₁ Γ Δ Θ A σ τ = refl

-- u[1] = u
EQSub₂ : ∀(Γ : Cxt) (A : Type Γ) (u : Term Γ A)
       → ⟪ Γ , Γ , A ⟫ u [ Ι Γ ]ᵐ ≡ u
EQSub₂ Γ A u = refl

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

\end{code}