## § 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:
`Γ <--Γ-- (Γ;Δ)---Δ--> Δ`

.