David Corfield relation between category theory and type theory

• nLab

Correspondence

Locally discrete 2-bifibration over 2-category: unary modal type theory.

Locally discrete 2-bifibration over cartesian monoidal 2-category: simple modal type theory.

fibration of comprehension 2-categories: modal dependent type theory

Typos for Mike

p. 23 they implicit

p. 25 id_A: (A \vdash B)

p. 31: “cut admissibility is a special case of cut-elimination, and sometimes people prove cut-elimination directly without explicitly using cut-elimination as a lemma”

p. 130: forumlate