Practical Foundations of Mathematics

Paul Taylor

8.5  Exercises VIII

  1. Show that, when src and tgt are omitted, the theory of categories in Example 8.1.12 is stratified (Definition  8.1.11). Extend this theory to categories with products, coproducts and exponentials by transcribing the universal properties.

  2. Describe the stratified algebraic theory of 2-categories.

  3. Why, with only O and H as types, is the theory of categories with pullbacks not a generalised algebraic theory as defined in Section 8.1? Describe such a theory using an additional type of commutative squares or triangles. This is not a stratified theory - do you think that any theory of pullbacks could be?

  4. Formulate the notions of plain, distributive, positive, division and power allegory in [FS90] as stratified algebraic theories. Why is the theory of tabular allegories not stratified?

  5. Formulate the generalised algebraic theory of generalised algebraic theories ( cf Remark 8.4.1). Extend this to the theory of a theory together with a model.

  6. Show that coercion (mentioned in Definition  8.2.3), weakening ( 8.2.5) and cut (8.2.6) are derived rules of the calculus of Section 8.1, in the external sense that if there is a valid deduction of the premise then there is also one of the conclusion. Explain what one must check in order to show that extensions of the calculus retain these properties, and verify them for the sum and product rules.

  7. Deduce the starred laws in Remark  8.2.7 from their unstarred forms using Lemma  8.2.15. [Hint: writing h:X® D for the unstarred commutative square, and f,g:[X,h *Y]\rightrightarrows [D,Y] for the two sides of the starred one, show that f = \idh*Y;\hY = g .]

  8. Let e = [x: = a] and m = [^(y)] where G\vdash a:X and D\vdash y:Y. Show that the diagonal fill-in for the orthogonality property (Definition  5.7.1) exists. [Hint: use Lemmas 5.7.10 and 8.2.10. ] omitted diagram environment Show that if e^[^(y)], ie the fill-in is unique, for all displays [^(y)] then e is an isomorphism, ie X º \terminalobjG . [Hint: let [^(y)]:[G ,x:X,y:X]® [G,x:X], f = [x: = a,y: = a] and g = id and show that both [y: = x] and [y: = a] are fill-ins.]

  9. Show that every map f:[G;F]® [G, D] such that f;[^(D)] = [^(F)] ( ie the triangle in Definition 8.2.9 commutes in the whole category) can be expressed as a composite of displays and cuts which each leave G untouched.

  10. Show that (D,J)® ([x:X,D], J) defines a functor [^(x)]!:Cn×L¯ [G,x:X]® Cn×L¯ G with [^(x)]!\dashv [^(x)]*.

  11. Show that pullback along any map u:G® D extends to a functor u*:C¯ D ® C¯ G.

  12. Prove the normal form theorem for (semantic) relative slice categories (Proposition 8.3.11).

  13. Let D Ì C be a class of display maps. Let \typeX(-):Á® D be a diagram where Á is a finite oriented graph which, qua unoriented graph, is simply connected. Show that this diagram has a limit in C and that the limiting cone consists of D-maps. Assuming that D is a subcategory closed under cofiltered limits, extend the result to arbitrary simply connected diagrams.

  14. Draw the diagram which introduces the variable qua term of an arbitrary instance of a type.

  15. Explain how the definition of a generalised algebraic theory reduces to Definition 4.6.2ff in simple type theory. Similarly compare the notions of interpretation and homomorphism, reconciling the presentation of laws as commutative polygons and as pullbacks. How does the canonical language reduce to Section 7.6 in simple type theory?

  16. Show that, once the interpretation of the display map [^(x)] is fixed, changing those of the auxiliary objects by isomorphisms does not affect the interpretation of a.