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.

Two proofs of one proposition are not definitionally equal. Proof irrelevance, like propositional extensionality, function extensionality, excluded middle and choice, exists only as an axiom in rainbow.math.profile, and shows up in the axiom set of any theorem that uses it.

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

The kernel compares levels after normalize-level (source), which 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.

(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.

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. See Inductive types.