§ 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.