categorical logic

• internal language
• the problem is not to find an internal language, it is to find a sharp one
• probabilistic Curry-Howard correspondence

Literature.

• Categorical Logic (Shulman, 2016)

Back: category theory, Type theory.