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)(t : ₂ℕ  ₂ℕ)(tC : t  C) 
        (q : (α : ₂ℕ)  A(p α))  q  Q p   (q  t)  Q (p  t) (gc₂ p  t tC))
    × (∀(ρ :   ₂ℕ  Γ)( : ∀(i : )  ρ i  P) 
        (ζ : (i : )  (α : ₂ℕ)  A(ρ i α))  (∀ i  ζ i  Q (ρ i) ( i)) 
        ( A ζ)  Q ( ρ) (gc₃ ρ ))
    × (∀(p : ₂ℕ  Γ){ pΓ' : p  P}
        (q : (α : ₂ℕ)  A(p α))  q  Q p   q  Q p pΓ')

Term : (Γ : Cxt)  Type Γ  Set
Term (Γ , P , _) (A , Q , _) =
  Σ \(u : (γ : Γ)  A γ)  ∀(p : ₂ℕ  Γ)( : p  P)  (u  p)  Q 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 [ (σ , )  =  , Q , c₁ , c₂ , c₃ , c₄
 where
   : U Δ  Set
   δ = U A (σ δ)
  Q : (p : ₂ℕ  U Δ)  p  Probe Δ  ((α : ₂ℕ)  (p α))  Set
  Q p  q = q  DProbe A (σ  p) ( p )
  c₁ : ∀(δ : U Δ)(a :  δ)   α  a)  Q  α  δ) (s⑴ Δ δ)
  c₁ δ a = goal
   where
    known :  α  a)  DProbe A  α  σ δ) (s⑴ Γ (σ δ))
    known = t⑴ A (σ δ) a
    goal :  α  a)  DProbe A  α  σ δ) (  α  δ) (s⑴ Δ δ))
    goal = t⑷ A  α  σ δ)  α  a) known
  c₂ : ∀(p : ₂ℕ  U Δ)( : p  Probe Δ)(t : ₂ℕ  ₂ℕ)(tC : t  C) 
        (q : (α : ₂ℕ)  (p α))  q  Q p   (q  t)  Q (p  t) (s⑵ Δ p  t tC)
  c₂ p  t tC q qQ = goal
   where
    known : q  t  DProbe A (σ  p  t) (s⑵ Γ (σ  p) ( p ) t tC)
    known = t⑵ A (σ  p) ( p ) t tC q qQ
    goal : q  t  DProbe A (σ  p  t) ( (p  t) (s⑵ Δ p  t tC))
    goal = t⑷ A (σ  p  t) (q  t) known
  c₃ : ∀(ρ :   ₂ℕ  U Δ)( : ∀(i : )  ρ i  Probe Δ) 
        (ζ : (i : )  (α : ₂ℕ)  (ρ i α))  (∀(i : )  ζ i  Q (ρ i) ( i)) 
        (  ζ)  Q ( ρ) (s⑶ Δ ρ )
  c₃ ρ  ζ  = goal
   where
    σρ :   ₂ℕ  U Γ
    σρ i α = σ(ρ i α)
    fσρ : ∀(i : )  σρ i  Probe Γ
    fσρ i =  (ρ i) ( i)
    known :  (U A) ζ  DProbe A ( σρ) (s⑶ Γ σρ fσρ)
    known = t⑶ A σρ fσρ ζ 
    goal :  (U A) ζ  DProbe A ( σρ) ( ( ρ) (s⑶ Δ ρ ))
    goal = t⑷ A ( σρ) ( (U A) ζ) known
  c₄ : ∀(p : ₂ℕ  U Δ){ pΔ' : p  Probe Δ}(q : (α : ₂ℕ)  (p α)) 
        q  Q 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) [ (σ , ) ]ᵐ = ( , cuσ)
 where
   : (δ : U Δ)  U A (σ δ)
   δ = u(σ δ)
  cuσ : ∀(p : ₂ℕ  U Δ) ( : p  Probe Δ)  (  p)  DProbe A (σ  p) ( p )
  cuσ p  = cu (σ  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}