# internal logic from higher categories

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 ?

• 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. – user40276 Sep 22 '16 at 1:10

In addition to the reference stated in the comment. nLab does provide an entry for internal logic from $(\infty,1)-$topos.