nLab has an article on internal logic. Homotopy type theory also discusses its application in logic. Any one knows references to the correspondence study of the internal logic induced from higher category theories and higher topo theories ?
1
-
$\begingroup$ This adjunction between internal logic and the syntactic category was stablished only for presentable locally cartesian closed quasicategories. Take a look at arxiv.org/abs/1507.02648 and the references in the introduction. It's expected to hold without the presentability hypothesis, by the way. $\endgroup$– user40276Sep 22, 2016 at 1:10
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
In addition to the reference stated in the comment. nLab does provide an entry for internal logic from $(\infty,1)-$topos.