HoTT/book

Univalent cardinals

Opened this issue · 10 comments

In section 10.2, the type Card of cardinals is defined as the 0-truncation of Set, the type of sets in a universe U.

Why isn't Card simply U ?

With the univalence axiom, two types in bijection (equivalence) are equal. So any type is an equivalence class modulo bijections, ie any type is a cardinal. It seems univalence hardcodes the concept of cardinal (which is good !), so why speak of cardinals in HoTT ?

Maybe that explains why all definitions in section 10.2 seem void, all trivial "induction on truncation". The real proofs start at Theorem 10.2.10 (Schroeder–Bernstein), aren't they true for all types, not just sets ?

The short answer is, because there's a difference between a set and its cardinal number. Sets have automorphisms; cardinal numbers don't. (For instance, with the ZFC definition of "cardinal number", a cardinal number is a particular kind of well-ordered set, and well-ordered sets have no automorphisms.)

Of course one can define "cardinal" any way one wants, but I believe the 0-truncation definition makes them behave much more like most mathematicians expect cardinal numbers to behave. For instance, with this definition the type of finite cardinal numbers is isomorphic to the set of natural numbers, something I would certainly expect to be true; whereas the type of finite sets is not, being rather the disjoint union of the classifying spaces of the symmetric groups.

What do you call the type of finite sets ? Is it something like

Fixpoint Fin (n : nat) : Set :=
  match n with
  | O => Empty_set
  | S p => unit + Fin p
  end.

Definition isCardinal : Type -> nat -> Prop :=
  fun A n => exists (f : A -> Fin n) (g : Fin n -> A), type_equivalence A (Fin n) f g.

Definition isFinite (A : Type) : Prop :=
  exists n : nat, isCardinal A n.

Definition Finite_types : Type := sig isFinite.

Definition inc : nat -> Finite_types.
Proof.
  intro n. exists (Fin n). exists n. exists id. exists id. split; auto.
Defined.

If isFinite is not a mere proposition, function inc is probably not surjective. Is this the problem ? Maybe there is a better definition of finiteness that would solve it.

Anyway these examples and motivations are interesting, why not put them in the book ?

Regarding whether 0-truncation behaves like ZFC cardinals, it has the unfortunate consequence that Card becomes a set in HoTT. That is against the Burali-Forti paradox.

I think that's what I mean, as long as by "exists" you mean the propositionally truncated version. In that case isFinite is a mere proposition by definition, and in any case inc is always surjective; the point is that inc is not an equivalence.

I'm actually surprised to see that there is no motivation at the beginning of section 10.2 in the book. There should definitely be, thanks for bringing it up.

But I have no idea what you mean by your last paragraph. The word "set" in HoTT is used purely to refer to the homotopy dimension of a type, it has nothing to do with the set/class distinction in ZFC. The set Card is defined relative to a universe, and belongs to the next higher universe; no paradoxes are engendered.

As you said "the 0-truncation definition makes them behave much more like most mathematicians expect cardinal numbers to behave". When they are not trained in HoTT and its language, most mathematicians expect that Card is not a set, by the Burali-Forti paradox.

Chapter 10 does start by warning that HoTT sets are "quite different" from ZFC sets. But then why reuse the word "set", when you already had the very precise word "0-type" ?

The book talks a lot about the difference between ZFC sets and Lawvere's ETCS. ETCS would be "casual" sets used in informal proofs of ordinary mathematics, whereas ZFC would be a specific study of big infinities (which happens to also model all of ordinary mathematics on the way).

I understand HoTT is more inclined towards ETCS, but cardinals and ordinals are the playground of ZFC : the study of big infinities, like inaccessible cardinals. In those particular sections 10.2 and 10.3, I think special care is needed so that the reader doesn't compare too much with ZFC. Maybe by stating that the HoTT cardinals are rather small ones, not the big inaccessible cardinals of ZFC. Then it becomes natural that Card is a HoTT set.

Also, your position that a set is not its cardinal is inconsistent with the definition 10.3.17 of ordinals.

10.3.17 defines an ordinal as a well-order. But likewise, ZFC says that a well-order is not its ordinal : a well-order has an ordinal. It is even written in page 360 of the book :

In classical mathematics, the characterization of Theorem 10.4.3 is taken as the definition of a well-ordering, with the ordinals being a canonical set of representatives of isomorphism classes
for well-orderings. In our context, the structure identity principle means that there is no need to
look for such representatives: any well-ordering is as good as any other.

So I can rephrase my question : by univalence, there is no need to look for a canonical set of representatives of isomorphism classes for bijections : any type is a cardinal, and is as good as any other type in bijection with it.

Or if there is a need for such distinguished cardinals, this need should be explained in more details. Those details should also explain why cardinals and ordinals are treated differently in HoTT.

As you said "the 0-truncation definition makes them behave much more like most mathematicians expect cardinal numbers to behave". When they are not trained in HoTT and its language, most mathematicians expect that Card is not a set, by the Burali-Forti paradox.

You can think of the sets in HoTT as if you have chosen an increasing sequence of ω many inaccessible cardinals κᵢ. The sets in universe Uᵢ correspond to the sets of rank smaller than κᵢ. Therefore, the cardinals in universe Uᵢ, Cardᵢ, correspond to the the cardinals below κᵢ. Now Cardᵢ is a set in Uᵢ₊₁, but from the perspective of Uᵢ, Cardᵢ is not a set. You will be able to prove in HoTT that there is no set in Uᵢ which is in bijection with Cardᵢ.

This is the same in set theory: if we take the cumulative hierarchy at level κᵢ, this forms a model of set theory. In this model, the cardinals below κᵢ form a class, even though in the bigger model the cardinals below κᵢ form a set.

The "expectation" that's referred to is a structural expectation, not a size-related one. As Floris says, in type theory we use a sequence of universes rather than ever making a set/class distinction. The reason for using "set" instead of "0-type" is that these are the objects mathematicians use to build all their ordinary structures. It would be quite annoying if we would have to change "a group is a set equipped with a binary operation such that ..." to "a group is a 0-type equipped with a binary operation such that ... ".

The difference between cardinals and ordinals is that, as i've already said, well-orders are rigid, and thus (by univalence!) the type of well-orders is already a 0-type, whereas the type of sets is not a 0-type until you 0-truncated it. Cardinals should not be thought of as representatives of equivalence classes, but quotients of equivalence classes. Put another way, to say that a given set X "has cardinality 4" should not mean that we have fixed a particular bijection from X to {1,2,3,4}; it should be a mere property of X that such a bijection merely exists. This means that the operation "cardinality of" must map the 1-type Set of sets into a 0-type Card of cardinals.

I agree that all of this should be more clearly explained.

True, the isomorphism between a well-order and its ordinal is unique, whereas the bijection between a set and its cardinal is not. I guess that leads to different treatments in proof-relevant HoTT.

Please tell me when you have updated the book, I'll be interested in how the details go. It's hard to see exactly how proofs change when you switch from ZFC to HoTT.

I'm going to re-open this issue to remind us that when someone has time they should try adding some more explanation to section 10.2.

In set theory, cardinals are representatives of isomorphism classes of sets. The book tries to emulate this in the univalent foundations setting. But then the restriction to (univalent) sets does seem artificial, given the richer supply of types available in univalent mathematics. Also, some amount of arithmetic is available for types more general than sets (in particular, sum, product, exponentiation). To the extent that the notion of cardinality is useful for univalent mathematics, so should be the notion of h-cardinality, or univalent cardinality going beyond univalent sets.