--- layout: post title: "Martin-Löf type theory as an internal language for categories" --- why care about undecidable extensional mltt? internal langauge of LCCCs, describe the theory and the construction in a palettable way. Does katex support tikz-cd?