The Curry-Howard correspondence is only one of many lenses we can use to view the relationship between things and facts. Different lenses characterize different approaches to foundation: - Propositions are basic (single-sorted logics, ZF) - Types are basic, some types are propositions (Homotopy Type Theory) - Propositions and types are the same (Martin-Löf’s Type Theory) - Propositions and types are different but equally basic (Logic-enriched Type Theory) Shulman explains how the Axiom of Choice is true some but not in others, arguing that in certain respects, the HoTT’s way is the most “natural”: golem.ph.utexas.edu/category… Adams & Luo argue instead for the practical virtues of making propositions and types completely separate: arxiv.org/html/0809.2061v3