Comment by zmgsabst

I think the intuition behind HoTT is truly fascinating:

The topology of (category) diagrams can represent a type theory’s semantics — and equivalence in your theory is a question about paths in diagrams.

An application of the idea that topology connects “algebra” (type theory) to “geometry” (diagrams composed of cells).