What set-theoretic definitions can't easily be formalized in a type theory?

Question

Most proof assistants (with some exceptions like Isabelle/ZF or the B method) rely on type theory.

See also the MathOverflow question What makes dependent type theory more suitable than set theory for proof assistants?

Next, formalizing mathematics is one of the main use cases of an interactive proof assistant.
But many pen-and-paper mathematical proofs are written in a set-theoretic fashion (e.g., in ZFC).

Finally, there are many different type theories (first-order, higher-order, dependently-typed or not, intuitionistic or not, etc.)

So, formalizing existing set-theoretic results typically involves some formal hindrances.

Keeping the constructiveness issue apart, and focusing on the definability of mathematical objects:

1. what mathematical concepts can't typically be "formalized as is", within the main proof-assistants / type-theories?
   (e.g., we can think about matrices in a non-dependently-typed theory…)
2. is a "workaround" possible, to still be able to formally deal with this mathematical concept in the considered theory? (if yes, feel free to cite a formalization example)

Answer 1

Almost no pen-and-paper mathematics is written in ZFC. The vast majority of mathematical texts is actually written in something that resembles structural set theory and is closer to type theory than to ZFC.

Most mathematics can be formulated in type theory in a fairly straightforward manner. However, not every brand of type theory is equally good for formalization of mathematics. Some type theories are more like programming languages, and others are geared towards formalization of mathematics.

Here are some features that make it easier to formalize mathematics in type theory:

1. Quotients: it is annoying to not be able to form quotients by equivalence relations. In type theories without quotients people use setoids (types equipped with equivalence relations) – and those who worked with setoids sometimes refer to the activity as "setoid hell".

2. Impredicativity: often a type theory does not have a type of truth values, but instead has a whole hierarchy of them (one in each universe). This leads to various complications because one has to keep track of universes.

3. Extensional equality: In type theory equality is represented by identity types. These may behave in unusual ways, unless we adopt some principles (such as Uniqueness of identity proofs or equality reflection).

4. Function extensionality: this principle states that $f, g : A \to B$ are equal if $f(x) = g(x)$ for all $x : A$. It seems quite hard to do mathematics without this principle.

5. Other extensionality principles: these are principles like "equivalent propositions are equal" and "pairs are equal if their first and second components are equal".

6. Excluded middle and the axiom of choice are needed to a much lesser degree than one might expect.

Some type theories have all of the above constructions and principles, for instance the type theory of Lean. By doing so they sacrifice some good computational properties that "pure" type theories have (by this I mean that the type theory can be used a programming language as well as a foundation of mathematics). And there are alternatives which keep the good computational properties but require one to rethink how mathematics is done (such as cubical type theories).

Answer 2

Andrej's answer that "Almost no pen-and-paper mathematics is written in ZFC" is correct. But it's perhaps also worth noting that some pen-and-paper mathematics is written in ZFC (or, at least, something closer to ZFC than to type theory), such as much of the mathematics done by set theorists (in which phrase, of course, "set" refers traditionally to a ZFC-set).

A good deal of set theory can be rephrased more structurally to make sense in type theory, but this would be a rephrasing, and the amount of work that would be required is, I think, variable. For instance, set theorists work with ordinals defined in the von Neumann way, with $\in$ as the well-founded relation. This in particular implies that ordinals are literally unique representatives of isomorphism classes of well-ordered sets. In type theory it is more natural to work "structurally" with arbitrary well-ordered sets rather than with von Neumann ordinals. This makes some things more cumbersome because of isomorphisms that get carried around (although under univalence, these isomorphisms become equalities), but probably doesn't change things a whole lot.

On the other hand, as far as I know, no one has ever come up with a convincing structural presentation of Godel's constructible universe $L$. The only structural approaches to $L$ that I know of essentially involve building a model of ZF(C) in some way and then constructing $L$ inside that model. Note that $L$ is, as far as I know, still the only way to prove the relative consistency of the Axiom of Choice, so it is of interest even to mathematicians who don't care about ZF for its own sake. (In contrast, the symmetric/permutation methods used to prove relative consistency of not-AC, and the forcing methods that can be used to prove consistency of other properties such as GCH and not-GCH, seem much more amenable to structuralization.) [Note: this paragraph was edited to remove a false claim that GCH is not forceable; see comments.]

As another example, Scott's trick is a method used in pen-and-paper mathematics that is of interest beyond set theory, but relies on the axiom of foundation from ZFC, and so is not obviously formalizable in type theory.