Foundation-agnostic mathematics

Collection

Collection is an informal notion used in these notes for Foundation-agnostic mathematics, which may correspond to

• A class,
• A set of any size,
• A type of any h-level.

Notably, we do not require a collection to have any notion of equality on its elements.

#state/develop | #lang/en | #SemBr