Metric spaces and SDG

Abstract

We explore how the synthetic theory of metric spaces (Busemann) can coexist with synthetic differential geometry in the sense based on nilpotent elements in the number line.

Compared to Version 2 and 3, some redundancies are removed, and some arguments are corrected or completed