[j2kun]

A quibble of my own: a lot of the "infinity" constructions in mathematics only use infinity as a name. Projective geometry (1) is a good example of that. The formalization doesn't actually appeal to any sort of infinite quantities.

[chalst]

Projective geometry: even in the simple case I outlined, you have lines being circles of infinite diameter. That infinity is just an additional closure point on the plane for shapes (and you can think of the similar projective line providing the complementary notion of displacement we can use to measure the diameter of infinite circles) doesn't stop the geometry from representing shapes with infinite attributes.

It is the case that all of this can be finitely represented. But this is true of a quite large part of large cardinal set theory as well, which can be represented in constructive type theory - mathematicians make it their business to transform the infinitary into the finitary.