Discrete differential geometry in homotopy type theory

Greg Langmead

Type families on higher inductive types such as pushouts can capture homotopical properties of differential geometric constructions including connections, curvature, and vector fie…