We define cardinal numbers as a quotient of types under the equivalence relation of equinumerity. We define the order on cardinal numbers, define omega, and do basic cardinal arithmetic: addition, multiplication, power, cardinal successor, minimum, supremum, infinitary sums and products
cardinal number, cardinal arithmetic, cardinal exponentiation, omega
The equivalence relation on types given by equivalence (bijective correspondence) of types. Quotienting by this equivalence relation gives the cardinal numbers.
cardinal.{u} is the type of cardinal numbers in Type u, defined as the quotient of Type u by existence of an equivalence (a bijection with explicit inverse).
The cardinal number of a type
We define the order on cardinal numbers by mk α ≤ mk β if and only if there exists an embedding (injective function) from α to β.
The cardinal exponential. mk α ^ mk β is the cardinal of β → α.
The minimum cardinal in a family of cardinals (the existence of which is provided by injective_min).
The successor cardinal - the smallest cardinal greater than c. This is not the same as c + 1 except in the case of finite c.
The indexed sum of cardinals is the cardinality of the indexed disjoint union, i.e. sigma type.
The indexed supremum of cardinals is the smallest cardinal above everything in the family.
The indexed product of cardinals is the cardinality of the Pi type (dependent product).
The universe lift operation on cardinals. You can specify the universes explicitly with lift.{u v} : cardinal.{u} → cardinal.{max u v}
ω is the smallest infinite cardinal, also known as ℵ₀.
König's theorem
The function α^{<β}, defined to be sup_{γ < β} α^γ. We index over {s : set β.out // mk s < β } instead of {γ // γ < β}, because the latter lives in a higher universe