Practical Foundations of Mathematics
Paul Taylor
8.5 Exercises VIII

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.

Describe the stratified algebraic theory of 2categories.

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?

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?

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.

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.

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 = \id_{h*Y};\h_{Y} = g .]

Let e = [x: = a] and m = [^(y)] where
G\vdash a:X and D\vdash y:Y. Show that the diagonal
fillin 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 fillin is
unique, for all displays [^(y)] then e is an isomorphism,
ie X º \terminalobj_{G} . [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 fillins.]

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.

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

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

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

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 Dmaps.
Assuming that D is a subcategory closed under cofiltered limits,
extend the result to arbitrary simply connected diagrams.

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

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?

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.