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}