## ยง Emily Riehl Contrability as uniqueness

- untyped lambda calc/simply typed is topology of computation.
- dependent lambda calc/topos theoretic interpretation gives extensional mltt. Diagonal is identity type.
- challenge: intensional in topological setting. Path space is the identity type.