Comment by drnonsense42

Homotopy type theory probably. Uses in modern theorem prover languages include verification of systems/hardware and formalization of math.