Page 97 - Textos de Matemática Vol. 40

2.3. Universes in explicit mathematics 85
(4) ∀f,x.inv(f,x) ∈ W → x ∈ W,
(5) ∀x, f.j(x, f) ∈ W → x ∈ W ∧ ∀y ∈˙ x.f y ∈ W, (6) ∀x, y.i(x, y) ∈ W → x ∈ W ∧ y ∈ W,
(7) ∀x.lx∈W →x∈W.
Accordingly, a type W is called a strict universe if it is a universe and if it satisfies the condition Str(W).
Definition 2.3.17. 1. We write SU(W) to express that the type W is a name strict universe,
SU(W) := U(W) ∧ Str(W).
2. We write SU(t) to express that the individual t is a name of a name strict
universe,
SU(t) := ∃X.R(t, X) ∧ SU(X).
Our old limit axiom (Lim) postulates that every name a belongs to a uni- verse which is named l a. In the context of name strictness, this axiom is now replaced by the corresponding limit axiom for name strict universes,
(sLim) ∀x.R(x)→SU(lx)∧x∈˙ lx.
Our definition of universe is too general for requiring that all universes are name strict. Following the pattern of the proof of Theorem 2.3.8 it is easy to see that, at least in the presence of (LEM-UG), there are universes that are not name strict.
Lemma 2.3.18. In EETJ + (sLim) + (LEM-UG), one can prove that ∃X.U(X) ∧ ¬SU(X).
Proof. Let S be the universe which is named by l(l(lnat)), and let T be the type S \{l nat}. As in the proof of Theorem 2.3.8, we realize that T is a universe. However, T obviously does not contain the element lnat, although it contains l (l nat). Hence T is not name strict. ⊣
The model construction of Ja¨ger and Studer [JS02b] shows that all proof-theoretic equivalences mentioned in the first two parts of Theorem 2.3.10 remain true if we replace the limit axiom (Lim) by our new axiom (sLim). The same should be the case for parts three and four of that Theorem.
We end this Section with a simple example which illustrates the usefulness of name strict universes. Suppose that we want a universe which contains two given names a and b. In the presence of (sLim) we can proceed as follows. We first select the name du(a, b), the disjoint union of the types named by a and b (cf. proof of Theorem 2.3.13). Then we form l(du(a,b)). Because of name