x
A Mathematics Without Undefined Operations: Constructive Operational Type Theory (COTT) — LessWrong