Practical Foundations of Mathematics

Paul Taylor

9.7  Exercises IX

1. Investigate the naturality of $x\dashv [^(x)]^* \dashv "x as in Section 7.2.

2. Definition 9.2.1 associates a divided context to any jumbled one. Construct the isomorphism between them.

3. In the first part of Lemma 9.2.2, show that this is the initial solution to forming a pullback square with the given top and right sides.

4. Show that any fibration P:C® S preserves pullbacks. Give a semilattice example in which it does not preserve T, but show that if there is a functor T with P·T = \id _S then P does preserve all finite limits. Conversely, show that if C and S have and P:C® S preserves pullbacks, and P\dashv T with P·T = \id_S, then P is a fibration.

5. Show that the pseudo-vertical and prone maps for any fibration P:C® S form a factorisation system ( Definition 5.7.2) in C. [Hint: the prone part of a C-morphism f is the lifting of Pf ; use the universal property again to show that the fill-in property holds.] Also show that every square consisting of parallel vertical and prone maps is a pullback. We call this situation a cartesian factorisation system.

6. Show that every fibration in which the base category and fibres have all finite limits arises uniquely from a conservative extension of Horn (or essentially algebraic) theories: the two classes of displays consist of the prone and vertical maps respectively.

7. Show that p₀:S¯ U® S in Proposition 7.7.1 is a fibration, but is not comprehensive or an op-fibration. What is the corresponding conservative extension of theories?

8. In any fibration P:C® S, show how to find limits in C, given limits in S and the fibres. Show that pts:Sp® Set and ob:Cat® Set are bifibrations (Definition 9.2.6(e)), and use this to describe limits and colimits in Sp and Cat, cf Section 7.4.

9. Let E^M be a factorisation system in a category C. Verify that the supine, vertical and prone morphisms for the codomain fibration tgt = p₁: M¯ C® C are as shown below, and that if E^M is stable then so is the supine-vertical factorisation. omitted diagram environment Conversely, suppose that M Ì C is such that the class M¢ of squares like those in the middle, but with isomorphisms at the bottom, is part of a (stable) factorisation system; show that M is too.

10. Prove Proposition 9.2.9 in detail for Horn theories. Let S = È^­ \typeR_i in the base category (algebraic lattice) Mod(L_type ). Prove the limit-colimit coincidence, that the projections Mod(S)® Mod(\typeR_i) form a limiting cone, and the embeddings a colimiting cocone in the category of algebraic lattices and Scott-continuous functions. Show that every fibration of algebraic lattices with these properties arises from a conservative extension of Horn theories.

11. Formulate the divided theory whose type part has one sort and whose propositional part is the theory of groups. Use this and Proposition 9.2.9 to compute limits and colimits in Gp. More generally, describe the theory which divides the laws of an algebraic theory from its sorts and operation- symbols ( cf Remark 7.4.10 and Example  9.2.4(h)), and use it to compute free algebras.

12. Formulate the sense in which the total category C of a fibration P:C® S is the lax colimit of the corresponding indexed category, considered as a diagram of shape S in the 2-category ^C/_at.

13. Use the Grothendieck construction for a diagram Á ® Set to compute its (strict) colimit. [Hint: consider the connected components of the total category.]

14. (For group theorists.) Use the fact that fibrations of groups are surjective homomorphisms and that this class is closed under pullbacks to prove the Jordan-Hölder theorem.

15. Repeat Exercise 4.41, that Set^Cop is cartesian closed, using the Grothendieck construction to replace presheaves by discrete fibrations.

16. Let P:C® S be a fibration. Define the morphisms of the category D, whose objects are triples (G,F,u:G® PF), such that p₀:D ® S is a split fibration and F® (PF,F,\id_F ) is a weak equivalence. [Hint: this is not the comma category C¯ P.] Describe the groupoid that arises in this way from Z/(4)\twoheadrightarrow Z/(2).

17. Let P:C® S be any fibration. Suppose that there is a choice of re-indexing functors u^*:P( D)® P(G) for each u:G® D in S. Formulate the coherence conditions which relate id^* to the identity re-indexing functor and (u;| )^* to u^*·|^*. Conversely, given assignments P(G) and u^* satisfying these conditions, adapt the Grothendieck construction (Proposition  9.2.7) to recover the fibration.

18. Investigate the formation and coherence rules for explicit isomorphisms instead of equalities of types in Definition  8.1.7.

19. In terms of bifibrations, show that the Beck-Chevalley condition for a particular pullback in the base category says that the prone and supine liftings going two ways around the square ``join up.''

20. Let C be a category with products and 2 = 1+1 such that the inclusions 1® 2 are carrable. Show that C is extensive (Section  5.5) iff there is a class D of displays with the following type-theoretic property: for any two types Y, N there is a dependent type i:2\vdash X[i] type such that Y º X[1], N º X[0], and Si:2.X[i] is their coproduct. In this case show also that Pi:2.X[i] is their product. ( Cf Exercise 5.35.)

21. Show that ($x:X.^) º ^,

    = 2pt omitted array environment

    and $x:X.$y:Y[x].f[x,y] º $z:(Sx:X.Y[x]).f[p₀(z),p₁(z)].

22. Consider a generalised cut of a substitution u: G® D with the ($^-E)-rule. Show that the substituted form of the rule as we gave it in Definition  9.3.6 is what is needed to commute these sequent rules.

23. What is the type of lz.(let(x,y )bezind)? Considering this type as a proposition, what is its relationship to that of lx, y.d? [Hint: Exercise 1.22.] How is this relationship expressed by the ve operation?

24. Formulate the canonical $-language (Section  7.6) for a stable factorisation system, and use gluing (Section 7.7) to prove conservativity and equivalence.

25. Show that the Beck-Chevalley comparison maps as given in Definition 9.3.6ff for the existential quantifier are mutually inverse.

26. Show that the Beck-Chevalley condition is automatic for dependent sums, ie composition of displays. Using Exercise  7.29, deduce the same condition for locally cartesian closed categories (Proposition  9.4.6).

27. (Jacobs, Moggi and Streicher) Show that if M is closed under composition, ie it admits strong sums over itself, then weak sums over D are sufficient to derive the strong version ( cf Exercise 5.47).

28. Show how to define

    omitted prooftree environment

    [Hint: define \polly₁:$x:X.f® q₁ with the weak sum, then use the strong sum for \polly₂:$x:X.f® \polly₁^*q₂ and again for \polly₃.]

29. Adapt Section 9.3 to sums Sx:X. f in which the result is of a different kind (M) from the body (\nearrow [thick]). [Hint: Theorem  9.3.11 becomes E^M and \nearrow [thick];D Ì E;M stably.]

30. For the continuation rule for the strong sum type, the top right square in Theorem 9.3.11 need not be a pullback. What is the effect of this in terms of the universal property of a factorisation system, and why is this automatic? Formulate the corresponding type-theoretic rule for the strong and weak sums and also discuss it in the idioms of Section 7.2.

31. Let E and M be two classes of maps satisfying the conditions of Theorem 9.3.11. Suppose that either (a) all maps (in particular verdicts) factorise, or (b) all M-maps are mono. Show that E is pullback-stable .

32. Formulate the cut-elimination step which expresses Pb in the sequent calculus. (The right rule is essentially the same as ("Á ), and the left rule was given in Definition  9.4.1.)

33. Show how to extend the universal quantifier to "x. F, where F is a list of propositions dependent on x:X. [Hint: adapt Lemma 9.4.13.]

34. Deduce from Exercise 7.36 that D(-)^X preserves monos, so the class of monos is closed under universal quantification in the sense needed for the remarks following Proposition 9.4.6.

35. Show that the free algebra FG on a set G for a finitary free theory is the partial product Px.G of G along the map X® F 1 that is itself defined as the pullback of tgt:( < ) ® N along the interpretation [[-]]:F1® N defined in Exercise 6.3.

36. Formulate the canonical language for partial products and prove conservativity for dependent products as in Sections 7.6 and 7.7.

37. Prove Theorem 9.4.14, that dependent products can be reduced to partial products, type- theoretically.

38. Prove Lemma 9.4.10, that DXF^X º (DX)xF if DX® D is mono, using type theory.

39. Let F be a propositional context and suppose that the partial products of F along the displays DXy \hookrightarrow DX® D exist. Prove, both type- theoretically and by diagram-chasing, that the partial product along D($x.y)\hookrightarrow D also exists. [Hint: "z:($x.y).F º "x."y :y.F.]

40. Deduce that any local homeomorphism is exponentiable in Sp.

41. Find a Scott-continuous function between dcpos which satisfies the conditions of Example 9.4.9(d) for being exponentiable in Pos, but which is not exponentiable in Dcpo. [Hint: the bilimit of the fibres over some ascending sequence fails to be the fibre over its directed join.]

42. How can Pasynkov's expression of spheres as partial products be used to calculate p₁(S¹), the fundamental group of the circle?

43. Assuming proof-anonymity, explain in terms of Theorem  9.5.3 why the results of comprehension are monos.

44. Show how to calculate the comprehension {G|F} of a list of propositions.

45. Give the equational formulation in a 2-category or bicategory ( cf Exercise 7.30) of the notion of a fibration with lex fibres, and of the same with comprehension. In this sense show that tgt:C^v® C freely adds comprehension to P:C® S, where the objects of C^v are the vertical morphisms of C; type-theoretically, this inserts an arbitrary division in the propositional part of contexts. [Hint: for uniqueness of the meditator between the total categories, you need to know that omitted diagram environment is a pullback in C^v, where

    G = TPF = TPY .] Although having comprehension is a property of the fibration, viz that an adjoint exists, this construction is not idempotent; explain why this is. In Section 5.3 we wanted to use fibrations and comprehension to add partial maps; does the construction achieve this goal?

46. What does it mean for a fibration P:C® S to have equality predicates corresponding to the types given by product diagonals in S (Section 8.3)? Assume that the fibres are all preorders. Construct the category of partial maps ( cf Propositions 5.3.5) and a fibration with comprehension whose objects are the virtual objects of the allegory ( cf footnote  pfn comp footn on page  pfn comp footn).

47. Assuming that P:C® S admits existential quantification, construct the allegory of relations (Proposition 5.8.7), and recover the comprehensive fibration using Freyd's tabular allegories [ FS90, §2.166].

48. Let S be the category of types in Zermelo type theory generated by 1, N, x and P ( cf Exercise 2.17), and all functions between them, so S is a full subcategory of Set which is closed under these operations but not under pullback. Carry out and contrast the constructions of the preceding three exercises for the predicate fibration P:C® S.

49. Discuss the commutation of comprehension and powerset with substitution ( cf Remark 9.1.11) and with the connectives and quantifiers ( cf Exercise  2.17). Show that all proposition-symbols except w can be eliminated, and that if types do not depend on proofs (Section 9.2) then the fibres P(G) are simply typed.

50. Describe the types w[x]xw[y] etc more explicitly and show that Ù, Ú and Þ make W into a Heyting lattice.

51. Reformulate the type-theoretic rules in Definition  9.5.5 so that, categorically, propositions over G are classified by spans G\twoheadleftarrow D ® Prop (with two pullbacks) instead of just maps G® Prop. Relate this to Remark 6.6.5 and Example 9.3.10(e). Rework Sections  9.5 and 9.6 with this definition, which is the one used in [JM95].

52. Let T:1® S in S be a support classifier (Definition 5.2.10). Suppose that S admits Þ , S^X exists for each X Î obE, the Leibniz principle holds (Proposition 2.8.7) and the quantifiers $:S^X® S and ":S^SX® S exist. Show that S is a topos and S = W [Tay98].

53. Show that the inverse image map !^*:S® S^X, where !:X® 1 in Sp, has a continuous right adjoint ( all_X) iff X is compact.

54. What are the assumptions behind Example  9.5.10(a)?

55. Implement Proposition  6.1.11 in a functional programming language with list- and function-types, showing that any free theory has an equationally free model without assuming propositional extensionality (Remark 9.5.10). Assume that Prop is a semilattice with structure and:Prop® Prop® Prop and true: Prop, and the type W of operation-symbols has an equality function eq:W® W® Prop.

56. Prove the second order representations of the propositional connectives and Leibniz' principle (Proposition  2.8.6ff), making use of proof-anonymity but not extensionality.

57. For any support classifier S (satisfying extensionality), show that aÙf(a) = aÙf(T) for G\vdash a:S and G, x:S\vdash f:S.

    [Hint: consider the subobject classified by