Universes

A type lives in a universe, [:sort level]. A level is [:zero], [:succ l], [:max l r], [:imax l r] (zero when r is zero, otherwise max) or a parameter [:param u] (level? in term.clj).

[:sort [:zero]] is Prop, and the elaborator reads 'Prop as exactly that. Data types such as data/Nat live in [:sort [:succ [:zero]]]. Modules usually name it once:

(def zero-level [:zero])
(def type-level [:succ zero-level])

Prop and imax

In the kernel’s infer* (source), [:sort l] has type [:sort [:succ l]], and [:pi A B mode] with A in [:sort l1] and B in [:sort l2] lives in [:sort [:imax l1 l2]]. So a function type whose body is a proposition is a proposition, whatever the domain. “Every proposition holds” quantifies over all of Prop and stays in Prop:

(kernel/infer (environment/empty-environment)
              [:pi [:sort [:zero]] [:bound 0] :explicit])
;=> {:status :checked,
;    :term [:pi [:sort [:zero]] [:bound 0] :explicit],
;    :type [:sort [:zero]]}

That term is the body of proposition/falsity. Truth, conjunction, disjunction and existence use the same encoding, and equality/Eq is Leibniz equality: x equals y when every predicate true of x is true of y (source). They are ordinary definitions.

The kernel has no proof-irrelevance rule: two proofs of one proposition are definitionally equal only if their normal forms match. Proof irrelevance, like propositional extensionality, function extensionality, excluded middle and choice, is declared as an axiom in rainbow.math.profile, and shows up in the axiom set of any theorem that uses it. It is also a theorem of propositional extensionality: logic/proof-irrelevance-from-proposition-extensionality has exactly the axiom’s statement, and its axiom set is exactly #{logic/proposition-extensionality} (CHANGELOG).

There is no cumulativity. A type in [:sort [:zero]] is not also in [:sort [:succ [:zero]]], so checking [:sort [:zero]] against [:sort [:succ [:succ [:zero]]]] fails with :kernel/type-mismatch.

Level normal forms

normalize-level (source) simplifies max and imax with zero, equal sides and successors, and sorts the sides of any other max, so [:max u v] and [:max v u] match. The calculus has the full rules.

The normal form is not complete, so the kernel compares levels by value: two levels are equal when they agree under every assignment (term/level-equivalent?, source). So max (succ u) u equals succ u, and the two groupings of a three-way max are equal, although their normal forms differ. Beyond 12 parameters under an imax’s second argument in one comparison, the kernel falls back to comparing normal forms (CHANGELOG).

(term/normalize-level [:imax [:succ [:zero]] [:zero]])      ;=> [:zero]
(term/normalize-level [:imax [:param 'u] [:succ [:zero]]])  ;=> [:max [:succ [:zero]] [:param u]]
(term/normalize-level [:imax [:param 'u] [:param 'v]])      ;=> [:imax [:param u] [:param v]]
(term/normalize-level [:max [:succ [:param 'u]] [:succ [:param 'v]]])
;=> [:succ [:max [:param u] [:param v]]]

The third stays an imax because v might be zero.

Polymorphic declarations

List the parameters in :universes and use them as [:param u]. Leibniz equality works at any level:

(def U [:param 'u])
(def sort-u [:sort U])

(def equality-definition
  {:name 'equality/Eq
   :kind :definition
   :universes ['u]
   :transparency :reducible
   :type (forall [['A sort-u] ['x 'A] ['y 'A]] 'Prop)
   :value (lam [['A sort-u] ['x 'A] ['y 'A]]
               (forall [['P (arrow 'A 'Prop)]
                        ['px (app 'P 'x)]]
                       (app 'P 'y)))})

A reference gives one level per parameter, in order. (const* 'equality/Eq [U]) uses equality at the caller’s u, and (const* 'equality/Eq [[:succ [:zero]]]) uses it for data types such as data/Nat. For equality between functions, rainbow.math.profile uses the level of a function type, an imax:

(proposition/equality [:imax u v] function-type 'left 'right)

:universes must be a vector of distinct symbols. A [:param u] that is not declared fails with :kernel/unbound-universe, and a [:const id levels] with the wrong number of levels fails with :kernel/universe-arity. Those are the categories kernel/infer reports. In a declaration added with add-declaration, the error is wrapped: the category becomes :kernel/invalid-declaration-type or :kernel/invalid-declaration-value, with the original under :cause.

Inductive types

A block declares its own universe parameters and level. data/List takes ['u] and lives in [:sort U]. data/Product takes ['u 'v] and lives in [:sort [:max U V]]. The recursor adds one parameter, _rainbow_motive_universe, for the type you eliminate into, so data/List.rec takes [U type-level] when you compute a natural number from a list. That use requires U to be at least 1, because a proposition with two or more constructors can only be eliminated into Prop. A constructor field may not live in a universe above the block’s level. See Inductive types.