@misc{oai:tsukuba.repo.nii.ac.jp:00038353, author = {西村, 泰一 and NISHIMURA, Hirokazu}, month = {Oct}, note = {Both syntheticc differential geometry and homotopy type theory pre- fer synthetic arguments to analytical ones. This paper gives a first step towards developing synthetic differential geometry within homotopy type theory. Model theory of this approach will be discussed in a subsequent paper.}, title = {Synthetic differential geometry within homotopy type theory I}, year = {2016}, yomi = {ニシムラ, ヒロカズ} }