§ Simple Type Theory via Fibrations
- Objects are contexts, so sequence of
- 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, ...,
- 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
- 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
M2:s2, so they have the correct types to be substituted for
x2. Thus, in context
N1[x1 := M1, x2 := M2]has the same type it used to have
- 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
- Do the same for
- 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
- The categorical product of contexts is given by sequencing (see that this needs exchange), and the projections are the "obvious" rules:
Γ <--Γ-- (Γ;Δ)---Δ--> Δ.