[bitdiddle]

Your comments in this thread have really piqued my interest enough to read some of this HoTT. I'd heard of this a couple of years back and didn't have the energy for it at the time.

Some years ago I spent a serious amount of time reading topos theory, particularly local set theory, as given by the Mitchell-Benabou internal language of any topos, looking for a better approach to description logics.

I do believe topos theory provides a better foundations than set theory because the logic is inherently intuitionistic. I found it also provided a simpler explanation of independence results. However one of the things I believe is true of the proof theory is that there is no cut-elimination theorem, which is important to establish a sub-formula property.

Sorry to ramble here, let me ask specifically, are there connections between HoTT and topos theory? Or geometric logic? Your earlier comment on the synthetic nature made me think there might be.

Thank you

Edit: I more or less answered my own question by reading the introduction, the section on open problems, the possible connections are between HoTT and the higher toposes. Judging from the intro, this seems very readable.