Cool! (Nitpick: You should probably mention that you are deviating from the naming in the HoTT book. AFAIK usually Π and Σ types are called Pi and Sigma types respectively, while the words “product” and “sum” (or “coproduct” in the HoTT book) are reserved for A×B and A+B.)
I am especially looking forward to discussion on how MLTT relates to alignment research and how it can be used for informal reasoning as Alignment Research Field Guide mentions.
Cool! (Nitpick: You should probably mention that you are deviating from the naming in the HoTT book. AFAIK usually Π and Σ types are called Pi and Sigma types respectively, while the words “product” and “sum” (or “coproduct” in the HoTT book) are reserved for A×B and A+B.)
I am especially looking forward to discussion on how MLTT relates to alignment research and how it can be used for informal reasoning as Alignment Research Field Guide mentions.
I always get confused when the term “type signature” is used in text unrelated to type theory. Like what do people mean when they say things like “What’s the type signature of an agent?” or “the type of agency is (A→B)→A”?