Basic SIA / SDG in Agda
A basic implementation of synthetic differential geometry in Agda following roughly the developments in Kock's Synthetic Differential Geometry and Bell's A Primer of Smooth Infinitesimal Analysis.
This library is intended to eventually serve as a basis for a verified implementation in Agda of forward-mode automatic differentiation.
Not to be confused with sdg-agda.