Chuangjie Xu 2014

\begin{code}

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

module CwF.Sheaf.TypesAndTerms where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber
open import Preliminaries.Sequence
open import CwF.Sheaf.Preliminaries
open import CwF.Sheaf.Base

\end{code}

Types and terms

\begin{code}

Type : Cxt → Set₁
Type Γ = Σ \(A : U Γ → Set) →
Σ \(_✦_ : {γ : U Γ} → A γ → (t : ℂ) → A(γ •[ Γ ] t)) →
(hset-valued A)
× (∀(γ : U Γ)(a : A γ)
→ a ✦ Ι ≈[ A , cond₁ Γ γ ]≈ a)
× (∀(γ : U Γ)(a : A γ)(t r : ℂ)
→ (a ✦ t) ✦ r ≈[ A , cond₂ Γ γ t r ]≈ a ✦ (t ○ r))
× (∀(n : ℕ)(ρ : ₂Fin n → U Γ)(ξ : (s : ₂Fin n) → A(ρ s))
→ Σ! \(a : A (Amal Γ n ρ)) →
∀ s → (a ✦ (Cons s)) ≈[ A , Amal-spec Γ n ρ s ]≈ (ξ s))

Term : (Γ : Cxt) → Type Γ → Set
Term (Γ , _•_ , _) (A , _✦_ , _) =
Σ \(u : (γ : Γ) → A γ) → ∀(γ : Γ)(t : ℂ) → ((u γ) ✦ t) ≡ u(γ • t)

\end{code}

Substitutions

\begin{code}

tySub : (Γ Δ : Cxt) → Type Γ → Sub Δ Γ → Type Δ
tySub Γ Δ (A , _✦_ , hA , ac₁ , ac₂ , ac₃) (σ , nσ) = (Aσ , _✧_ , hAσ , c₁ , c₂ , c₃)
where
_•_ : U Γ → ℂ → U Γ
_•_ = Act Γ
_◦_ : U Δ → ℂ → U Δ
_◦_ = Act Δ
Aσ : U Δ → Set
Aσ δ = A(σ δ)
_✧_ : {δ : U Δ} → Aσ δ → (t : ℂ) → Aσ(δ ◦ t)
a ✧ t = transport A (nσ _ t) (a ✦ t)
hAσ : hset-valued Aσ
hAσ δ = hA(σ δ)
hΓ : hset (U Γ)
hΓ = pr₁(pr₂(pr₂ Γ))

c₁ : ∀(δ : U Δ)(a : Aσ δ)
→ (a ✧ Ι) ≈[ Aσ , cond₁ Δ δ ]≈ a
c₁ δ a = e₀ · e₁ · e₃ · e₄
where
e₀ : transport Aσ (cond₁ Δ δ) (transport A (nσ δ Ι) (a ✦ Ι))
≡ transport A (ap σ (cond₁ Δ δ)) (transport A (nσ δ Ι) (a ✦ Ι))
e₀ = transport-∘ A σ (cond₁ Δ δ)
e₁ : transport A (ap σ (cond₁ Δ δ)) (transport A (nσ δ Ι) (a ✦ Ι))
≡ transport A ((nσ δ Ι) · (ap σ (cond₁ Δ δ))) (a ✦ Ι)
e₁ = transport-· A (nσ δ Ι) (ap σ (cond₁ Δ δ))
e₂ : ((nσ δ Ι) · (ap σ (cond₁ Δ δ))) ≡ (cond₁ Γ (σ δ))
e₂ = hΓ ((nσ δ Ι) · (ap σ (cond₁ Δ δ))) (cond₁ Γ (σ δ))
e₃ : transport A ((nσ δ Ι) · (ap σ (cond₁ Δ δ))) (a ✦ Ι)
≡ transport A (cond₁ Γ (σ δ)) (a ✦ Ι)
e₃ = ap (λ x → transport A x (a ✦ Ι)) e₂
e₄ : transport A (cond₁ Γ (σ δ)) (a ✦ Ι) ≡ a
e₄ = ac₁ (σ δ) a

c₂ : ∀(δ : U Δ)(a : Aσ δ)(t r : ℂ)
→ ((a ✧ t) ✧ r) ≈[ Aσ , cond₂ Δ δ t r ]≈ (a ✧ (t ○ r))
c₂ δ a t r = e₀ · e₁ · e₂ · e₃ · e₄ · e₅ · e₆
where
p₀ : ((δ ◦ t) ◦ r) ≡ (δ ◦ (t ○ r))
p₀ = cond₂ Δ δ t r
p₁ : σ((δ ◦ t) ◦ r) ≡ σ(δ ◦ (t ○ r))
p₁ = ap σ p₀
p₂ : (σ (δ ◦ t) • r) ≡ σ((δ ◦ t) ◦ r)
p₂ = nσ (δ ◦ t) r
p₃ : ((σ δ • t) • r) ≡ (σ(δ ◦ t) • r)
p₃ = ap (λ x → x • r) (nσ δ t)
e₀ : transport Aσ p₀ ((a ✧ t) ✧ r) ≡ transport A p₁ ((a ✧ t) ✧ r)
e₀ = transport-∘ A σ p₀
e₁ : transport A p₁ ((a ✧ t) ✧ r)
≡ transport A (p₂ · p₁) ((a ✧ t) ✦ r)
e₁ = transport-· A p₂ p₁
d₀ : ((transport A (nσ δ t) (a ✦ t)) ✦ r)
≡ transport A p₃ ((a ✦ t) ✦ r)
d₀ = transport-ap A (nσ δ t) (λ x → x ✦ r)
e₂ : transport A (p₂ · p₁) ((a ✧ t) ✦ r)
≡ transport A (p₂ · p₁) (transport A p₃ ((a ✦ t) ✦ r))
e₂ = ap (transport A (p₂ · p₁)) d₀
e₃ : transport A (p₂ · p₁) (transport A p₃ ((a ✦ t) ✦ r))
≡ transport A (p₃ · p₂ · p₁) ((a ✦ t) ✦ r)
e₃ = transport-· A p₃ (p₂ · p₁)
p₄ : ((σ δ • t) • r) ≡ (σ δ • (t ○ r))
p₄ = cond₂ Γ (σ δ) t r
p₅ : ((σ δ) • (t ○ r)) ≡ σ(δ ◦ (t ○ r))
p₅ = nσ δ (t ○ r)
d₁ : p₃ · p₂ · p₁ ≡ p₄ · p₅
d₁ = hΓ (p₃ · p₂ · p₁) (p₄ · p₅)
e₄ : transport A (p₃ · p₂ · p₁) ((a ✦ t) ✦ r)
≡ transport A (p₄ · p₅) ((a ✦ t) ✦ r)
e₄ = ap (λ x → transport A x ((a ✦ t) ✦ r)) d₁
e₅ : transport A (p₄ · p₅) ((a ✦ t) ✦ r)
≡ transport A p₅ (transport A p₄ ((a ✦ t) ✦ r))
e₅ = (transport-· A p₄ p₅)⁻¹
d₂ : transport A p₄ ((a ✦ t) ✦ r) ≡ (a ✦ (t ○ r))
d₂ = ac₂ (σ δ) a t r
e₆ : transport A p₅ (transport A p₄ ((a ✦ t) ✦ r))
≡ transport A p₅ (a ✦ (t ○ r))
e₆ = ap (transport A p₅) d₂

c₃ : ∀(n : ℕ)(ρ : ₂Fin n → U Δ)(ξ : (s : ₂Fin n) → Aσ(ρ s))
→ Σ! \(a : Aσ (Amal Δ n ρ)) →
∀ s → (a ✧ (Cons s)) ≈[ Aσ , Amal-spec Δ n ρ s ]≈ (ξ s)
c₃ n ρ ξ = a , spec , uniq
where
σρ : ₂Fin n → U Γ
σρ s = σ(ρ s)
γ : U Γ
γ = Amal Γ n σρ
a₀ : A γ
a₀ = pr₁(ac₃ n σρ ξ)
δ : U Δ
δ = Amal Δ n ρ
claim₀ : ∀(s : ₂Fin n) → ((σ δ) • (Cons s)) ≡ σ(ρ s)
claim₀ s = e₀ · e₁
where
e₀ : ((σ δ) • (Cons s)) ≡ σ(δ ◦ (Cons s))
e₀ = nσ δ (Cons s)
e₁ : σ(δ ◦ (Cons s)) ≡ σ(ρ s)
e₁ = ap σ (Amal-spec Δ n ρ s)
claim₁ : γ ≡ σ δ
claim₁ = Amal-uniq Γ n σρ (σ δ) claim₀
a : Aσ δ
a = transport A claim₁ a₀
spec : ∀ s → (a ✧ (Cons s)) ≈[ Aσ , Amal-spec Δ n ρ s ]≈ (ξ s)
spec s = goal
where
known : transport A (Amal-spec Γ n σρ s) (a₀ ✦ (Cons s)) ≡ ξ s
known = pr₁(pr₂(ac₃ n σρ ξ)) s
subgoal : transport Aσ (Amal-spec Δ n ρ s) (transport A (nσ δ (Cons s)) (a ✦ (Cons s)))
≡ transport A (Amal-spec Γ n σρ s) (a₀ ✦ (Cons s))
subgoal = e₀ · e₁ · e₃ · e₄ · e₆
where
p : (δ ◦ Cons s) ≡ ρ s
p = Amal-spec Δ n ρ s
q : (σ δ • Cons s) ≡ σ(δ ◦ Cons s)
q = nσ δ (Cons s)
r : (γ • Cons s) ≡ (σ δ • Cons s)
r = ap (λ x → x • Cons s) claim₁
e₀ : transport Aσ p (transport A q (a ✦ Cons s))
≡ transport A (ap σ p) (transport A q (a ✦ Cons s))
e₀ = transport-∘ A σ p
e₁ : transport A (ap σ p) (transport A q (a ✦ Cons s))
≡ transport A (q · (ap σ p)) (a ✦ Cons s)
e₁ = transport-· A q (ap σ p)
e₂ : (a ✦ Cons s) ≡ transport A r (a₀ ✦ Cons s)
e₂ = transport-ap A claim₁ (λ x → x ✦ Cons s)
e₃ : transport A (q · (ap σ p)) (a ✦ Cons s)
≡ transport A (q · (ap σ p)) (transport A r (a₀ ✦ Cons s))
e₃ = ap (transport A (q · (ap σ p))) e₂
e₄ : transport A (q · (ap σ p)) (transport A r (a₀ ✦ Cons s))
≡ transport A (r · q · (ap σ p)) (a₀ ✦ Cons s)
e₄ = transport-· A r (q · (ap σ p))
e₅ : (r · q · (ap σ p)) ≡ Amal-spec Γ n σρ s
e₅ = hΓ (r · q · (ap σ p)) (Amal-spec Γ n σρ s)
e₆ : transport A (r · q · (ap σ p)) (a₀ ✦ Cons s)
≡ transport A (Amal-spec Γ n σρ s) (a₀ ✦ Cons s)
e₆ = ap (λ x → transport A x (a₀ ✦ Cons s)) e₅
goal : transport Aσ (Amal-spec Δ n ρ s) (transport A (nσ δ (Cons s)) (a ✦ (Cons s)))
≡ ξ s
goal = subgoal · known
uniq : ∀ a' → (∀ s → (a' ✧ (Cons s)) ≈[ Aσ , Amal-spec Δ n ρ s ]≈ ξ s) → a ≡ a'
uniq a' spec' = e₀ · e₁
where
known : ∀ a'' → (∀ s → (a'' ✦ (Cons s)) ≈[ A , Amal-spec Γ n σρ s ]≈ ξ s) → a₀ ≡ a''
known = pr₂(pr₂(ac₃ n σρ ξ))
a'' : A γ
a'' = transport A (claim₁ ⁻¹) a'
spec'' : ∀ s → (a'' ✦ (Cons s)) ≈[ A , Amal-spec Γ n σρ s ]≈ ξ s
spec'' s = subgoal · sclaim₀
where
sclaim₀ : transport Aσ (Amal-spec Δ n ρ s) (transport A (nσ δ (Cons s)) (a' ✦ Cons s))
≡ ξ s
sclaim₀ = spec' s
subgoal : transport A (Amal-spec Γ n σρ s) ((transport A (claim₁ ⁻¹) a') ✦ Cons s)
≡ transport Aσ (Amal-spec Δ n ρ s) (transport A (nσ δ (Cons s)) (a' ✦ Cons s))
subgoal = e₁ · e₂ · e₄ · d₁ ⁻¹ · d₀ ⁻¹
where
p : (γ • Cons s) ≡ σ(ρ s)
p = Amal-spec Γ n σρ s
q : (σ δ • Cons s) ≡ (γ • Cons s)
q = ap (λ x → x • Cons s) (claim₁ ⁻¹)
p' : (δ ◦ Cons s) ≡ ρ s
p' = Amal-spec Δ n ρ s
r : (σ δ • Cons s) ≡ σ(δ ◦ Cons s)
r = nσ δ (Cons s)
e₀ : ((transport A (claim₁ ⁻¹) a') ✦ Cons s) ≡ transport A q (a' ✦ Cons s)
e₀ = transport-ap A (claim₁ ⁻¹) (λ x → x ✦ Cons s)
e₁ : transport A p ((transport A (claim₁ ⁻¹) a') ✦ Cons s)
≡ transport A p (transport A q (a' ✦ Cons s))
e₁ = ap (transport A p) e₀
e₂ : transport A p (transport A q (a' ✦ Cons s))
≡ transport A (q · p) (a' ✦ Cons s)
e₂ = transport-· A q p
d₀ : transport Aσ p' (transport A r (a' ✦ Cons s))
≡ transport A (ap σ p') (transport A r (a' ✦ Cons s))
d₀ = transport-∘ A σ p'
d₁ : transport A (ap σ p') (transport A r (a' ✦ Cons s))
≡ transport A (r · (ap σ p')) (a' ✦ Cons s)
d₁ = transport-· A r (ap σ p')
e₃ : (q · p) ≡ (r · (ap σ p'))
e₃ = hΓ (q · p) (r · (ap σ p'))
e₄ : transport A (q · p) (a' ✦ Cons s)
≡ transport A (r · (ap σ p')) (a' ✦ Cons s)
e₄ = ap (λ x → transport A x (a' ✦ Cons s)) e₃
subgoal : a₀ ≡ a''
subgoal = known a'' spec''
e₀ : a ≡ transport A claim₁ a''
e₀ = ap (λ x → transport A claim₁ x) subgoal
e₁ : transport A claim₁ a'' ≡ a'
e₁ = transport-p⁻¹·p A claim₁ a'

tmSub : (Γ Δ : Cxt) → (A : Type Γ)
→ Term Γ A → (σ : Sub Δ Γ) → Term Δ (tySub Γ Δ A σ)
tmSub (Γ , _•_ , _) (Δ , _◦_ , _) (A , _✦_ , _) (u , nu) (σ , nσ) = (uσ , nuσ)
where
uσ : (δ : Δ) → A(σ δ)
uσ δ = u(σ δ)
nuσ : ∀(δ : Δ)(t : ℂ) → transport A (nσ δ t) ((uσ δ) ✦ t) ≡ (uσ (δ ◦ t))
nuσ δ t = goal
where
claim₀ : ((uσ δ) ✦ t) ≡ u((σ δ) • t)
claim₀ = nu (σ δ) t
claim₁ : ((σ δ) • t) ≡ σ(δ ◦ t)
claim₁ = nσ δ t
claim₂ : transport A (nσ δ t) (u((σ δ) • t)) ≡ uσ (δ ◦ t)
claim₂ = apd u claim₁
goal : transport A (nσ δ t) ((uσ δ) ✦ t) ≡ (uσ (δ ◦ t))
goal = transport (λ r → transport A (nσ δ t) r ≡ uσ (δ ◦ t)) (claim₀ ⁻¹) claim₂

\end{code}

Equations

\begin{code}

-- A[1] = A
Eq₄ : (Γ : Cxt) (A : Type Γ)
→ ∀(γ : U Γ) → U (tySub Γ Γ A (I Γ)) γ ≡ U A γ
Eq₄ Γ A γ = refl

-- A[σ][τ] = A[σ ∘ τ]
Eq₅ : (Γ Δ Θ : Cxt) (A : Type Γ) (σ : Sub Δ Γ) (τ : Sub Θ Δ)
→ ∀(θ : U Θ) →   U (tySub Δ Θ (tySub Γ Δ A σ) τ) θ
≡ U (tySub Γ Θ A (⟪ Γ , Δ , Θ ⟫ σ ◎ τ)) θ
Eq₅ Γ Δ Θ A σ τ θ = refl

-- u[1] = u
Eq₆ : (Γ : Cxt) (A : Type Γ) (u : Term Γ A)
→ ∀(γ : U Γ) → pr₁ (tmSub Γ Γ A u (I Γ)) γ ≡ pr₁ u γ
Eq₆ Γ A u γ = refl

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

\end{code}