Topos theory in HoTT

[Ali Caglayan]

How would we go ahead and formalise some Topos theory in HoTT? I know from the HoTT book, in chapter 10.1.4 elementary topoi are discussed. 

So far the only barrier to being able to define an elementary topos seems to be no definition of cartesian closed category (which should be easy to fix).

What I am hoping to achieve with this is being able to reason within the internal language of topoi in HoTT. This would allow us to define sheaves of rings as ring objects internal to Sh(X) on some locale X etc.

I am wondering what any developments on this are and who is thinking about it.

[Andrej Bauer]

The problem with having a topos of sheaves is that we're working in a
predicative setting so powersets are not easy to get. Have a look at
Michael Warrne's Master's thesis and subsequent work on the topic
(section "Mathematical logic and topos theory" at
http://mawarren.net), where he worked out how to do predicative
sheaves in type theory.

> --
> You received this message because you are subscribed to the Google Groups
> "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Ali Caglayan]

Hi Andrej,

Thanks for the reply, so from what I can gather using a 'predicative' kind of topos like a PiW-Topos is really the only way to get around the nature of elementary topoi. It seems to me that by jumping through a few extra hoops you can derive similar results.

I don't know a lot about Topos theory however I have been learning it recently. I like the fact that it allowed for short and sweet explanations of many things which got me thinking about it being useful for HoTT. However now that I am reading all this I am slightly upset by the fact that Topos theory isn't really well suited for predicative mathematics as you say. And I guess the best one can hope for is a similar notion of a topos which can have many of its useful properties.

But already I am thinking that it may not be possible to have an internal language of a topos like object unless it is purely a constructive type theory. But I guess that answers my question of why this hasn't been developed.

Perhaps I can study it some more in the summer and see if any of the nonsense I said is actually correct =).

Thank you for even reading this far,

Ali Caglayan

[Michael Shulman]

There is no problem at all in having an internal language for
predicative categories. Indeed, Martin-Lof Type Theory itself is an
internal language for locally cartesian closed categories that are not
necessarily toposes. Part D of Johnstone's "Sketches of an Elephant"
is a good summary of the internal logics of many different kinds of
categories, starting with categories that only have finite limits and
working all the way up to toposes.

I think Andrej's point was just specifically about sheaves, which have
special issues in defining them predicatively (but can certainly be
done).

On the other hand, one can also just add the propositional resizing
axiom to HoTT in order to get powersets and a topos.

>> > email to hott-cafe+...@googlegroups.com <javascript:>.

[Ali Caglayan]

Hi Mike,

Could you elaborate on how propositional resizing would give power objects? I am thinking about formalizing some basic Topos theory with the HoTT library. Until a clearer workaround is found I have no problem using prop-res for now.

And another thing, how would one go about writing in an internal logic in coq? I was hoping to kind of define a section where I specifiy that I am working in some internal type theory and then coq takes it from there. But maybe I am too hopeful?

Thanks,

Ali 

[Michael Shulman]

The power object of A is (A -> hProp).

It would be really nice if a proof assistant had the ability to step
into and out of internal languages, and automatically apply the
relevant interpretation. Unfortunately that's a ways in the future.
If it's enough for you to stay in the internal language, you can just
write in Coq and say to the reader "we are working in the internal
language". But if you want to prove something "external" about a
topos *using* its internal language, and have that external result
formalized, then you'd need to formalize the entire construction of
the internal language semantics, and the "internal language" that
you'll get won't be Coq itself but a type theory coded up *inside* Coq
as metatheory (hence it won't have conveniences like implicit
arguments, unification, and tactics, unless you implement *those*
yourself too0.

[Andrej Bauer]

On Sat, May 26, 2018 at 2:50 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> The power object of A is (A -> hProp).
>
> It would be really nice if a proof assistant had the ability to step
> into and out of internal languages, and automatically apply the
> relevant interpretation. Unfortunately that's a ways in the future.

Hopefully it's not that far in the future. I have a cunning plan. (And
since you're from USA, it's a reference to Boldrick.)

With kind regards,

Andrej

[Matt Oliveri]

Yes, perhaps, but I think I may have a more cunning one.

I'm interested to hear yours. Why don't you tell us about it in a new thread?

[Ali Caglayan]

Those nice features of Coq could be implemented in an 'inernal language' just by proving that the semantics of that language give rise to a type theory. Now being even more handwavy, if Coq can verify it's own kernal what is stopping it from comming up with an internal Coq (ad. infinum?).

It seems to me like stepping into an internal lanugage should be a very automatic process. Leaving the limitations of Coq, let's imagine a hypothetical proof assistant.

This proof asistant would only have as an input, inferance rules that you give it. From that it would be able to verify them. Now if you constructed some sort of category with an internal logic in this proof assitant, there could be a step where you tell it: Look here are your new inference rules (defined in terms of the categorical semantics) go process that internal language. This would all be verified because the proof assistant would have verified itself at some stage.

I imagine if we were to construct something like that it would have to be very simple like simply typed lambda calculus. I am not sure if simply type lambda calculus can eat itself however.

But these are the ideas that have been floating around in my head recently, hopefully someone can make light of it.

[Ali Caglayan]

After thinking a bit, I think we may be able to define a locally cartesian closed category in a locally cartesian closed category. We will only need typed lambda calculus with dependent products. We can define categories the same way we do in HoTT, infact these precategories won't have to worry about the identity type because there isn't one. I am not sure how much category theory can be done or if we really do need identity types here.

Continuing on, say somehow, we managed to define the notion of a monoidal category. We can then think about cartesian closed categories and then locally cartesian closed categories all internally. 

Now if our magic proof assistant can recognise such a structure, it should be able to go down into the internal language, as it was a proof assistant for LCCCs to begin with. I have no clue if you can even prove such a thing is valid.

[Ali Caglayan]

Actually I think we would need identity types, however I am pretty sure we can define inductive types with what we have an get them that way. But then we would need to define a Univalent category, which I am guessing would need some help from Univalence. Then this all boils down to Mikes idea of HoTT should eat itself.

hmmmmm

[Michael Shulman]

Right, this is exactly what I said would be really nice to have, but
doesn't yet exist.

On Sat, Aug 11, 2018 at 9:47 AM Ali Caglayan <ali...@gmail.com> wrote:
>
> Actually I think we would need identity types, however I am pretty sure we can define inductive types with what we have an get them that way. But then we would need to define a Univalent category, which I am guessing would need some help from Univalence. Then this all boils down to Mikes idea of HoTT should eat itself.
>
> hmmmmm
>