Categorical Models of Type Theory Exercise Sheet 1
23.02.2022
Exercise 1.15
1. Given a A-term s with an occurrence of App(Ax.ti, t2), we obtain another term s' with an occurrence of ti[t2/x] by replacing App(Ax.t1; t2) in s by ti[t2/x]. In this case we say that s /3-contracts to s'. We say that s (5-reduces to s' if s' can be obtained from s by finitely many /3-contractions and changes of bound variables (a-congruences). We then write s' <p s. A /3-conversion is a finite sequence of /3-reductions and reversed /3-reductions. Two A-terms s,t are /3-congruent if there is a /3-conversion from s to t.
(a) Show that two A-terms s, t are /3-congruent if and only if A/3 h s := t.
(b) Show that two A-terms s,t are 77-congruent (defined accordingly by a finite sequence of (reversed) a-congruences, /3-reductions and rj-reductions) if and only ifA/3?7 h s := t.
2. For a A-theory A/3 C T C Ac, show that T h \j3rj if and only if T h / := 1, where 1 = Ax.Ay.App(x, y) denotes the first Church numeral.
3. For ti,t2 e Ac, let [ti,t2] = Az.App(App(z,ti),t2) for a variable z FV(ti) U FV(t2)- For i = 1, 2, let pr, = Ay.App(y, Axi.Ax2.Xi). Show that
A/3h App(prJ,[t1,t2]) :=U
for i = 0,1 (Pair-Elimination). Vice versa, one can show that it is not true that A/3 h t := [App(pr1; t), App(pr2, t)] for all t e Ac (Pair Uniqueness). This is in Barendregt's Book, Exercise 5.4.4, and more involved. That means, not every A-term is (provably) a pair of terms.
Exercise 1.16 For s e Ac, a finite set X = {x\,..., xn} of variables, and a finite set {ti,... ,tn} of A-terms, define the simultaneous substitution of (t^i < n) in s for (xi \ i < n) recursively as follows.
1. Xj[ti/xi]i<n = tj for all j < n.
2. a[ti/xi]i<n = a for all a e C U (Var \ X).
1
3. (Xx.s)[ti/xi]i<n = \xj.s[ t /~x^]i<n,i^j for j < n.
4. {Xx.s^U/x^Kn = Xy.slU/x,}^ if y e Var \(IU U<„FV(£4)) orlfl FV(s) = 0.
5. (Xx.s)[tl/xl]l<n = Xz.s[z/y][tl/xl]l<n if y e Ui<nFV(*i) \and ^n FV(s) = 0, for zeVar\(!U FV(s) U U,<„ FV(£4)) minimal.
6. App(si,s2)[ti/xi]i<n = App(si[ti/xi]i<n,S2[ti/xi]i<n).
Show the Substitution Lemma, i.e. for all A-terms Si,t\ for i = 1, 2, j < n, and for all pairwise distinct variables x\,... ,xn, show that if Xß h si := s2 and
A/3 :=    :=    for all j < n, then Xß h si[tj/xi]i<„ := S2[*iM]i<n-
Exercise II.3
1. Let {C* ) be an applicative structure and [■]: Val(C) xAc^Cbea function which satisfies Conditions 1,2 and 4 from the definition of a A-model (Definition II.1). The triple {C* , [■]) is said to satisfy Berry's Extensio-nality Property if for all s,t e Ac, all x,y e Var, and all p, a e Val(C), the following implication holds.
(VceC: IAx.S]p «c = IAx.t]ff #c)     [Aa;.a]p = IAx.t]ff
Show that the conjunction of Conditions 3,5 and 6 is equivalent to Berry's Extensionality Property.
2. Let (C*,* , [■]) be a A-model. Then for all s,t e Ac, x e Var, p e Val(C), we have
(a) Is[t/a;]]p = Wp[[t]p/a;],
(b) lApp(Xx.s,t)}p = ls[t/x}}p.
2