Mathematical Object

Let $\mathcal{C}$ be a category.

Definition. A mathematical object is an object of $\mathcal{C}$. It is the primitive datum: the thing that morphisms go between, that products and coproducts are taken of, that functors act on.

What “object” means depends entirely on $\mathcal{C}$:

Proposition. An object $A$ in $\mathcal{C}$ is determined up to isomorphism by its hom-functor $\mathrm{Hom}_{\mathcal{C}}(-, A) : \mathcal{C}^{\mathrm{op}} \to \mathbf{Set}$ (Yoneda lemma). Two objects with naturally isomorphic hom-functors are isomorphic.

Proposition. Every mathematical object lives in at least one category. The mathematical-object frontmatter field on a term file names the category (or specific object within a category) that the term requires in order to be stated. If a file says mathematical-object: topological-space, it means: “to define this term, let $(X, \tau)$ be a topological space” — the ambient category is $\mathbf{Top}$ and the term operates on an object of $\mathbf{Top}$.

In set-theoretic foundations (ZFC), an object is a set. In type-theoretic foundations (HoTT), an object is a type. In categorical foundations, “object” is primitive — it is characterized entirely by the morphisms it participates in (Yoneda lemma).

Open questions

• Whether the system should track the ambient category explicitly (e.g. ambient-category: Top) separately from the specific object within it.