How do I call cardinality in type theory?

Question

In set theory, we say "cardinality" when we mean "how many members are there in a set". Is there a corresponding notion in type theory? (Any thereof)

For example, I have the idea that the functions of type $X \to Y$ are $Y^X$ in number. But I cannot explain how I arrived to this thought.

Answer 1

Not in general, no. Types are not "collections of things". The closest you can get to this with a fair amount of generality is to look at the number of closed (normal form) terms of the given type. This more or less corresponds to looking at the number of global elements categorically speaking. The problem is the closed terms/global elements rarely tell you everything about a type in most type theories. The interesting thing about (usual) set theories is that the global elements tell you everything there is to know about a set. Returning to type theory, we can have, for example, a type that has no closed terms/global elements, and yet is still distinct from the empty type.

As a concrete example of this phenomenon in a relatively well-known type theory we have the circle type, $\mathbb S^1$, in Homotopy Type Theory (HoTT). This type has only one closed term, and yet it is quite distinct from the unit type. A function $f:\mathbb S^1\to X$ not only has to map the global element from $\mathbb S^1$ to $X$, but it also needs to map the path in $\mathbb S^1$ to a path in $X$. Two functions $\mathbb S^1\to X$ can differ on how they map the path even if they agree on how they map the global element. The intuition from classical homotopy theory is that $f$ is continuous and defined for all the "points" of the circle $\mathbb S^1$ even though we can only name one of those "points".

In many richer type theories, e.g. descendants of Martin-Löf type theory (MLTT), you can define (or have axiomatically) finite types. For example, in Agda, a variation on MLTT, you can define:

data ℕ : Set where -- Don't let the word "Set" mislead you. "Type" would be a better name.
    Z : ℕ
    S : ℕ → ℕ

data Fin : ℕ → Set where
    FZ : {n : ℕ} → Fin (S n)
    FS : {n : ℕ} → Fin n → Fin (S n)

Fin n where n : ℕ is now a type that has n closed, normal form terms, which will look like FZ, FS FZ, FS (FS FZ), etc. You could then attempt to prove (Fin n -> Fin m) ≅ Fin (m^n) where m^n is an implementation of exponentiation of natural numbers (You may need to assume function extensionality. I haven't tried it.) By ≅ I mean an explicit isomorphism, i.e. a pair of functions going opposite directions and a pair of proofs show that they are mutually inverse.

For an analogue to the general theory of (infinite) cardinals and ordinals, it takes a fairly rich type theory just to formulate the problem. My understanding is that, for at least typical constructive type theories, there isn't really a meaningful/useful notion of "cardinal".