I've read as much as I can understand about type theory and homotopy type theory (HoTT) and it seems like these are very promising directions for re-foundationalizing mathematics in a way where complicated math proofs can be programmed and verified mechanistically. Unfortunately, but not surprisingly, all of this activity going on with type theory/HoTT is at a graduate-level and above.
Would it be useful as an exercise to try to formalize my understanding of relatively elementary subjects such as calculus, linear algebra, geometry, etc in a proof assistant such as Agda and just ignore the more advanced aspects of HoTT? Or is HoTT only useful for super advanced math