A Note on Formalizing Undefined Terms in Real Analysis

To adopt proof assistants based on logic of total functions in education, one major problem is that of representing partial functions. In particular, one wishes to capture undefinedness in a rigorous way, while staying as close as possible to traditional mathematical practice. In this paper, we propose to represent potentially undefined terms with partial setoids on lifted terms, and to understand book equalities occurring in equality chains as special directed relations that hold only under assumptions of definedness for some terms. We also employ a suitable notion of strict morphism to fully automate propagation of these directed relations in strict contexts.