Fix typos

[inexxt]

Typos:

• [x] 324: "explicitly"
• [x] 389: \pi_1 should be a function to A, not U
• [x] 401: transport-equiv(P) x y is an equivalence for all x, y : A
• [x] 448-455: T is an arbitrary type, T : U.
• [x] 500: In the commutativity clause for disjoint union one of the Ys should be an X
• [x] 763: not an "inclusion"
• [x] 806: rename "k" to "i"
• [x] 872: A parenthesis around the argument of the dependent sum
• [x] 390: U should be A
• [x] 417: Sub-universe
• [x] 485: ones
• [x] 614: notation for group homomorphism
• [x] 821: double "the"
• [x] 843: respect
• [x] 1068: consists of
• [x] 1073: computes to the following
• [x] 1122: It could
• [x] 1124: difficult to formalize
• [x] 1131: comma before "see"
• [x] 1147: results suggest
• [x] 356: Pi-types