Synthetic differential geometry within homotopy type theory I

Abstract

This paper gives a first step towards developing synthetic differential geometry within homotopy type theory. Its model theory will be discussed in a subsequent paper.