Category Theory
Zulip Server
Archive

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.

Stream: community: our work

Topic: Ivan Di Liberti

Ivan Di Liberti (Dec 13 2021 at 11:35):

Greta Coraglia and I recently landed on the ArXiv with Context, Judgement, Deduction.

I will be giving a talk at the Leeds-Ghent Virtual Logic Seminar this Wednesday, 15 December at 3pm UK time. Those that would like to attend, can click on the link below.

Meeting Link:
https://universityofleeds.zoom.us/j/97238759794?pwd=M2FWUXVXckVhcHBpMjZlbmdRZks3UT09

Meeting ID: 972 3875 9794
Password: 219588

The talk will be more tailored for philosophers of logic and proof theorists, but of course the whole paper is phrased in the language of categories. If you are interested in the topic, but you happen to miss the talk, you will have a second chance at ItaCa21, where Greta will present the same material from a more category theoretic and type theoretic point of view.

I should probably say what's the paper about.
We introduce the notion of Judgemental Theory and its calculus. A judgemental theory is a mathematical gadget inspired by Awodey's natural models that allows for a very flexible presentation of several logical frameworks, including of course dependent type theory, but also natural deduction, the internal logic of a 1 and 2 topos, and several other interesting fragments of logic. At the current state, we do not have an example of something that cannot be presented by a judgemental theory.
JTs focus on the notion of rule, and provide a very algebraic approach to manipulation of (nested) judgements, so that we can provide a very compact and neat definition of type constructor. Notice that while some type constructors are of course studied by several authors, this is the first time that a categorical definition of type constructor appears in the literature, and indeed there are reasons for which this is true.
More significantly JTs are a candidate categorical syntax for dependent type theory, more than a categorical semantics, offering a clear way to transform categorical properties of the judgemental theory into its a formal calculus.

It's hard to convey everything that we do in a message without essentially re-writing the paper, but you can read page 3 and 4 of the introduction to get a general sense of our results, or you can just trust me and come to the talks!

José Siqueira (Dec 13 2021 at 12:18):

@Ivan Di Liberti the link to the paper leads to a blog post on benzene by John Baez, which I'm guessing wasn't the plan!

Spencer Breiner (Dec 13 2021 at 14:20):

Link: https://arxiv.org/abs/2111.09438

Ulrik Buchholtz (Dec 14 2021 at 14:55):

Looks interesting, and I'm looking forward to the talk!

I'm a bit confused about how the definition (Def. 1.0.1) should be read: There's a weak and a strict reading, if I'm not mistaken. On the strict reading, we think of $\mathsf{ctx}$ and each $\mathbb{F}$ and $\mathbb{G}$ as strict categories (with sets of objects), and then we can regard $\mathcal{J}$, $\mathcal{R}$ and $\mathcal{C}$ as subsets of the corresponding (large) sets. Alternatively, we think of (univalent) categories (if you excuse the HoTTism: this just means we're working up to equivalence of categories). Then we should think of $\mathcal{J}$, $\mathcal{R}$ and $\mathcal{C}$ as sets indexing various structures. But then we need to add mediating equivalences for the cuts, e.g., for the left-most, an equivalence between the codomain of $\lambda$ and the domain of $\tau$.

Is there a difference between “composed judgments” and “nested judgments” in the paper?

I'm also curious how you'd capture modal logics (and modal type theories) in this framework, as you indicate on p. 3 should be possible. I don't quite see it, so I'd appreciate a hint.

BTW, I noticed some typos when skimming through:

• p. 11 “(pre)judjemental”
• p. 13 “Let $\mathbb{C}$ a category” and “between the corresponding fibration,” and “not the vice versa” (“not vice versa” or “not the other way round”)
• p. 18 “far to be” (“far from”)
• p. 40 “subojbect”

Ivan Di Liberti (Dec 30 2021 at 17:27):

I am incredibly late, sorry Ulrik. Life has been intense as I am moving recently, and of course there was panettone-time in the meanwhile. Let me try and address your comments.

I think there is no reason to be confused, the definition clearly talks about categories, in a very neat sense of the word, there is no ambiguity. Our notion generalises Natural Models, so there is nothing you can do with NM that you can't do with our notion.

Of course, as you say, a weaker interpretation is available, and indeed essentially everything would carry to such a weakening with very little effort. Thus, if you find such a weakening interesting or useful, I think it is doable.

There is no difference between composed and nested judgements. Actually, the former is a typo. We should uniform the notation to "nested".

Concerning modal logics, a modality can be axiomatized with an operator $$ \box: \mathbb{U} \to \mathbb{U}$$ decorated by a bunch of axioms, of course, there is a lot of work to do (as in the case of Natural Deduction, to make everything follow nicely, but I think the paper shows that this is more a matter of patience than a matter of ideas.

Finally, thank you for the typos! We will implement them. Did you happen to have time to give a look to the paper? You may have any additional comment, don't be shy!

Ulrik Buchholtz (Dec 30 2021 at 20:32):

Ivan Di Liberti said:

I am incredibly late, sorry Ulrik. Life has been intense as I am moving recently, and of course there was panettone-time in the meanwhile. Let me try and address your comments.

Thanks for the reply! And no worries about being late!

I think there is no reason to be confused, the definition clearly talks about categories, in a very neat sense of the word, there is no ambiguity. Our notion generalises Natural Models, so there is nothing you can do with NM that you can't do with our notion.

Hm, I'll think about it some more, but even when working with strict categories, you'd get a groupoid of rules, unless you have a set of labels of rules with decoding functions. (But labels for judgments, rules, and cuts might be needed anyway to get a syntax for derivations?)

Of course, as you say, a weaker interpretation is available, and indeed essentially everything would carry to such a weakening with very little effort. Thus, if you find such a weakening interesting or useful, I think it is doable.

Good, I think that makes more sense, and I'll think about how it relates to natural models.

Concerning modal logics, a modality can be axiomatized with an operator $$ \box: \mathbb{U} \to \mathbb{U}$$ decorated by a bunch of axioms, of course, there is a lot of work to do (as in the case of Natural Deduction, to make everything follow nicely, but I think the paper shows that this is more a matter of patience than a matter of ideas.

Thanks, I'll think about it some more once I digest your presentation of natural deduction.

Finally, thank you for the typos! We will implement them. Did you happen to have time to give a look to the paper? You may have any additional comment, don't be shy!

I haven't looked at it since then, but I'll return to it soon, because I'd like to understand what you're doing!

Greta Coraglia (Jan 15 2022 at 15:33):

@Ivan Di Liberti if that's alright I'll leave here the link to my talk at ItaCa, maybe someone can find it an helpful first approach to the subject.

https://youtu.be/lfm8HH5gLyU

Ivan Di Liberti (Jan 24 2022 at 10:17):

I gave a talk at ItaCa21.

Title: Givant, Morley, Zilber.
Abstract: https://genoa-logic-group.github.io/itaca-workshop-2021/assets/abstracts/DiLibertiI.pdf

Very short summary: The talk is an invitation to some topics in Universal Algebra that are not very well known in our community. The leading question is can we characterise algebraic theories for which every algebra is free? (Examples are pointed sets, or vector spaces).

Video: https://www.youtube.com/watch?v=9cGgOmnqzvE

Tom Hirschowitz (May 11 2022 at 09:11):

@Greta Coraglia Very helpful, thanks for posting! I really like the approach, which I learnt from in another online talk by @Ivan Di Liberti some time ago. The definition of dependent type theory as an adjunction between discrete fibrations is really clean, imho.

One thing that's a bit mysterious to me is the notation for nested judgements. How do you parse, e.g., $Fλ.H$? Is it $F;λ(H)$, in the sense of $F$, "composed" with $λ$ applied to $H$? If so, I'd suggest at least a space, as in $F\ λ.H$, but possibly a more visible symbol like $;$, to emphasise the separation.

Mathematical question 1: why do you insist on using #-liftings instead of plain cartesian liftings (in the 2-categorical sense)?

Mathematical question 2: you lost me in the examples on toyMLTT involving equalisers: the equalisers you take are equalisers in $\mathbf{Cat}$, right? If so, why would the equaliser of $(π₁,π₂)$ differ from the diagonal? E.g., for identity type formation, I'd have expected a rule from the equaliser of $\dot{\mathbb{U}} × \dot{\mathbb{U}} \rightrightarrows \mathbb{U}$ (two terms of the same type) to $\mathbb{U}$. How far off the point is this?

Finally, one future work that might be useful is to design a notion of signature ($\approx$ sketch), to describe these judgemental theories formally, and prove that each signature admits an initial model. But maybe this is related to the completeness result you mention in the conclusion? I didn't quite get what you meant there. :sweat_smile:

Ivan Di Liberti (May 11 2022 at 09:52):

Hi Tom, thank you very much for your comments. This week I am in Brno for the PSSL106 and I cannot comment as much as I would like, especially on a technical level. Sparse comments:

(a) Concerning the definition of a ddt as an adjunction between fibrations, one should acknowledge that in the case of discrete fibrations, this was already in Awodey's natural models, even though very implicitly (see rmk 3.1.3 in our paper). Our contributions in the paper (in my opinion) are to (1) generalize it to fibrations, (2) because in Sec 2 we make a much more formal process of translation between the categorical presentation and the deductive system, the sense in which our structures model a dtt is much more precise then Awodeys (3) I think our proofs are crisper.

(b) About future work. I do not like to disclose the projects I am working on at the moment, I have lamented about others doing it in the past as I think it is a great way to overstretch one's influence and even to scientifically bully the other researchers. Thus I won't say much. Yet, given my scientific background and my recent scientific production (see also the paper with Osmond), one can imagine that I could have something like that in mind.

Greta Coraglia (May 11 2022 at 10:20):

@Tom Hirschowitz
Thanks for reaching out! I'll try to answer the remaining questions.

Tom Hirschowitz said:

One thing that's a bit mysterious to me is the notation for nested judgements. How do you parse, e.g., $Fλ.H$? Is it $F;λ(H)$, in the sense of $F$, "composed" with $λ$ applied to $H$? If so, I'd suggest at least a space, as in $F\ λ.H$, but possibly a more visible symbol like $;$, to emphasise the separation.

In choosing the notation we had a bit of a struggle (to say the least!): we needed a way in which we could encode a lot of information, yet compact enough to be readable after many iterations. We kind of wanted to express the fact that $H$ is free, while at the same time describing the way in which $F$ is instead bounded to it, hence the moving around of the $\ λ$ part. Perhaps I like your suggestion better, after all the symbol $.$ has a very precise meaning in the context of dependent types, but that also is not far from our original intuition for nested judgments i.e. the binding relation.

Tom Hirschowitz said:

Mathematical question 1: why do you insist on using #-liftings instead of plain cartesian liftings (in the 2-categorical sense)?

Our starting point was: what if we read diagrams in a 2-category? It is clear that #-lifting would not be possible without a fibration, and in fact it details what a fibration does, but we needed the information encoded in diagram-form. Does this make sense?

Tom Hirschowitz said:

Mathematical question 2: you lost me in the examples on toyMLTT involving equalisers: the equalisers you take are equalisers in $\mathbf{Cat}$, right? If so, why would the equaliser of $(π₁,π₂)$ differ from the diagonal? E.g., for identity type formation, I'd have expected a rule from the equaliser of $\dot{\mathbb{U}} × \dot{\mathbb{U}} \rightrightarrows \mathbb{U}$ (two terms of the same type) to $\mathbb{U}$. How far off the point is this?

It does not differ from the diagonal! It was just about encoding the correct input, that is having $\dot{\mathbb{U}}$ as a starting point. In fact, your predictions for identity types are precisely right! You can read about them in Section 3.6 of the newest arXiv version. I hope you can enjoy how, in our framework, what one guesses is precisely what one has to ask of the theory.

Also, I hope I didn't ramble too much.

Tom Hirschowitz (May 11 2022 at 11:59):

@Ivan Di Liberti Yes, I saw that paper. It's on my reading list, but I admit it's a bit scary!

Tom Hirschowitz (May 11 2022 at 12:10):

@Greta Coraglia Thanks for your quick answers!

In choosing the notation we had a bit of a struggle (to say the least!): we needed a way in which we could encode a lot of information, yet compact enough to be readable after many iterations. We kind of wanted to express the fact that $H$ is free, while at the same time describing the way in which $F$ is instead bounded to it, hence the moving around of the $\ λ$ part. Perhaps I like your suggestion better, after all the symbol $.$ has a very precise meaning in the context of dependent types, but that also is not far from our original intuition for nested judgments i.e. the binding relation.

Not quite following this one, sorry.
Do you mean that my initial suggestion (i.e., it should be parsed as $F;\lambda(H)$) is wrong?
If so, second attempt: are you thinking of it as a ternary operator with arguments $F,\lambda,H$?

Our starting point was: what if we read diagrams in a 2-category? It is clear that #-lifting would not be possible without a fibration, and in fact it details what a fibration does, but we needed the information encoded in diagram-form. Does this make sense?

Surely does, but cartesian liftings also exist in diagram form, right? (See [[fibrations in a 2-category]] for a start.) Reading the beginning of the paper, I couldn't tell why such 2-categorical liftings wouldn't suit your needs.

Greta Coraglia (May 12 2022 at 10:21):

@Tom Hirschowitz
(Ha, sorry for the delay, I got swamped with academic responsibilities)

You make a very good point, but we kind of noticed that you don't need such a powerful environment to do the calculations we describe. In fact, we pin-pointed that particular construction because that was sufficient to do so. Moreover, one could ask whether

p is a fibration iff every such #-lifting exists

and if you try to make it work you realize that such notion is much weaker (mostly for compatibility reasons).
Now, this clearly poses the question of:

what if we endow our calculus with even stronger deductive power (i.e. the full power of a fibration)? What more could we prove?

That I do not know the answer to, but it sounds pretty interesting to me, though I admit I wish I had some consistency results* on our calculus first, so that I could check that such a consistency is preserved through the extension of the deductive power of the system.

*Do not mistake me here, I have good reasons to believe that it is, in fact, consistent, but our calculus has so many more rules - though well organized - than regular calculi that I cannot write such a result properly, yet.

Greta Coraglia (May 12 2022 at 10:23):

Tom Hirschowitz said:

If so, second attempt: are you thinking of it as a ternary operator with arguments $F,\lambda,H$?

I think I would go for $F\lambda ; G$ as to make it clear about what the position of the rule is, but I want to hear @Ivan Di Liberti's opinion on this one too :wink:

Tom Hirschowitz (May 12 2022 at 15:15):

Greta Coraglia said:

such notion is much weaker (mostly for compatibility reasons).

Oh! I didn't notice this. :grimacing: But it makes sense, thanks!

That I do not know the answer to, but it sounds pretty interesting to me, though I admit I wish I had some consistency results* on our calculus first, so that I could check that such a consistency is preserved through the extension of the deductive power of the system.

What would you call a consistency result in this setting? Do you mean you're not yet entirely sure that, e.g., dependent type theory would form such an enhanced judgemental theory?

Ivan Di Liberti (Nov 08 2022 at 18:12):

So, in the last week two papers with my name have appeared on the arXiv. Let me say something about them.

(1) KZ monads and Kan Injectivity, j.w. Gabriele Lobbia, Lurdes Sousa.

Let $T$ be a KZ doctrine on Cat. Say the (small) presheaf construction, which we all know and like, then its category of pseudoalgebras is the $2$-category of cocomplete categories and cocontinuous functors between them. In this case it is well known that those can be described as those categories which are "Kan injective" with respect to the Yoneda embeddings, in the sense that we can always Kan extend along Yoneda when the codomain is a cocomplete category.
This is a quite general pattern, and it is known that for every KZ-doctrine we can describe its pseudoalgebras as those objects that are Kan injective with respect to the units.

This result is much easier to understand, and serves as a motivation for our main theorem, if we downgrade lax-idempotent pseudomonads to idempotent monads (their 1-dimensional downgrade). There it is clear that the category of algebras for an idempotent monad is detected by being orthogonal with respect to the units.

Yet, it is also (somewhat) the other way around!

Given a class of maps in a $1$-category K, we can show that under some reasonable condition, its full subcategory of orthogonal objects is reflective in K. Classically this is done by use of the small object argument, and is known under the name of "the orthogonal subcategory problem", which allows to formulate many problems in Category theory in terms of some forms of the AFT.

In the paper we show that, given a class of $1$-cells in a reasonable $2$-category K, its locally full subcategory of Kan injective objects is the category of pseudoalgebras for a KZ monad.

Ivan Di Liberti (Nov 08 2022 at 18:21):

(2) The geometry of Coherent topoi and Ultrastructures.

One of the leitmotivs of topos theory is that we can use geometric intuition as a guiding principle to devise correct definitions. The motivation for this paper is to clarify the notion of ultrastructure and ultracategory via a geometric approach. Ultrastructures were defined by Makkai to condense the main properties of the category of models of a first order theory. He successfully used this technology to provide a reconstruction theorem for first order logic that goes under the name of conceptual completeness.

This result falls under the umbrella of Stone-like dualities, as many others celebrated results like. The general idea behind an ultrastructure is to account for the construction of ultraproducts of models. Indeed, given a coherent/first order theory $\mathbb{T}$, a set $X$, and an ultrafilter $U \in \beta(X)$, one can define the functor,

$$\int_X (-)dU: \mathsf{Mod}(\mathbb{T})^X \to \mathsf{Mod}(\mathbb{T}).$$

Such functor takes an $X$-indexed family of models and computes the ultraproduct of those along the ultrafilter $U$.

Despite delivering a very satisfactory theorem, the notion of ultrastructure seemed quite complicated -- if not ad-hoc -- and it was never clear whether it was the correct or definitive notion. The first attempt of providing a more conceptual framing to understand ultrastructures and ultracategories was given by Marmolejo in his PhD thesis.

In more recent years Lurie revisited the notion of ultracategory, proposing a morally similar, but technically different notion of ultrastructure, ultracategory and ultrafunctor with respect to Makkai's one. Both Makkai's and Lurie's notions are justified by the fact that they manage to deliver the most compelling theorems of this theory. Yet, none of these notions appears definitive when read or encountered for the first time for several reasons. The main one being that the definition of ultracategory is in both cases very heavy, and comes together with axioms whose choice seems quite arbitrary; and indeed the two authors make different choices.

In the paper I study the geometric properties of coherent topoi with respect to flat embeddings, so that the notion of ultrastructure emerge naturally from general considerations on the topology of flat embeddings.