Chuangjie Xu 2014

\begin{code}

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

module CwF.Sheaf.ContextComprehension where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import CwF.Sheaf.Preliminaries
open import CwF.Sheaf.Base
open import CwF.Sheaf.TypesAndTerms

\end{code}

Context comprehension

\begin{code}

infixl  _₊_

_₊_ : (Γ : Cxt) → Type Γ → Cxt
(Γ , _•_ , hΓ , gc₀ , gc₁ , gc₂) ₊ (A , _✦_ , hA , ac₀ , ac₁ , ac₂) = 
  (ΣΓA , _◦_ , hΣΓA , c₀ , c₁ , c₂)
 where
  ΣΓA : Set
  ΣΓA = Σ \(γ : Γ) → A γ
  _◦_ : ΣΓA → ℂ → ΣΓA
  (γ , a) ◦ t = (γ • t , a ✦ t )
  hΣΓA : hset ΣΓA
  hΣΓA = Σ-hset hΓ hA
  c₀ : ∀(w : ΣΓA) → (w ◦ Ι) ≡ w
  c₀ (γ , a) = pair⁼ (gc₀ γ) (ac₀ γ a)
  c₁ : ∀(w : ΣΓA)(t r : ℂ) → ((w ◦ t) ◦ r) ≡ (w ◦ t ○ r)
  c₁ (γ , a) t r = pair⁼ (gc₁ γ t r) (ac₁ γ a t r)
  c₂ : ∀(n : ℕ)(ρ : ₂Fin n → ΣΓA) → Σ! \(w : ΣΓA) → ∀ s → (w ◦ Cons s) ≡ ρ s
  c₂ n ρ = (γ , a) , spec , uniq
   where
    γ : Γ
    γ = pr₁(gc₂ n (pr₁ ∘ ρ))
    a : A γ
    a = pr₁(ac₂ n (pr₁ ∘ ρ) (pr₂ ∘ ρ))
    spec : ∀ s → (γ • (Cons s) , a ✦ (Cons s)) ≡ ρ s
    spec s = pair⁼ (pr₁(pr₂(gc₂ n (pr₁ ∘ ρ))) s) (pr₁(pr₂(ac₂ n (pr₁ ∘ ρ) (pr₂ ∘ ρ))) s)
    uniq : ∀(w' : ΣΓA) → (∀ s → (w' ◦ Cons s) ≡ ρ s) → (γ , a) ≡ w'
    uniq (γ' , a') spec' = pair⁼ eγ ea
     where
      spec-γ' : ∀ s → (γ' • Cons s) ≡ pr₁(ρ s)
      spec-γ' s = pr₁⁼ (spec' s)
      eγ : γ ≡ γ'
      eγ = pr₂(pr₂(gc₂ n (pr₁ ∘ ρ))) γ' spec-γ'
      spec-γ : ∀ s → (γ • Cons s) ≡ pr₁(ρ s)
      spec-γ = pr₁(pr₂(gc₂ n (pr₁ ∘ ρ)))
      claim₀ : ∀ s → transport A (spec-γ' s) (a' ✦ Cons s) ≡ pr₂(ρ s)
      claim₀ s = pr₂⁼ (spec' s)
      a'' : A γ
      a'' = transport A (eγ ⁻¹) a'
      claim₁ : ∀ s → transport A (spec-γ s) ((transport A (eγ ⁻¹) a') ✦ Cons s) ≡ pr₂(ρ s)
      claim₁ s = e₁ · e₂ · e₄ · claim₀ s
       where
        p : (γ' • Cons s) ≡ (γ • Cons s)
        p = ap (λ x → x • Cons s) (eγ ⁻¹)
        e₀ : (transport A (eγ ⁻¹) a' ✦ Cons s) ≡ transport A p (a' ✦ Cons s)
        e₀ = transport-ap A (eγ ⁻¹) (λ x → x ✦ Cons s)
        e₁ : transport A (spec-γ s) (transport A (eγ ⁻¹) a' ✦ Cons s)
           ≡ transport A (spec-γ s) (transport A p (a' ✦ Cons s))
        e₁ = ap (transport A (spec-γ s)) e₀
        e₂ : transport A (spec-γ s) (transport A p (a' ✦ Cons s))
           ≡ transport A (p · (spec-γ s)) (a' ✦ Cons s)
        e₂ = transport-· A p (spec-γ s)
        e₃ : (p · (spec-γ s)) ≡ (spec-γ' s)
        e₃ = hΓ (p · (spec-γ s)) (spec-γ' s)
        e₄ : transport A (p · (spec-γ s)) (a' ✦ Cons s)
           ≡ transport A (spec-γ' s) (a' ✦ Cons s)
        e₄ = ap (λ x → transport A x (a' ✦ Cons s)) e₃
      claim₂ : a ≡ a''
      claim₂ = pr₂(pr₂(ac₂ n (pr₁ ∘ ρ) (pr₂ ∘ ρ))) a'' claim₁
      claim₃ : transport A eγ a ≡ transport A eγ a''
      claim₃ = ap (transport A eγ) claim₂
      claim₄ : transport A eγ a'' ≡ a'
      claim₄ = transport-p⁻¹·p A eγ a'
      ea : a ≈[ A , eγ ]≈ a'
      ea = claim₃ · claim₄


[_₊_]ⓟ : (Γ : Cxt) → (A : Type Γ) → Sub (Γ ₊ A) Γ
[ Γ ₊ A ]ⓟ = pr₁ , (λ w t → refl)

[_₊_]ⓠ : (Γ : Cxt) → (A : Type Γ) → Term (Γ ₊ A) (tySub Γ (Γ ₊ A) A [ Γ ₊ A ]ⓟ)
[ Γ ₊ A ]ⓠ = pr₂ , (λ w t → refl)

[_,_,_]⟨_,_⟩ : (Γ Δ : Cxt) (A : Type Γ)
             → (σ : Sub Δ Γ) → Term Δ (tySub Γ Δ A σ) → Sub Δ (Γ ₊ A)
[ Γ , Δ , A ]⟨ (σ , nσ) , (u , nu) ⟩ = τ , nτ
 where
  _◦_ = pr₁(pr₂ Δ)
  _●_ = pr₁(pr₂ (Γ ₊ A))
  τ : U Δ → U(Γ ₊ A)
  τ δ = (σ δ , u δ)
  nτ : ∀(δ : U Δ) (t : ℂ) → ((τ δ) ● t) ≡ τ(δ ◦ t)
  nτ δ t = pair⁼ (nσ δ t) (nu δ t)

\end{code}

Substitution by terms

\begin{code}

tySubᵐ : (Γ : Cxt) (A : Type Γ)
       → (B : Type (Γ ₊ A)) → Term Γ A → Type Γ
tySubᵐ Γ A B u = tySub (Γ ₊ A) Γ B [ Γ , Γ , A ]⟨ I Γ , u ⟩


tmSubᵐ : (Γ : Cxt) (A : Type Γ) (B : Type (Γ ₊ A))
       → Term (Γ ₊ A) B → (u : Term Γ A) → Term Γ (tySubᵐ Γ A B u)
tmSubᵐ Γ A B v u = tmSub (Γ ₊ A) Γ B v [ Γ , Γ , A ]⟨ I Γ , u ⟩

\end{code}

Equations

\begin{code}

-- p ∘ (σ , u) = σ
Eq₈ : (Γ Δ : Cxt) (A : Type Γ) (σ : Sub Δ Γ) (u : Term Δ (tySub Γ Δ A σ))
    → ∀(δ : U Δ) →   pr₁ (⟪ Γ , Γ ₊ A , Δ ⟫ ([ Γ ₊ A ]ⓟ) ◎ ([ Γ , Δ , A ]⟨ σ , u ⟩)) δ
                   ≡ pr₁ σ δ
Eq₈ Γ Δ A σ u δ = refl

-- q[(σ , u)] = u
Eq₉ : (Γ Δ : Cxt) (A : Type Γ) (σ : Sub Δ Γ) (u : Term Δ (tySub Γ Δ A σ))
    → ∀(δ : U Δ) →   pr₁ (tmSub (Γ ₊ A) Δ (tySub Γ (Γ ₊ A) A [ Γ ₊ A ]ⓟ)
                                ([ Γ ₊ A ]ⓠ) ([ Γ , Δ , A ]⟨ σ , u ⟩)) δ
                   ≡ pr₁ u δ
Eq₉ Γ Δ A σ u δ = refl

-- (p,q) = 1
Eq₁₀ : (Γ : Cxt) (A : Type Γ)
     → ∀(w : U(Γ ₊ A))
     → pr₁ ([ Γ , Γ ₊ A , A ]⟨ [ Γ ₊ A ]ⓟ , [ Γ ₊ A ]ⓠ ⟩) w ≡ w
Eq₁₀ Γ A w = refl

\end{code}

To formulate (σ , u) ∘ τ = (σ ∘ τ , u[τ]), we need the following transport map,
because u[τ] has type A[σ][τ] instead of A[σ∘τ], and A[σ][τ] = A[σ∘τ] holds up
to pointwise equality only.

\begin{code}

T₁₁ : (Γ Δ Θ : Cxt) (A : Type Γ) (σ : Sub Δ Γ) →
      (u : Term Δ (tySub Γ Δ A σ)) (τ : Sub Θ Δ)
    → Term Θ (tySub Δ Θ (tySub Γ Δ A σ) τ) → Term Θ (tySub Γ Θ A (⟪ Γ , Δ , Θ ⟫ σ ◎ τ))
T₁₁ Γ Δ Θ A σ u τ (ν , nν) = ν , nν'
 where
  _•_ = pr₁(pr₂ Θ)
  _✦_ = pr₁(pr₂ A)
  nσ = pr₂ σ
  nτ = pr₂ τ
  nστ = pr₂(⟪ Γ , Δ , Θ ⟫ σ ◎ τ)
  Aσ : U Δ → Set
  Aσ δ = U A (pr₁ σ δ)
  nν' : ∀(θ : U Θ)(t : ℂ) → transport (U A) (nστ θ t) (ν θ ✦ t) ≡ ν(θ • t)
  nν' θ t = (e₀ ⁻¹ · e₁ · e₂ · e₄)⁻¹
   where
    e₀ : transport Aσ (nτ θ t) (transport (U A) (nσ (pr₁ τ θ) t) (ν θ ✦ t)) ≡ ν(θ • t)
    e₀ = nν θ t
    e₁ : transport Aσ (nτ θ t) (transport (U A) (nσ (pr₁ τ θ) t) (ν θ ✦ t))
       ≡ transport (U A) (ap (pr₁ σ) (nτ θ t)) (transport (U A) (nσ (pr₁ τ θ) t) (ν θ ✦ t))
    e₁ = transport-∘ (U A) (pr₁ σ) (nτ θ t)
    e₂ : transport (U A) (ap (pr₁ σ) (nτ θ t)) (transport (U A) (nσ (pr₁ τ θ) t) (ν θ ✦ t))
       ≡ transport (U A) ((nσ (pr₁ τ θ) t) · (ap (pr₁ σ) (nτ θ t))) (ν θ ✦ t)
    e₂ = transport-· (U A) (nσ (pr₁ τ θ) t) (ap (pr₁ σ) (nτ θ t))
    e₃ : ((nσ (pr₁ τ θ) t) · (ap (pr₁ σ) (nτ θ t))) ≡ (nστ θ t)
    e₃ = pr₁(pr₂(pr₂ Γ)) ((nσ (pr₁ τ θ) t) · (ap (pr₁ σ) (nτ θ t))) (nστ θ t)
    e₄ : transport (U A) ((nσ (pr₁ τ θ) t) · (ap (pr₁ σ) (nτ θ t))) (ν θ ✦ t)
       ≡ transport (U A) (nστ θ t) (ν θ ✦ t)
    e₄ = ap (λ x → transport (U A) x (ν θ ✦ t)) e₃

-- (σ , u) ∘ τ = (σ ∘ τ , u[τ])
Eq₁₁ : (Γ Δ Θ : Cxt) (A : Type Γ) (σ : Sub Δ Γ) →
       (u : Term Δ (tySub Γ Δ A σ)) (τ : Sub Θ Δ)
     → ∀(θ : U Θ) →   pr₁ (⟪ Γ ₊ A , Δ , Θ ⟫ ([ Γ , Δ , A ]⟨ σ , u ⟩) ◎ τ) θ
                    ≡ pr₁ ([ Γ , Θ , A ]⟨ (⟪ Γ , Δ , Θ ⟫ σ ◎ τ ) ,
                                          T₁₁ Γ Δ Θ A σ u τ (tmSub Δ Θ (tySub Γ Δ A σ) u τ) ⟩) θ
                                         -----
Eq₁₁ Γ Δ Θ A σ u τ θ = refl

\end{code}