nLab Tarski universe

Redirected from "strict Tarski universes".
Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Equality and Equivalence

Universes

Contents

Idea

In intensional type theory and homotopy type theory, there are typically two ways to construct a “type of small types”. One way is by Russell universes, where an element A:UA:U of a type universe UU is literally a type AtypeA \; \mathrm{type}. The alternative is by Tarski universes, where elements A:UA:U are not literally types, but rather the universe type UU comes with the additional structure of a type family TT, such that the dependent type T(A)T(A) represents the actual type. Usually universes are defined in intensional type theory and homotopy type theory using derivations and inference rules, such as the type reflection rule

ΓA:UΓT(A)type\frac{\Gamma \vdash A:U}{\Gamma \vdash T(A) \; \mathrm{type}}

for Tarski universes. Furthermore, universes are usually defined as being closed under all type formers inside the type theory, regardless of the type theory.

However, this approach of defining Tarski universes means that the notion of “Tarski universe” differs from type theory to type theory. By this approach, a Tarski universe in the bare intensional Martin-Löf type theory, which has identity types, dependent product types, dependent sum types, an empty type, a unit type, a booleans type, and a natural numbers type, would not be considered a Tarski universe in homotopy type theory, since it is missing important type formers present in homotopy type theory, such as internal pushout types, a torus type?, propositional truncations, W-types, and localizations. On the other hand, one could consider an even more spartan type theory which doesn’t even have the unit type, let alone the empty type, the natural numbers type, and the booleans type, whose Tarski universes are thus consisting of only internal identity types, dependent product types, dependent sum types.

All three notions of Tarski universe described above are in fact definable in all three versions of intensional type theory mentioned above, but Tarski universes are usually described as having, apart from addiitonal internal Tarski universes, exactly the internal type formers that the external type theory has. One usually doesn’t consider Tarski universes with an internal James construction type in bare intensional Martin-Löf type theory, even though a Tarski universe closed under James constructions is definable in Martin-Löf type theory. On the other hand, in homotopy type theory the name “Tarski universe” isn’t usually used for a universe only closed under identity types, dependent product types, dependent sum types.

From a global perspective, however, all of these types should be considered Tarski universes, since they model some notion of type of small types, even though the small types in the universe do not behave as the external types in the type theory do. And that is how we approach Tarski universes in this article: Tarski universes are a very general notion encompassing all of the above notions of Tarski universe and more, and one could describe more specific versions of Tarski universes by adding additional structure and axioms to Tarski universes, in the same way one adds additional structure and axioms to an abelian group to get a ring, a commutative ring, a RR-module, a RR-algebra, and an RR-commutative algebra. We could then study in general Tarski universes and their properties as we do for abelian groups and rings. This requires a shift in the point of view of what Tarski universes are: Tarski universes are actual mathematical structure in intensional type theory, rather than being something in the foundations of mathematics to merely address size? issues or do mathematics in.

Definition

With a family of types

A Tarski universe or universe à la Tarski is simply a type UU with a type family TT whose dependent types T(A)T(A) are indexed by elements A:UA:U. The elements A:UA:U are usually called UU-small types, or small types for short, and T(A)T(A) is the type of elements of AA.

With a type and a function

A Tarski universe or universe à la Tarski is a type UU of all UU-small types with a type TT' of all elements, and a function typeOf:TU\mathrm{typeOf}:T' \to U which gets the associated type for every element a:Ta:T'.

Equivalence of definitions

From one direction, the individual dependent types T(A)T(A) could be defined as the fiber type of typeOf\mathrm{typeOf} at AA

T(A)fiber T,U(typeOf,A) t:TtypeOf(t)= UAT(A) \coloneqq \mathrm{fiber}_{T', U}(\mathrm{typeOf},A) \equiv \sum_{t:T'} \mathrm{typeOf}(t) =_U A

From the other direction, the entire type of elements TT' is just the dependent sum type of all the type reflections of small types

T A:UT(A)T' \coloneqq \sum_{A:U} T(A)

We shall be using the first definition throughout this article, but everything could be translated into the second definition of a Tarski universe.

Tarski universes as models of type theory

The definitions above are already enough to build an internal model of dependent type theory inside the Tarski universe:

  • The type AtypeA \; \mathrm{type} is represented by the small type A:UA:U
  • The element a:Aa:A is represented by the element a:T(A)a:T(A) for small type A:UA:U.
  • The type family BB indexed by the type AtypeA \; \mathrm{type} is represented by the function B:T(A)UB:T(A) \to U for small type A:UA:U
  • The dependent type a:ABtypea:A \vdash B \; \mathrm{type} is represented by the section B(a):UB(a):U for element a:T(A)a:T(A) and small type A:UA:U.
  • The section a:Ab:Ba:A \vdash b:B is represented by the element b:T(B(a))b:T(B(a)) for element a:T(A)a:T(A) and small type A:UA:U.

Properties

Univalence

There are two notions of equivalence in a Tarski universe (U,T)(U, T), equality A= UBA =_U B and equivalence T(A)T(B)T(A) \simeq T(B). By the properties of the identity type, there is a canonical transport dependent function

transport T: A:U B:U(A= UB)T(A)T(B)\mathrm{transport}^T:\prod_{A:U} \prod_{B:U} (A =_U B) \to T(A) \simeq T(B)

A Tarski universe is a univalent Tarski universe if for all elements A:UA:U and B:UB:U the function transport T(A,B)\mathrm{transport}^T(A, B) is an equivalence of types

A:U B:UisEquiv(transport T(A,B))\prod_{A:U} \prod_{B:U} \mathrm{isEquiv}(\mathrm{transport}^T(A, B))

This is the extensionality principle for any Tarski universe (U,T)(U, T).

Equivalently, by the fundamental theorem of identity types, a Tarski universe is a univalent Tarski universe if it comes with a dependent function

t: X:UC(X,X,id X)J(t): A:U B:U R:T(A)T(B)C(A,B,R)t:\prod_{X:U} C(X, X, \mathrm{id}_X) \vdash J(t):\prod_{A:U} \prod_{B:U} \prod_{R:T(A) \simeq T(B)} C(A, B, R)

and a dependent function

t: X:UC(X,X,id X)β(t): A:UJ(t,A,A,id A)= C(A,A,id A)t(A)t:\prod_{X:U} C(X, X, \mathrm{id}_X) \vdash \beta(t):\prod_{A:U} J(t, A, A, \mathrm{id}_A) =_{C(A, A, \mathrm{id}_A)} t(A)

When the Tarski universe is closed under identity types, dependent sum types, and dependent product types (see below for more on closure of Tarski universes under type formers), one is able to internalize the type of equivalences in the universe as A UBA \simeq_U B. It can be proven that T(A UB)T(A \simeq_U B) is equivalent to T(A)T(B)T(A) \simeq T(B), and that the definition of univalence using transport is equivalent to the usual definition given by the internal type of equivalences and the canonical function idtoequiv\mathrm{idtoequiv}. See at Univalence axiom#For Tarski universes for more details on this.

Construction of univalent Tarski universes via a higher inductive type

Let (U,T)(U, T) be a Tarski universe. Then one could construct a univalent Tarski universe as the higher inductive type (U,T)(U', T') generated by

  • a function F:UUF:U \to U'
  • a function G(A):T(A)T(A)G(A):T(A) \to T'(A) for all elements a:Ua:U
  • a dependent function
    ua U: A:U B:UisEquiv(transport T(A,B))\mathrm{ua}_{U'}:\prod_{A:U} \prod_{B:U} \mathrm{isEquiv}(\mathrm{transport}^{T'}(A, B))

Regularity and product-regularity

A univalent Tarski universe (U,T)(U, T) is regular if it is closed under dependent sum types: namely, for all UU-small types A:UA:U and UU-small type families B:T(A)UB:T(A) \to U, the dependent sum type x:T(A)T(B(x))\sum_{x:T(A)} T(B(x)) is essentially U U -small.

ax Σ: Σ: A:U(T(A)U)U A:U B:T(A)UT(Σ(A,B)) x:T(A)T(B(x))\mathrm{ax}_\Sigma:\sum_{\Sigma:\prod_{A:U} (T(A) \to U) \to U} \prod_{A:U} \prod_{B:T(A) \to U} T(\Sigma(A, B)) \simeq \sum_{x:T(A)} T(B(x))

Regular univalent Tarski universes are the type theoretic equivalent of regular cardinals in set theory.

A univalent Tarski universe (U,T)(U, T) is product-regular if it is closed under dependent product types: namely, for all UU-small types A:UA:U and UU-small type families B:T(A)UB:T(A) \to U, the dependent product type x:T(A)T(B(x))\sum_{x:T(A)} T(B(x)) is essentially U U -small.

ax Π: Π: A:U(T(A)U)U A:U B:T(A)UT(Π(A,B)) x:T(A)T(B(x))\mathrm{ax}_\Pi:\sum_{\Pi:\prod_{A:U} (T(A) \to U) \to U} \prod_{A:U} \prod_{B:T(A) \to U} T(\Pi(A, B)) \simeq \prod_{x:T(A)} T(B(x))

Product-regular univalent Tarski universes are the type theoretic equivalent of product-regular cardinals in set theory.

Since product-regularity implies that function types between UU-small types are essentially UU-small, and regularity implies that subtypes of essentially UU-small types are essentially UU-small, this implies that in a regular and product-regular universe, equivalence types between UU-small types are essentially UU-small, because equivalence types are subtypes of function types. In combination with univalence, regularity and product-regularity implies that the identity types between UU-small types are also essentially UU-small.

Closure under identity types

A univalent Tarski universe (U,T)(U, T) is closed under identity types if for all UU-small types A:UA:U and elements x:T(A)x:T(A) and y:T(A)y:T(A), the identity type x= T(A)yx =_{T(A)} y is essentially U U -small.

ax Id: Id: A:U(T(A)×T(A))U A:U x:T(A) y:T(A)T(Id(A,x,y))(x= T(A)y)\mathrm{ax}_\mathrm{Id}:\sum_{\mathrm{Id}:\prod_{A:U} (T(A) \times T(A)) \to U} \prod_{A:U} \prod_{x:T(A)} \prod_{y:T(A)} T(\mathrm{Id}(A, x, y)) \simeq (x =_{T(A)} y)

Regularity and closure under identity types implies that the universe is closed under pullbacks.

Singletons

A univalent Tarski universe satisfies the axiom of singletons if it is closed under the (weak) unit type: if the unit type 𝟙\mathbb{1} is essentially UU-small. The axiom of singletons comes from the formation rule, the introduction rules, and the dependent universal property of the natural numbers, which are represented by the following elements:

  • formation rules: 𝟙:U\mathbb{1}:U

  • introduction rules: 0:T(𝟙)0:T(\mathbb{1})

and either an universal property or a dependent universal property

  • universal property:

    up 𝟙 U: C:U c 0:T(C)!c:T(𝟙)T(C).(c(0)= T(C)c 0)\mathrm{up}_\mathbb{1}^U:\prod_{C:U} \prod_{c_0:T(C)} \exists!c:T(\mathbb{1}) \to T(C).(c(0) =_{T(C)} c_0)
  • dependent universal property:

    dup 𝟙 U: C:T(𝟙)U c 0:T(C(0))!c: x:T(𝟙)T(C(x)).(c(0)= T(C(0))c 0)\mathrm{dup}_\mathbb{1}^U:\prod_{C:T(\mathbb{1}) \to U} \prod_{c_0:T(C(0))} \exists!c:\prod_{x:T(\mathbb{1})} T(C(x)).(c(0) =_{T(C(0))} c_0)

    where !x:A.B(x)\exists!x:A.B(x) is the uniqueness quantifier for the type family x:AB(x)x:A \vdash B(x).

By using dependent sum types, these can be combined into a single element of the following types

axsingl U: 𝟙:U 0:T(𝟙) C:U c 0:T(C)!c:T(𝟙)T(C).(c(0)= T(C)c 0)\mathrm{axsingl}_U:\sum_{\mathbb{1}:U} \sum_{0:T(\mathbb{1})} \prod_{C:U} \prod_{c_0:T(C)} \exists!c:T(\mathbb{1}) \to T(C).(c(0) =_{T(C)} c_0)
axsingl U: 𝟙:U 0:T(𝟙) C:𝟙U c 0:T(C(0))!c: x:T(𝟙)T(C(x)).(c(0)= T(C(0))c 0)\mathrm{axsingl}_U:\sum_{\mathbb{1}:U} \sum_{0:T(\mathbb{1})} \prod_{C:\mathbb{1} \to U} \prod_{c_0:T(C(0))} \exists!c:\prod_{x:T(\mathbb{1})} T(C(x)).(c(0) =_{T(C(0))} c_0)

Alternatively, since the notion of truth could be defined using the type of UU-small contractible types A:UisContr(T(A))\sum_{A:U} \mathrm{isContr}(T(A)), the axiom of singletons could be represented as a resizing axiom, similar to propositional resizing.

A univalent Tarski universe (U,T)(U, T) satisfies the axiom of singletons if it is closed under the type of all UU-small contractible types: namely, the dependent sum type A:UisContr(T(A))\sum_{A:U} \mathrm{isContr}(T(A)) is essentially U U -small:

axSingl U: 𝟙:UT(𝟙) A:UisContr(T(A))\mathrm{axSingl}_U:\sum_{\mathbb{1}:U} T(\mathbb{1}) \simeq \sum_{A:U} \mathrm{isContr}(T(A))

Empty type

A univalent Tarski universe satisfies the axiom of empty type if it is closed under the (weak) empty type: if the empty type \emptyset is essentially UU-small. The axiom of empty type comes from the formation rule and the dependent universal property of the empty type, which are represented by the following elements:

  • formation rules: :U\emptyset:U

and either an universal property or a dependent universal property

up U: C:UisContr(T()T(C))\mathrm{up}_\emptyset^U:\prod_{C:U} \mathrm{isContr}\left(T(\emptyset) \to T(C)\right)
  • dependent universal property:
    up U: C:T()UisContr( x:T()T(C(x)))\mathrm{up}_\emptyset^U:\prod_{C:T(\emptyset) \to U} \mathrm{isContr}\left(\prod_{x:T(\emptyset)} T(C(x))\right)

By using dependent sum types, these can be combined into a single element of the following types

axempty U: :U C:UisContr(T()T(C))\mathrm{axempty}_U:\sum_{\emptyset:U} \prod_{C:U} \mathrm{isContr}\left(T(\emptyset) \to T(C)\right)
axempty U: :U C:T()UisContr( x:T()T(C(x)))\mathrm{axempty}_U:\sum_{\emptyset:U} \prod_{C:T(\emptyset) \to U} \mathrm{isContr}\left(\prod_{x:T(\emptyset)} T(C(x))\right)

Alternatively, since falsehood or the empty proposition could be defined using the type of UU-small propositions A:UisProp(T(A))\sum_{A:U} \mathrm{isProp}(T(A)), the axiom of empty set could be represented as a resizing axiom, similar to propositional resizing.

A univalent Tarski universe (U,T)(U, T) satisfies the axiom of empty type if it is closed under the empty proposition or falsehood: namely, the dependent product type A:PropUT(A)\prod_{A:\mathrm{Prop}}_U T(A) is essentially U U -small:

axempty U: :UT() A:Prop UT(A)\mathrm{axempty}_U:\sum_{\emptyset:U} T(\emptyset) \simeq \prod_{A:\mathrm{Prop}_U} T(A)

where

Prop U A:UisProp(T(A))\mathrm{Prop}_U \equiv \sum_{A:U} \mathrm{isProp}(T(A))

Product regularity and the axiom of empty type imply the axiom of singletons, because the dependent universal property of the empty set states that for every type family C:T(𝟘)UC:T(\mathbb{0}) \to U the dependent function type x:T(𝟘)T(C(x))\prod_{x:T(\mathbb{0})} T(C(x)) is a singleton, and product regularity implies that x:T(𝟘)T(C(x))\prod_{x:T(\mathbb{0})} T(C(x)) is essentially UU-small.

Propositional resizing

A univalent Tarski universe (U,T)(U, T) satisfies propositional resizing if it is closed under the type of all U U -small propositions: namely, the dependent sum type A:UisProp(T(A))\sum_{A:U} \mathrm{isProp}(T(A)) is essentially U U -small:

propresize U: Ω:UT(Ω) A:UisProp(T(A))\mathrm{propresize}_U:\sum_{\Omega:U} T(\Omega) \simeq \sum_{A:U} \mathrm{isProp}(T(A))

This is a version internal to the universe UU of having a type of all propositions in the type theory itself. While propositional resizing implies that the universe is impredicative, it does not imply that the type theory as a whole is impredicative; the latter requires an actual type of all propositions in the type theory.

Product regularity and propositional resizing imply the axiom of empty set, because propositional resizing implies that Prop U\mathrm{Prop}_U is essentially UU-small, and then product regularity implies that A:Prop UT(A)\prod_{A:\mathrm{Prop}_U} T(A) is essentially UU-small.

Infinity

A univalent Tarski universe satisfies the axiom of infinity if it is closed under the (weak) natural numbers type: if the natural numbers type \mathbb{N} is essentially UU-small. The axiom of infinity comes from the formation rule, the introduction rules, and the dependent universal property of the natural numbers, which are represented by the following elements:

  • formation rules: :U\mathbb{N}:U

  • introduction rules: 0:T()0:T(\mathbb{N}) and s:T()T()s:T(\mathbb{N}) \to T(\mathbb{N})

and either an universal property or a dependent universal property

  • universal property:

    up U:: C:U c 0:T(C) c s:T(C)T(C)!c:T()T(C).(f(0)= T(C)c 0)× n:T()c(s(n))= T(C)c s(c(n))\mathrm{up}_\mathbb{N}^U::\prod_{C:U} \prod_{c_0:T(C)} \prod_{c_s:T(C) \to T(C)} \exists!c:T(\mathbb{N}) \to T(C).(f(0) =_{T(C)} c_0) \times \prod_{n:T(\mathbb{N})} c(s(n)) =_{T(C)} c_s(c(n))
  • dependent universal property:

    dup U: C:U c 0:T(C(0)) c s: x:T(C(x))T(C(s(x)))!c: x:T(C(x)).(c(0)= T(C(0))c 0)× x:(c(s(x))= T(C(s(x)))c s(c(x)))\mathrm{dup}_\mathbb{N}^U:\prod_{C:\mathbb{N} \to U} \prod_{c_0:T(C(0))} \prod_{c_s:\prod_{x:\mathbb{N}} T(C(x)) \to T(C(s(x)))} \exists!c:\prod_{x:\mathbb{N}} T(C(x)).(c(0) =_{T(C(0))} c_0) \times \prod_{x:\mathbb{N}} (c(s(x)) =_{T(C(s(x)))} c_s(c(x)))

    where !x:A.B(x)\exists!x:A.B(x) is the uniqueness quantifier for the type family x:AB(x)x:A \vdash B(x).

By using dependent sum types, these can be combined into a single element of the following types:

axinf U: :U 0:T() s:T()T() C:U c 0:T(C) c s:T(C)T(C)!c:T()T(C).(f(0)= T(C)c 0)× n:T()c(s(n))= T(C)c s(c(n))\mathrm{axinf}_U:\sum_{\mathbb{N}:U} \sum_{0:T(\mathbb{N})} \sum_{s:T(\mathbb{N}) \to T(\mathbb{N})} \prod_{C:U} \prod_{c_0:T(C)} \prod_{c_s:T(C) \to T(C)} \exists!c:T(\mathbb{N}) \to T(C).(f(0) =_{T(C)} c_0) \times \prod_{n:T(\mathbb{N})} c(s(n)) =_{T(C)} c_s(c(n))

or

axinf U: :U 0:T() s:T()T() C:T()U c 0:T(C(0)) c s: x:T()T(C(x))T(C(s(x)))!c: x:T()T(C(x)).(c(0)= T(C(0))c 0)× x:T()(c(s(x))= T(C(s(x)))c s(c(x)))\mathrm{axinf}_U:\sum_{\mathbb{N}:U} \sum_{0:T(\mathbb{N})} \sum_{s:T(\mathbb{N}) \to T(\mathbb{N})} \prod_{C:T(\mathbb{N}) \to U} \prod_{c_0:T(C(0))} \prod_{c_s:\prod_{x:T(\mathbb{N})} T(C(x)) \to T(C(s(x)))} \exists!c:\prod_{x:T(\mathbb{N})} T(C(x)).(c(0) =_{T(C(0))} c_0) \times \prod_{x:T(\mathbb{N})} (c(s(x)) =_{T(C(s(x)))} c_s(c(x)))

Alternatively, since the type of all U U -small finite types and set truncations could be defined using the type of UU-small propositions A:UisProp(T(A))\sum_{A:U} \mathrm{isProp}(T(A)), the axiom of infinity could be represented as a resizing axiom, similar to propositional resizing.

A univalent Tarski universe (U,T)(U, T) satisfies the axiom of infinity if it is closed under the set truncation of the type of all U U -small finite types: namely, the type [ A:UisFinite(T(A))] 0\left[\sum_{A:U} \mathrm{isFinite}(T(A))\right]_0 is essentially U U -small:

axinf U: :UT()[ A:UisFinite(T(A))] 0\mathrm{axinf}_U:\sum_{\mathbb{N}:U} T(\mathbb{N}) \simeq \left[\sum_{A:U} \mathrm{isFinite}(T(A))\right]_0

where

isFinite(A) S:(AProp U)Prop U(((λx:A.)S)× P:AProp U Q:AProp U(PS) ×(!x:A.xQ)×(PQ= AProp Uλx:A.)(PQS))((λx:A.)S) \mathrm{isFinite}(A) \equiv \begin{array}{c} \prod_{S:(A \to \mathrm{Prop}_U) \to \mathrm{Prop}_U} (((\lambda x:A.\bot) \in S) \times \prod_{P:A \to \mathrm{Prop}_U} \prod_{Q:A \to \mathrm{Prop}_U} (P \in S) \\ \times (\exists!x:A.x \in Q) \times (P \cap Q =_{A \to \mathrm{Prop}_U} \lambda x:A.\bot) \to (P \cup Q \in S)) \to ((\lambda x:A.\top) \in S) \end{array}

and

Prop U A:UisProp(T(A))\mathrm{Prop}_U \equiv \sum_{A:U} \mathrm{isProp}(T(A))

The membership relation and the subtype operations used above are defined in the nLab article on subtypes.

Replacement

A univalent Tarski universe satisfies the axiom of replacement if for every essentially U U -small type AA, every locally U U -small type BB, and every function f:ABf:A \to B, the image of ff, im(f)\mathrm{im}(f), is essentially UU-small.

Equivalently, given types AA and BB, there is a function

axrepl U A,B:( C:UT(C)A)×( R:B×BU a:B b:BT(R(a,b))(a= Bb))( I:(AB)U f:ABT(I(f))im(f))\mathrm{axrepl}_U^{A, B}:\left(\sum_{C:U} T(C) \simeq A\right) \times \left(\sum_{R:B \times B \to U} \prod_{a:B} \prod_{b:B} T(R(a, b)) \simeq (a =_B b)\right) \to \left(\sum_{I:(A \to B) \to U} \prod_{f:A \to B} T(I(f)) \simeq \mathrm{im}(f)\right)

Excluded middle

A univalent Tarski universe (U,T)(U, T) satisfies excluded middle if all UU-small propositions are decidable propositions:

lem U: A:UisProp(T(A))[T(A)+¬T(A)]\mathrm{lem}_U:\prod_{A:U} \mathrm{isProp}(T(A)) \to [T(A) + \neg T(A)]

Theorem

Suppose that there is a univalent Tarski universe closed under dependent product types, dependent sum types, and identity types, and satisfying the axiom of infinity and excluded middle. Then the limited principle of omniscience for natural numbers LPO \mathrm{LPO}_\mathbb{N} holds in the type theory itself.

Proof

The type of all UU-small propositions Prop U\mathrm{Prop}_U is a σ \sigma -frame, and thus the homotopy-initial σ\sigma-frame Σ\Sigma is a sub-σ\sigma-frame of Prop U\mathrm{Prop}_U, with the following embedding of types

boolΣProp U\mathrm{bool} \hookrightarrow \Sigma \hookrightarrow \mathrm{Prop}_U

The first embedding is a unique distributive lattice homomorphism, since the boolean domain is the homotopy-initial distributive lattice, and the second embedding is a unique σ\sigma-frame homomorphism, by definition of homotopy-initial σ\sigma-frame. Excluded middle for UU implies that Prop U\mathrm{Prop}_U is equivalent to the boolean domain and to Σ\Sigma, implying that the boolean domain is the initial σ \sigma -frame, which then implies LPO \mathrm{LPO}_\mathbb{N}.

Choice

A univalent Tarski universe satisfies the axiom of choice if for every UU-small type A:UA:U and every UU-small type family B:T(A)UB:T(A) \to U, and for every every UU-small type family C: x:T(A)T(B(x))UC:\prod_{x:T(A)} T(B(x)) \to U, if T(A)T(A) is a set and each T(B(x))T(B(x)) is a set for all x:T(A)x:T(A), and each T(C(x,y))T(C(x, y)) is a proposition for all x:T(A)x:T(A) and y:T(B(x))y:T(B(x)), then if for all x:Ax:A there merely exists a y:T(B(x))y:T(B(x)) such that T(C(x,y))T(C(x, y)), then there merely exists a dependent function g: x:T(A)T(B(x))g:\prod_{x:T(A)} T(B(x)) such that for all x:T(A)x:T(A), T(C(x,g(x)))T(C(x, g(x))).

choice U: A:U B:T(A)U C: x:T(A)T(B(x))U (isSet(T(A))× x:T(A)(isSet(T(B(x)))× y:T(B(x))isProp(T(C(x,y))))) x:T(A).y:T(B(x)).T(C(x,y))g: x:T(A)T(B(x)).x:T(A).T(C(x,g(x)))\mathrm{choice}_U: \begin{array}{c} \prod_{A:U} \prod_{B:T(A) \to U} \prod_{C:\prod_{x:T(A)} T(B(x)) \to U} \\ \left(\mathrm{isSet}(T(A)) \times \prod_{x:T(A)} \left(\mathrm{isSet}(T(B(x))) \times \prod_{y:T(B(x))} \mathrm{isProp}(T(C(x, y)))\right)\right) \\ \to \forall x:T(A).\exists y:T(B(x)).T(C(x, y)) \to \exists g:\prod_{x:T(A)} T(B(x)).\forall x:T(A).T(C(x, g(x))) \end{array}

Choice operators and existence

A choice operator on a type is a function from its propositional truncation to the type itself, and represents the concept that if there exists an element of the set (i.e. the propositional truncation has an element), then the set itself has an element chosen by the choice operator. A Tarski universe satisfies the type-theoretic axiom of existence if every UU-small type in the Tarski universe has a choice operator, represented by the following dependent function

ε U: A:U|T(A)|T(A)\varepsilon_U:\prod_{A:U} \vert T(A) \vert \to T(A)

UU satisfying the type-theoretic axiom of existence implies that UU satisfies axiom K or UIP. If UU is also univalent, then it is an h-groupoid.

Closure of Tarski universes under other type formers

There are many ways of defining type formers internally in a universe:

Using a definitional equality with an existing global type former for each type former results in a strict Tarski universe, while using equivalences for each type former results in a weak Tarski universe. There are also various Tarski universes where some type formers are strictly closed, and some type formers are only weakly closed, resulting in Tarski universes which are intermediate between strict Tarski universes and weak Tarski universes.

Tarski universes with all propositions

A Tarski universe (U,T)(U, T) has all propositions if given a type AA with a family of identities x:A,y:Aτ 1(x,y):x= Ayx:A, y:A \vdash \tau_{-1}(x, y):x =_A y, the universe UU comes with the structure of an element A U:UA_U:U and an equivalence δ A:T(A U)A\delta_A:T(A_U) \simeq A.

The rules for this condition on Tarski universes is as follows:

ΓAtypeΓ,x:A,y:Aτ 1(x,y):x= AyΓA U:UΓAtypeΓ,x:A,y:Aτ 1(x,y):x= AyΓδ A:T(A U)A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A \vdash \tau_{-1}(x, y):x =_A y}{\Gamma \vdash A_U:U} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A \vdash \tau_{-1}(x, y):x =_A y}{\Gamma \vdash \delta_A:T(A_U) \simeq A}

Given a Tarski universe which has all propositions, the type A:UisProp(T(A))\sum_{A:U} \mathrm{isProp}(T(A)) is the type of all propositions. This is a form of strong impredicativity in the type theory, as given a type AA, the type A A:UisProp(T(A))A \to \sum_{A:U} \mathrm{isProp}(T(A)) is the power set on AA.

Tarski subuniverses

Let (U,T U)(U, T_U) be a Tarski universe. A Tarski universe (V,T V)(V, T_V) is a Tarski subuniverse of (U,T U)(U, T_U) if it comes with an embedding t:VUt:V \hookrightarrow U and a dependent function

p: a:VT U(t(a))T V(a)p:\prod_{a:V} T_U(t(a)) \simeq T_V(a)

This is equivalent to a family of Tarski universes (U(i),T(i))(U(i), T(i)) indexed by elements i:𝟚i:\mathbb{2} of the interval preorder (𝟚, 𝟚)(\mathbb{2}, \leq_\mathbb{2}), which comes with

  • a dependent function

    t: a:𝟚 b:𝟚(a 𝟚b)(U(a)U(b))t:\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} (a \leq_\mathbb{2} b) \to (U(a) \hookrightarrow U(b))
  • a dependent function

    q: a:𝟚 b:𝟚 p:a 𝟚b A:U(a)T(a)(A)T(b)(t(a,b)(p)(A))q:\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} \prod_{p:a \leq_\mathbb{2} b} \prod_{A:U(a)} T(a)(A) \simeq T(b)(t(a, b)(p)(A))

    indicating that lifting each small type results in a type equivalent to the original small type.

Modalities and comodalities

A modal operator on a Tarski universe (U,T)(U, T) is just an endofunction L:UUL:U \to U. Given a Tarski universe, the modal unit family is a family of functions

η: L:UU A:UT(A)T(L(A))\eta:\prod_{L:U \to U}\prod_{A:U} T(A) \to T(L(A))

and the comodal counit family is a family of functions

ϵ: L:UU A:UT(L(A))T(A)\epsilon:\prod_{L:U \to U}\prod_{A:U} T(L(A)) \to T(A)

Given a modal operator L:UUL:U \to U, η(L)\eta(L) is called the modal unit of LL and ϵ(L)\epsilon(L) is called the comodal counit of LL. A small type A:UA:U is LL-modal if the function

η(L)(A):T(A)T(L(A))\eta(L)(A):T(A) \to T(L(A))

is an equivalence of types, and LL-comodal if the function

ϵ(L)(A):T(L(A))T(A)\epsilon(L)(A):T(L(A)) \to T(A)

is an equivalence of types.

A modality is…

…and a comodality is…

Reflective and coreflective Tarski subuniverses

(Section under construction see reflective subuniverse for the Russell universe variant for the time being)

Essentially small Tarski universes

A Tarski universe (V,T V)(V, T_V) inside of a Tarski universe (U,T U)(U, T_U) consists of an element V:UV:U and a function T V:T U(V)UT_V:T_U(V) \to U.

Given a Tarski universe (U,T U)(U, T_U), a Tarski universe (V,T V)(V, T_V) is essentially UU-small if it comes with

  • an element V:UV':U

  • a function T V:T U(V)UT_{V'}:T_U(V') \to U

  • an equivalence

    smallType:VT U(V)\mathrm{smallType}:V \simeq T_U(V')
  • a dependent function

    smallFamily: A:VT V(A)T U(T V(smallType(A)))\mathrm{smallFamily}:\prod_{A:V} T_V(A) \simeq T_U(T_{V'}(\mathrm{smallType}(A)))

Equivalently, the entire structure could be regarded as a family of Tarski universes (U(a),T(a))(U(a), T(a)) indexed by elements a:𝟚a:\mathbb{2} of the interval preorder (𝟚, 𝟚)(\mathbb{2}, \leq_\mathbb{2}), which comes with

  • a dependent function

    U: a:𝟚 b:𝟚 p:a 𝟚b((b 𝟚a))U(b)U':\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} \prod_{p:a \leq_\mathbb{2} b} \left((b \leq_\mathbb{2} a) \to \emptyset\right) \to U(b)
  • a dependent function

    T: a:𝟚 b:𝟚 p:a 𝟚b((b 𝟚a))(T(b)(U(a,b,p))U(b))T':\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} \prod_{p:a \leq_\mathbb{2} b} \left((b \leq_\mathbb{2} a) \to \emptyset\right) \to \left(T(b)(U'(a, b, p)) \to U(b)\right)
  • an dependent function

    smallType: a:𝟚 b:𝟚 p:a 𝟚b((b 𝟚a))(U(a)T(b)(U(a,b,p)))\mathrm{smallType}:\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} \prod_{p:a \leq_\mathbb{2} b} \left((b \leq_\mathbb{2} a) \to \emptyset\right) \to \left(U(a) \simeq T(b)(U'(a, b, p))\right)
  • a dependent function

    smallFamily: a:𝟚 b:𝟚 p:a 𝟚b((b 𝟚a)) A:U(a)T(a)(A)T(b)(T(a,b,p)(smallType(a,b,p)(A)))\mathrm{smallFamily}:\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} \prod_{p:a \leq_\mathbb{2} b} \left((b \leq_\mathbb{2} a) \to \emptyset\right) \to \prod_{A:U(a)} T(a)(A) \simeq T(b)(T'(a, b, p)(\mathrm{smallType}(a, b, p)(A)))

Hierarchy of Tarski universes

Let PP be a preorder. Then, a PP-indexed hierarchy of Tarski universes is a type family UU such that for all indices a:Pa:P, there is a Tarski universe (U(a),T(a))(U(a), T(a)), such that for all indices a:Pa:P and b:Pb:P and witnesses p:a Pbp:a \leq_P b, the Tarski universe (U(a),T(a))(U(a), T(a)) is an essentially U(b)U(b)-small Tarski subuniverse of the Tarski universe (U(b),T(b))(U(b), T(b)).

Expanded out, the family of Tarski universes (U(a),T(a))(U(a), T(a)) indexed by elements a:Pa:P additionally come with

  • a dependent function

    U: a:P b:P p:a Pb((b Pa))U(b)U':\prod_{a:P} \prod_{b:P} \prod_{p:a \leq_P b} \left((b \leq_P a) \to \emptyset\right) \to U(b)
  • a dependent function

    T: a:P b:P p:a Pb((b Pa))(T(b)(U(a,b,p))U(b))T':\prod_{a:P} \prod_{b:P} \prod_{p:a \leq_P b} \left((b \leq_P a) \to \emptyset\right) \to \left(T(b)(U'(a, b, p)) \to U(b)\right)
  • an dependent function

    smallType: a:P b:P p:a Pb((b Pa))(U(a)T(b)(U(a,b,p)))\mathrm{smallType}:\prod_{a:P} \prod_{b:P} \prod_{p:a \leq_P b} \left((b \leq_P a) \to \emptyset\right) \to \left(U(a) \simeq T(b)(U'(a, b, p))\right)
  • a dependent function

    smallFamily: a:P b:P p:a Pb((b Pa)) A:U(a)T(a)(A)T(b)(T(a,b,p)(smallType(a,b,p)(A)))\mathrm{smallFamily}:\prod_{a:P} \prod_{b:P} \prod_{p:a \leq_P b} \left((b \leq_P a) \to \emptyset\right) \to \prod_{A:U(a)} T(a)(A) \simeq T(b)(T'(a, b, p)(\mathrm{smallType}(a, b, p)(A)))
  • a dependent function

    t: a:P b:P(a Pb)(U(a)U(b))t:\prod_{a:P} \prod_{b:P} (a \leq_P b) \to (U(a) \hookrightarrow U(b))
  • a dependent function

    q: a:P b:P p:a Pb A:U(a)T(a)(A)T(b)(t(a,b)(p)(A))q:\prod_{a:P} \prod_{b:P} \prod_{p:a \leq_P b} \prod_{A:U(a)} T(a)(A) \simeq T(b)(t(a, b)(p)(A))

Usually, hierarchies of Tarski universes are indexed by the type of natural numbers. A type theory may have multiple hierarchies of type universes.

Examples

Cumulative hierarchy

Any cumulative hierarchy VV with a membership relation \in is a Tarski universe with universal type family

x:VEl(x) y:Vyxx:V \vdash \mathrm{El}(x) \coloneqq \sum_{y:V} y \in x

This is not a univalent universe if the von Neumann universe satisfies the set-theoretic axiom of extensionality, which states that

x:V y:V(x= Vy) z:V(zx)(zy)\prod_{x:V} \prod_{y:V} (x =_V y) \simeq \prod_{z:V} (z \in x) \simeq (z \in y)

However, the axiom of extensionality implies that VV is an h-sets, since the membership relation is an h-proposition, which in turn implies that each El(x)\mathrm{El}(x) is an h-set.

Examples include ZFC and its large cardinal, choice-less, constructive, predicative, and non-foundational/anti-foundational variants, such as ZF, Zermelo set theory, CZF, IZF, Mac Lane set theory?, Kripke–Platek set theory?, Tarski-Grothendieck set theory, New Foundations, Mostowski set theory, and so forth.

Well-pointed categories

Any well pointed category \mathcal{E} with hom-set type family hom(x,y)\mathrm{hom}(x, y) is a Tarski universe with universal type family

x:VEl(x)hom(1,y)x:V \vdash \mathrm{El}(x) \coloneqq \mathrm{hom}(1, y)

where 1:1:\mathcal{E} is the terminal object and indecomposable projective separator of the category \mathcal{E}.

Examples of this include ETCS.

Concrete categories

Every concrete category and every concrete dagger category? is a Tarski universe, as given a concrete category or concrete dagger category CC by definition for each object A:Ob(C)A:Ob(C) there is an h-set El(A)El(A). This includes models of Mike Shulman‘s SEAR, which is a concrete power allegory, as well as ETCS with elements, which is a concrete elementary topos.

Other examples

The empty type, unit type, boolean domain, and FinSet are all regular univalent Tarski universes. The types of propositions in a type theory are univalent Tarski universes: they model a dependent type theoretic model of propositional logic with function types, product types, disjunction higher inductive types, empty type, and unit type.

See also

For universes as a replacement for type judgments, see

Regarding the general notion of types of small types, see

Other mathematical structures and their univalent counterparts:

References

Historical review of Alfred Tarski‘s original notion in set theory:

The terminology “universe à la Tarski” — and now in the context of type universes for Martin-Löf dependent type theory — is due to:

Further discussion:

See also:

Last revised on July 26, 2024 at 21:44:01. See the history of this page for a list of all contributions to it.