scratch
§
Emily Riehl Contrability as Uniqueness
created 2021-05-16
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.
❦