This files proves that presheaves on a category C (contravariant functors into HSET) forms a type category (PreShv_TypeCat). As the collection of types in context Γ don't form an hset it is not possible to instantiate the CwF structure, however all of the other axioms of a CwF have been formalized. Contexts, written Γ ⊢, are modelled as presheaves and substitutions are modelled by natural transformations σ : Δ → Γ. So the identity substitution is given by the identity natural transformation 1 : Γ → Γ and composition of substitutions are given by composition of natural transformations σ · δ (note that the order is diagrammatic). So we automatically get the equations:

      1 · σ = σ · 1 = σ        (σ · δ) · τ = σ · (δ · τ)

Types in context Γ, usually written Γ ⊢ A and written A : Γ ⊢ in the formalization, are defined as presheaves on the category of elements of Γ. So A : Γ ⊢ means A : PreShv (∫ Γ). Terms a of type A in context Γ, usually written Γ ⊢ a : A and written a : Γ ⊢ A in the formalization, are defined as families of sets aρ in Aρ for each set ρ in Γ(I) such that (aρ)f = a(ρf) for f : J → I (see TermIn). This is equivalent to sections s : Γ → Γ.A of the projection map p : Γ.A → Γ (see TermIn_to_TermInSection, TermInSection_to_TermIn). The operations then defined are:

              Γ ⊢ A    σ : Δ → Γ
            ---------------------- ([subst_type])
                   Δ ⊢ Aσ


             Γ ⊢ a : A    σ : Δ → Γ
           -------------------------- ([subst_term)]
                 Δ ⊢ aσ : Aσ


                    Γ ⊢ A
                 ----------- ([ctx_ext])
                   Γ ⋆ A ⊢


                    Γ ⊢ A
               ----------------- ([ctx_proj])
                 p : Γ ⋆ A → Γ


                    Γ ⊢ A
              ------------------ ([ctx_last])
                Γ ⋆ A ⊢ q : Ap


             σ : Δ → Γ   Γ ⊢ A   Δ ⊢ a : Aσ
          ----------------------------------- ([subst_pair])
                (σ,a) : Δ → Γ ⋆ A


                  σ : Δ → Γ    Δ ⊢ A
                ---------------------- ([p_gen])
                  p_gen : Δ ⋆ A → Γ


                  σ : Δ → Γ    Γ ⊢ A
             ----------------------------- ([q_gen])
               Δ ⋆ Aσ ⊢ q_gen : A(p_gen)

These satisfy the following equations:

                       A1 = A            ([subst_type_id])

                    (Aσ)δ = A(σδ)        ([subst_type_comp])

                       a1 = a            ([subst_term_id])

                    (aσ)δ = a(σδ)        ([subst_term_comp])

                δ · (σ,a) = (δ · σ,aδ)   ([subst_pair_subst])

                (σ,a) · p = σ            ([subst_pair_p])

                   q(σ,a) = a            ([subst_pair_q])

                    (p,q) = 1            ([subst_pair_id])

        (p_gen,q_gen) · p = p · σ        ([q_gen_mor_p])

And the last square is a pullback square (isPullback_q_gen_mor). Written by: Anders Mörtberg, 2017

Γ ⊢ A is interpreted as a presheaf of ∫ Γ. In Coq this is written A : Γ ⊢

The substitution functor

WARNING: Only use this for small C

The right adjoint to substitution

Given Γ ⊢ A and a substitution σ : Δ → Γ we get Δ ⊢ Aσ

A1 = A

A(σ1 σ2) = (A σ2) σ1

Direct definition of terms: Γ ⊢ a : A

Context extension: given a context Γ and a type Γ ⊢ A define Γ.A

Context projection

Note that ctx_ext and p defines one part of the equivalence:

     PreShv(∫ Γ) ≃ PreShv(C) / Γ

by: Γ ⊢ A ↦ (Γ ⋆ A,p) Intuition: Γ ⋆ A is over Γ by p The last element of the context, often referred to as q

Given Γ ⊢ a : A and a substitution σ : Δ → Γ we get Δ ⊢ aσ : Aσ

a1 = a

a(σ1 σ2) = (a σ2)σ1

Pairing of substitutions

a = (1,a)

(σ,a) · p = σ

q(σ,a) = a

σ2 · (σ1,a) = (σ2 · σ1,a σ2)

(p,q) = 1

Γ ⊢ a : A can also be interpreted as sections s : Γ --> Γ.A to p

Various results for instantiating TypeCat

Presheaf categories are type categories

Failed attempt to instantiate CwF structure