You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Uroš Nedić (May 25 2020 at 19:09):Does anyone know any good (informal) introductory material about Topoi? To understand motivation and broad view, at least.
John Baez (May 25 2020 at 20:10):I wrote this:
Uroš Nedić (Aug 27 2020 at 13:51):Thank you Dr Baez. I did read it long time ago but I did search for some real world examples how powerful this theory is as tool?
John Baez (Aug 27 2020 at 22:15):It depends on what you're trying to do. At this point I'd say topos theory is only worth learning if you want to understand mathematics and/or logic in a very deep way. For example if you're doing a lot of work with sheaves, or you want to understand how logic is connected to category theory, topos theory starts getting useful.
John Baez (Aug 27 2020 at 22:18):David Spivak did a project on air traffic control systems using topos theory, and it could be used in many other applications, but nobody has actually implemented Spivak's ideas yet... so I think that "real world" applications of topos theory have not been carried to fruition yet.
Matteo Capucci (he/him) (Aug 29 2020 at 16:25):Look for Tom Leinster's introduction, I found it very useful to start
Matteo Capucci (he/him) (Aug 29 2020 at 16:26):It's a brid-eye view of various themes in topos theory and their relationships, plus a minimal amount of definitions and motivation, of course
Uroš Nedić (Oct 05 2020 at 09:15):I did read material from Dr Spivak. However, I still do not understand what are advantages of doing logic in CT (via Topoi) and doing 'classical' logic (first/higher-order) with predicate calculus?
I am asking this from practical point of view as a software developer interested in verification techniques.
Chad Nester (Oct 05 2020 at 10:52):I don't think topoi are the answer to any question that would come up in the day-to-day activity of software verification. My understanding is that people are interested in topos theory because it gathers many disparate threads of mathematics in a strikingly natural way.
Chad Nester (Oct 05 2020 at 10:53):(I would be happy to learn otherwise!)
Matteo Capucci (he/him) (Oct 05 2020 at 11:54):Spivak and Schultz famously approached verification through topos theory, you can find talks, a book and a paper by googling 'temporal type theory' next to their name.
The idea is to use the internal logic of a topos of 'time-dependent things' to characterize their interactions and put constraints.
Indeed, the great leverage of the topos-theoretic method is that internal languages are basically the same for every topos, but their semantics can be wildly different. So you can actually write very simple software to deal with very complicated stuff.
Morgan Rogers (he/him) (Oct 05 2020 at 12:18):Matteo Capucci said:
Indeed, the great leverage of the topos-theoretic method is that internal languages are basically the same for every topos, but their semantics can be wildly different.
The most powerful category theoretic "an X is just a Y in the category of Z" results that I've personally seen have been of the form "X is just a Y object in the topos of Z", but I'm a topos theorist, so heavily biased :joy:
Matteo Capucci (he/him) (Oct 05 2020 at 13:17):I do not call myself a topos theorist but I definitely agree with you! :)
John Baez (Oct 05 2020 at 15:53):Spivak was using the internal language of a particular presheaf topos to conveniently express predicates involving time, for the design of an air traffic control system.
John Baez (Oct 05 2020 at 15:54):Oh, I'm repeating what Matteo said.
John Baez (Oct 05 2020 at 15:55):So yeah, the point of topos theory in Spivak's book on temporal type theory is that if you pick the right topos, instead of propositions being just true or not, they can be "true now", "true for the next 10 minutes", etc.
Spencer Breiner (Oct 05 2020 at 16:05):John Baez said:
Spivak was using the internal language of a particular presheaf topos ...
If I remember correctly, there is a sheaf condition involving coverage by end-to-end intervals.
Uroš Nedić (Oct 05 2020 at 17:22):I understood. It is better theory (Topos) for knowledge organisation and connection with other knowledge. If you develop something using Topoi you can have a better overview of your theory itself and maybe find connections with other theories or use something already discovered.
sarahzrf (Oct 06 2020 at 00:57):here's a paper i like a lot which applies topos theory to the semantics of programming languages https://arxiv.org/abs/1208.3596
sarahzrf (Oct 06 2020 at 00:58):the concepts involved in it are closely linked to the stuff in Iris, which is definitely applicable to actual program verification
Henry Story (Oct 06 2020 at 07:27):John Baez said:
So yeah, the point of topos theory in Spivak's book on temporal type theory is that if you pick the right topos, instead of propositions being just true or not, they can be "true now", "true for the next 10 minutes", etc.
That is a very helpful summary, thanks.
I had a look at it a few months ago, but could now work out what "Temporal Type Theory" was
My first thought was that this must be a modal logic, but when I asked @David Spivak he did not seem to make the connection. @David Corfield in "Modal HoTT" mentions "Temporal Type Theory" in one sentence, but as work to be done relating it to the Modal HoTT project.
Henry Story (Oct 06 2020 at 08:20):With regard to the question of the practical uses of Topos theory by Uroš Nedić said:
I am asking this from practical point of view as a software developer interested in verification techniques.
in his book D. Corfield writes
where HoTT is the internal language of -toposes, _modal_ HoTT is the internal language for collections of -toposes related by geometric morphisms
The part to highlight here is that "HoTT is the internal language of -toposes". That is, as I understand, it defined the categorical structure and vice versa.
Cubical HoTT is a version of HoTT that can be implemented in computers, and there are a number of implementations of cubical HoTT's now, of which Cubical Agda. I think of that as the next step for proof assistants, the step after that being the Modal HoTT ones (allowing one to define graded modalities, linear logic ones, bunched logics, etc, in the language itself -- all of these highly useful in programming).
So what use is Cubical HoTT? Well most of the proof assistants are built on Martin-Löf type theory, and HoTT is an extension of that. The article Cubical Agda: a dependently typed programming language... gives a very interesting example, of how it allows one to take proofs from one domain of mathematics, eg the version of numbers and transport it without loss of mathematical rigor to another implementation that may be better suited for computing (e.g. a binary one). I guess this should lead to these languages creating both efficient and secure programs. One could prove properties of structures using representations where it is easier to prove them, and just write out the mapping to the structure most effective for the computer to which it needs to be compiled.
(note I am a programmer studying this, not a mathematician, so these are my intuitions).
David Corfield (Oct 06 2020 at 08:58):I think I'm saying a little more than that. We've had temporal logic around for decades as a kind of modal logic (https://plato.stanford.edu/entries/logic-temporal/). It's a fairly obvious move then to think about temporal versions of other logics, such as kinds of type theory: simple type theory, dependent type theory, even HoTT. I say 'obvious' but there's little that's been published on this, so in my chapter I'm just probing some possibilities.
See Schultz and Spivak "This book introduces a temporal type theory, the first of its kind as far as we know", "we also make very limited use of dependent types". Huge amounts remain to be done. People should see this as an opportunity, an unmined gold field. Think what might happen as the intricate identity structure of HoTT meets with modal temporal operators.
Lê Thành Dũng (Tito) Nguyễn (Oct 06 2020 at 10:05):sarahzrf said:
here's a paper i like a lot which applies topos theory to the semantics of programming languages https://arxiv.org/abs/1208.3596
Concerning toposes and programming there is also the recent
http://www.jonmsterling.com/pdfs/lrat.pdf
which I haven't actually read but I mention it because I just love how Figure 6 page 26 looks :stuck_out_tongue_closed_eyes:
Uroš Nedić (Oct 07 2020 at 20:18):Leslie Lamport discovered Temporal logic of actions (TLA) by combining Temporal Logic and Logic of Actions (https://lamport.azurewebsites.net/tla/tla.html). Is it possible for TLA to be transformed (connected) to Temporal Type Theory?
Spencer Breiner (Oct 07 2020 at 20:53):There is a group at Sandia working on a CT view of TLA. Jon Aytac gave a talk about this at ACT2019: http://eptcs.web.cse.unsw.edu.au/paper.cgi?ACT2019.11
Spencer Breiner (Oct 07 2020 at 20:57):No relation to Temporal Type Theory (yet), as far as I'm aware. At a glance, TLA seems to be principally discrete-time, whereas TTT aims to handle (and mix) discrete- and continuous-time behaviors.
Uroš Nedić (Oct 08 2020 at 22:57):Thank you for all these helpful comments. I did also look Effectus Theory (https://arxiv.org/abs/1512.05813). Is it possible to lift this into Topos and to establish relations with other theories?
John van de Wetering (Oct 08 2020 at 23:01):Hi Uros. Every topos is an effectus in a quite uninteresting way (in the paper you linked, they are related to "Boolean effectuses")
John van de Wetering (Oct 08 2020 at 23:01):A better version of that paper is Kenta Cho's PhD thesis, if you really want to get into it: https://arxiv.org/abs/1910.12198
Uroš Nedić (Oct 23 2020 at 23:30):Spencer Breiner said:
No relation to Temporal Type Theory (yet), as far as I'm aware. At a glance, TLA seems to be principally discrete-time, whereas TTT aims to handle (and mix) discrete- and continuous-time behaviors.
Is it possible for Discrete Temporal Type Theory (http://www.brendanfong.com/Spivak_TTT_Outline.pdf) to compare with TLA+?
Spencer Breiner (Oct 26 2020 at 15:50):tl;dr: TLA can probably be embedded into TTT, but working through the details would be a research project.
[Quoting…]
That work gives a start, but it's not enough. You would need to do some work to establish the appropriate relationships between TLA and the type theory. How much have you looked at TTT?
The basic entities in TTT are sets of behaviors, indexed by durations, with a gluing condition that says we can match behaviors as interval enpoints (a sheaf over the "interval site"). One thing you might want to do is interpret TLA(+) in TTT, by showing that any TLA specification defines a specific sheaf in TTT. Presumably this mapping would be functorial (for an appropriate notion of TLA arrow?). Writing S for a TLA spec and [S] for the associated sheaf, you would hope that it preserves some other structure as well, like the interpretation of the logic (e.g., [S & T]=[S]x[T]) and, more interestingly, the temporal structure.
So the first two questions you would need to answer are (i) what set of behaviors correspond to a TLA statement and (ii) how do TLA connectives/quantifies/modalities/etc transform into sheaf-theoretic constructions. From my admittedly limited knowledge of TLA, the main stumbling block is probably as follows.
I think that the inclusion of discrete behaviors into continuous behaviors in (TTT) is both fixed and regular, but in TLA (I think) neither is true. We can interpret the discrete embedding in a situational way (e.g., stuttering equivalence). That means you probably need to think about multiple discrete embeddings and their relationships (e.g., refinement).
If I had to guess, the sheaf of behaviors you get out will be something like this: start from a relatively small set of nominal behaviors in discrete time, embed them into the continuous setting, and then close them under monotone transformations of the duration intervals.
Spencer Breiner (Oct 26 2020 at 15:52):I should emphasize, again, that I'm basing this off a vague remembrance of a talk a couple of years ago. If you want to pursue this topic seriously, you should talk to @Jon Aytac and collaborators.