§ Simple Type Theory via Fibrations

• Objects are contexts, so sequence of (term:type)
• Morphisms between contents Γ = (v1:s1, v2:s2) and Δ = (w1:t1, w2:t2)are terms M1, M2 such that we have Γ |- M1 : t1 and Γ |- M2 : t2.
• More cleaned up, for a context Γ, and a context Δ with sequence of types (_:t1, _:t2, ..., _:tn), a morphism is a sequence of terms Γ|- M1: t1, Γ|- M2:t2, ..., Γ|-Mn:tn.
• For concreteness, let us suppose Δ = (w1:t1, w2: t2)
• The identity morphism is Δ -(d1, d2)-> Δ, since we have d1 := w1:t1, w2:t2|-w1:t1 and d2 := w1:t1, w2:t2|-w2:t2. Thus, starting from Δ on the context, we can derive terms of types t1, t2, which are given by the derivations d1, d2.
• Let us meditate on composition Γ -(d1, d2)-> Δ -(d1', d2')-> Θ. First off, let us write this more explicitly as:

Γ

(d1 := Γ|-M1:s1, d2 := Γ|-M2:s2)

Δ := (x1:s1, x2:s2)


(d'1 := Δ|-N1:t1, d2 := Δ|-N2:t2)

Θ := (_:t1, _:t2)

• See that have (x1:s1, x2:s2)|- N1 : t1
• If we substitute N1[x1 := M1, x2 := M2], then under context Γ, we know that M1:s1, and M2:s2, so they have the correct types to be substituted for x1 and x2. Thus, in context Γ, N1[x1 := M1, x2 := M2]has the same type it used to have (t1).
• Thus we have that Γ |- N1[x1 := M1, x2 := M2] : t1.
• This gives us the composite of the section of the morhphisms, by telling us how to compose d'1 with d1.
• Do the same for d2.
• What the hell is going on anyway?
• Given any well typed term in a context, Γ|-M:t, we can think of this as a morphism Γ --M--> (Δ:=M:t).
• This relative point of view (ala grothendieck) lets us extend to larger contexts.
• The empty context is the terminal object, since there is precisely one morphism, consisting of the empty sequence (). Can be written as Γ-()-> 0.
• The categorical product of contexts is given by sequencing (see that this needs exchange), and the projections are the "obvious" rules: Γ <--Γ-- (Γ;Δ)---Δ--> Δ.