Universes

A universe is a type of types. Since the type of all types cannot be consistently introduced into a type theory with dependent Pi types, as the type of types cannot contain itself, Arend contains a hierarchy of universes \Type n (the whitespace is optional), parameterized by a natural number n. This number is called the predicative level of the universe. Informally, the universe \Type0 contains all types that do not refer to universes in their definition, the universe \Type1 contains all types in \Type0 together with those types that refer to \Type0 and no other universes in their definitions, and so on. This is not precise, since, for instance, the universe \Type n also contains some data types, classes and records that refer to \Type m, where n ≤ m, in types of parameters. See section on universe placement rules below for more precise statements and details.

Note that the hierarchy of universes in Arend is cumulative, that is every expression of type \Type n has also type \Type (n+1).

Writing \Type without a level denotes the universe with the largest, infinite, predicative level. It is convenient for parameters whose predicative level does not matter. Note, however, that the infinite \Type is not itself a small type, so it is not a member of any \Type n (in particular, not of itself). This is what rules out contradictory circular definitions; for the same reason a definition such as \func bad : \Type => \Type is not allowed.

Homotopy levels

Types are further stratified into universes \n-Type p according to their homotopy level n, which is an integer number (or infinity ∞) in the range: -1 ≤ n ≤ ∞. Some of these universes have alternative names: the universe of propositions ((-1)-types) \Prop and universes of sets (0-types) \Set p (coincides with \0-Type p). The untruncated universe (homotopy level ∞) is simply \Type p.

Unlike the predicative level, the homotopy level is not an argument of \Type: the universe \Type always denotes the untruncated universe, and each truncated universe is written with its own keyword \n-Type, which is in turn parameterized by a predicative level. There is no \oo-Type, and it is not possible to write two levels after \Type.

Every truncated universe must be given a (finite) predicative level. Writing \Set or \66-Type with the level omitted is an error (“Infinite level is not allowed here”). Supply a concrete level, as in \Set 0, or a level parameter (see Level polymorphism). Only \Type may be used without a level.

Note that the universe \Prop is impredicative: it does not have a predicative level. Practically, this means that if B : \Prop, then the type \Pi (x : A) -> B is in \Prop for any A.

The universe \Prop is not proof irrelevant, but some elements of propositions are computationally equal. If A : \Prop and a, a' : A are such that they never evaluate to a constructor, then they are computationally equal. For example, if the type is an empty data type, then this is true for any pair of its elements, so they will always be computationally equal.

Universe placement rules

Types in Arend are distributed over the universes according to the following rules. Below we write \h-Type p for the universe of homotopy level h and predicative level p, where h = ∞ corresponds to the untruncated universe \Type p and h = -1 to \Prop.

  • If A : \h_1-Type p_1 and B : \h_2-Type p_2, then \Sigma A B : \max(h_1,h_2)-Type max(p_1,p_2).
  • If A : \h_1-Type p_1 and B : \h_2-Type p_2, then \Pi (x:A) -> B : \h_2-Type max(p_1,p_2). Note that if B : \Prop, then (\Pi (x : A) -> B) : \Prop for any A.
  • If 0 ≤ h < ∞, then \h-Type p : \(h+1)-Type (p+1).
  • \Prop : \Set 0, which is the same as \Prop : \0-Type 0.
  • \Type p : \Type (p+1) (the untruncated universe stays untruncated).
  • If A : I -> \h-Type p, then Path A a a' : \max(-1,h-1)-Type p. In particular, if A : \Set p, then a = a' : \Prop.
  • If D is a data type and A_1 : \h_1-Type p_1, ..., A_k : \h_k-Type p_k are types of parameters of constructors of D, then predicative level of D is the maximum over 0, p_1, ..., p_k. If D has conditions, equalising a constructor on two ends of the interval type, then homotopy level of D is ∞. Otherwise, if D has more than one constructor, then its homotopy level is the maximum over 0, h_1, ..., h_k, and if D has at most one constructor, then its homotopy level is the maximum over -1, h_1, ..., h_k.
  • If C is a class or record and A_1 : \h_1-Type p_1, ..., A_k : \h_k-Type p_k are types of parameters of unimplemented fields of C (including fields of superclasses), then its predicative level is the maximum over 0, p_1, ..., p_k and its homotopy level is the maximum over -1, h_1, ..., h_k.

Level polymorphism

A definition can be made polymorphic in the predicative level by declaring one or more level parameters right after its name, using the syntax .{...}, and referring to them in universes such as \Type l:

\func id.{l} (A : \Type l) (a : A) => a

There is no implicit level parameter: a definition that mentions only the bare (infinite) \Type is not level-polymorphic. Homotopy levels are not a polymorphic axis; only predicative levels can be abstracted this way.

Level arguments can be specified explicitly in a defcall with the same .{...} syntax; the arguments are level expressions:

\func test1 => id.{0} Nat 0
\func test2.{l} => id.{\suc l} (\Type l) Nat

Level expressions are defined inductively:

  • A level parameter (such as l above) is a level expression.
  • A constant (that is, a natural number) is a level expression.
  • _ is a level expression. Such an expression suggests the typechecker to infer the expression.
  • If l is a level expression, then \suc l is also a level expression.
  • If l1 and l2 are level expressions, then \max l1 l2 is also a level expression.

Multiple level parameters

A definition may declare several predicative level parameters, separated by commas; they are independent level variables:

\func pair.{l1, l2} (A : \Type l1) (B : \Type l2) => \Sigma A B

Level arguments for such a definition are given in the same order, again with .{...}:

\func example => pair.{0, 1} Nat \Type0

If level parameters are not explicitly declared for a definition, they will be inherited from definitions that appear in parameters if all of them have the same levels.

Level inference

The level arguments of a function in a defcall can often be inferred automatically, so .{...} rarely needs to be written explicitly. For example, id Nat 0 elaborates to id.{0} Nat 0.

The levels of a universe in the signature of a function can also be omitted, in which case they will be inferred by the typechecker. Note, however, that a bare \Type denotes the infinite universe rather than a level to be inferred; and \Set/\n-Type require a finite predicative level, so an unconstrained level there is an error rather than being defaulted silently.

The levels in the parameters and in the result type of a recursive function are inferred before the levels in the body.

A definition is marked as universe-like if it contains universes or universe-like definitions applied to one of its level parameters. If D is a universe-like definition, then D.{p} is equivalent to D.{p'} only if p = p'. If D is not universe-like, then these expressions are always equivalent.