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

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