Como estudiante de matemáticas, se suele enseñar con la teoría de conjuntos básica la noción de producto directo $A \times B$ y la unión disjunta $A \sqcup B$ . Pero por muy común que sea, nunca me he encontrado con la "Opción(A)" (Tiene muchos nombres) con $Opt(A) = A \sqcup \{\blacksquare\}$ donde $\blacksquare$ es disjunta de $A$ y se considera tal vez como "No A" o "Ninguno".
Por ejemplo, un matemático o ingeniero de software descuidado puede imaginar una función $FirstElement : FiniteSeqOf(A) \rightarrow A$ sin tener en cuenta cómo se definiría $FirstElement$ en la lista de longitud $0$ . Pero envolver el dominio con $Opt$ salva el día: $FirstElement: FiniteSeqOf(A) \rightarrow Opt(A)$ con $FirstElement([]) = \blacksquare$ .
La construcción $Opt(A)$ es un functor, por supuesto. También puede verse como la asociación de un conjunto $A$ con subconjuntos / secuencias finitas de $A$ si el tamaño $0$ o $1$ .
Estrechamente relacionados: funciones parciales, categorías de conjuntos puntuales.
Dada la simplicidad de este constructo en comparación con otros comúnmente vistos, ¿dónde aparece esto, explícitamente, en las matemáticas de pregrado?