adding hyperdoctrines to Mathlib

Stream: mathlib4

[Samy Avrillon]

Hello.
I asked in this zulip permission to create a branch to add hyperdoctrines to Mathlib.
In my message I reference a paper from Robert Seely in which this notion is defined.
I have been answered that this concept might not be fit for insertion into Mathlib as it was touching non-classical logics.
Hyperdoctrines are a way to formalize the semantics of first order logics, in the same way as Heyting algebras allow us to formalize propositional logics (including both classical and non-classical logics).
Similarly, hyperdoctrines can be used to formalize both classical and non-classical first order logics, even when using a classical metatheory (as that provided by Mathlib).
An interesting instance of the structure of hyperdoctrines arise from (a fragment of) the internal logic of Grothendieck toposes and one of my coworker is currently working out this instance.
For all these reasons, we think that Mathlib could benefit from being added a notion of hyperdoctrines and first order hyperdoctrines (i.e. hyperdoctrines over Heyting algebras)
What do you think ?

[Johan Commelin]

I personally think that hyperdoctrines are in scope for mathlib. A classical library can still have theory about non-classical logics (-; And of course hyperdoctrines have a bunch of applications besides non-classical logics.

[Ruben Van de Velde]

I'll make a note that @Johan Commelin volunteers to review :)

[Sina Hazratpour 𓃵]

@Samy Avrillon It might be helpful for you to know that we have done Beck-Chevalley condition in our LCCC development, and I am currently PRing this stuff to mathlib.

https://github.com/sinhp/Poly/blob/0740abde64b16779ab031e1c2cad61b929c9b32d/Poly/LCCC/BeckChevalley.lean

In Seely's paper you references that is page 511 as part of the definition of hyperdoctrines. Our approach to formalization of Beck-Chevalley was based on the theory of mates and a double-categorical adjunction you can find in the section 2 of the following paper with Emily Riehl:

A 2-categorical proof of Frobenius for fibrations defined from a generic point

[Samy Avrillon]

Hello @Sina Hazratpour 𓃵
Thank you for your message
Actually, i was already using formalization of Beck-Chevalley using the theory of mates (using CategoryTheory.mateEquiv like you do). Seely's paper reference was here to give a formal definition of Hyperdoctrines, expecially about «Which pullbacks should respect Beck-Chevalley condition» (Seely's answer is «all of them», but one could answer «only the projection pullbacks»).
I would gladly make branch my changes from your PR, thank you for sharing !

[Samy Avrillon]

@Kevin Buzzard After everything that has been said above, do you think you can give me access to a new branch on Mathlib github so i can start working on adding Hyperdoctrines ?

[Kevin Buzzard]

Yes definitely! I'm sorry nobody did this yet!

[Kevin Buzzard]

Oh -- can you put your github username in your Zulip profile @Samy Avrillon ?

[Samy Avrillon]

Done !

[Kim Morrison]

@Samy Avrillon, please check your (email) inbox for the invitation.

[Sina Hazratpour 𓃵]

@Samy Avrillon I forgot to share with you my PR on Beck-Chevalley condition:
https://github.com/leanprover-community/mathlib4/pull/22340

It's WIP, everything is done except the pentagon distributivity, which is under construction.

[Samy Avrillon]

Hello @Sina Hazratpour 𓃵

I found your PR and started to study it, thank you for that !
I have seen that you are defining a Beck-Chevalley condition on the Over category, as you do in (your paper with Emily Riehl)[https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/2categorical-proof-of-frobenius-for-fibrations-defined-from-a-generic-point/8A9A180160D0833C108E51B0B5D1E6F2]
I need the Beck-Chevalley condition in another context:
I have a pullback-preserving functor P from a category C to Cat, and for every morphism f : A -> B in C, i have a morphism ∀f : PA -> PB in Cat which is right adjoint to Pf
I want to state, that for any pullback in C (CommSq h f g k), that the mate of the image by P of the pullback (CommSq Ph Pf Pg Pk) is inversible.

It looks like your development is a _specialized_ case of what i want to do (taking a functor P that sends object X to Over X and mapping f to Over.map f, and the left adjoint construction is given by mapPullbackAdj)

Therefore i have two questions:

• Do you think that we can use you development to match your case (using a specific case of over categories). I don't see how you can do that, but maybe you have an idea.
• Are you okay with me generalizing the Beck-Chevalley condition so it applies both to my development and yours ?

Thank you very much !

[Sina Hazratpour 𓃵]

Interesting!

Indeed, I've been focusing on the more restricted case of the Beck-Chevalley for the Over prestack (aka pseudo-functor) since I wanted to develop LCCCs and Polynomial functors. And the file I PR'd to mathlib is in fact in the subdirectory LocallyCartesianClosed.

Note that this PR is WIP and usually a little behind the same file in the Poly project:
Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley

The Poly version uses the API of TwoSquare which was added to mathlib couple of days ago by @Joël Riou and @Jakob von Raumer .

I assume for hyperdoctrines you need the BC squares for a general pseudo-functor P : C => Cat, and not just for the representable Over : C => Cat.

I have a git repo that is developing BC for prestacks. I can add you to that as collaborator if you like. We can exploit the 2-categorical Yoneda which says that the space Over_C => P is equivalent to P (C). I think the triple adjunctions between P (C) and P (D) and the BC TwoSquares between them can be transferred from Over_C and Over_D, using Kan extensions.

[Samy Avrillon]

Thank you for your answer !
I cloned your Poly repository and i will try to add my Hyperdoctrines to it, in order to see if it will work when you will push to mathlib. I'll investigate the 2-Yoneda method, and i will try to write it in a generic way, and i can try to PR to your project (or you can add me as a contributor, and i will write on a secondary branch)

[Samy Avrillon]

Hello @Sina Hazratpour 𓃵 . Here is the current state of our work. I think we could take benefit from your point of view.

We work in the following context in order to define the notion of hyperdoctrine: we have a category $\mathcal{C}$ with all pullbacks and a contravariant functor $P : C^{\mathrm{op}} \to \operatorname{Cat}$ (where $\operatorname{Cat}$ is the 2-category of 1-categories with functors as 1-cells and natural transformations s 2-cells)
such that the image $P(f)$ of each arrow $f : X \to Y$ in $\mathcal{C}$ has both a left adjoint $\exists_f$ and right adjoint $\forall_f$ from $P(X)$ to $P(Y)$ in $\operatorname{Cat}$ ($\exists_f \dashv P(f) \dashv \forall_f$).

Given a commutative square in $\mathcal{C}$, we want to state the fact that the mate of the image by P of the commutative square (using the adjoints $\forall_-$) is an isomorphism (the Beck-Chevalley condition).

Our current plan goal is to reuse the statement that the mate of the image by $\mathcal{C}/-$ of the commutative square is an isomorphism .

Here's the proof sketch:
1) The image by the functor $C/-$ of the commutative square is a commutative square in $\operatorname{Fib}(\mathcal{C})$ (of fibrations with codomain $\mathcal{C}$).
2) We apply the pseudofunctor reciprocical to Grothendieck transformation $i : \operatorname{Fib}(\mathcal{C}) \to [C^{op}, \operatorname{Cat}]_{ps}$ to this diagram
3)Then, we apply further the contravariant pseudofunctor from $[C^{op}, \operatorname{Cat}]$ to $\operatorname{Cat}$ that associates to any functor $A$ the category $[C^{op}, \operatorname{Cat}](A,P)$
4) Finally, we apply the 2-yoneda equivalence to get the initial mate of the image by $P$ on the obtained square

If this method succeeds, we could prove using Sina's developpement that the initial mate obtained by P is always invertible if the initial commutative square is a pullback. This proof skecth is currently flawed because the functors $f^*$ employed to define the mate are not in $\operatorname{Fib}(\mathcal{C})$, so we can't translate the isomorphism directly.

Our main difficulty is that the right adjoint pullback functors used to define the Beck-Chevalley mate are not in the category $\operatorname{Fib}(\mathcal{C})$. Therefore, it is not trivial that we can apply the proof sketch to the mate 2-morphism in order to prove that our final 2-morphism exist and is iso.

What is your thought on this issue ? Did you think of some other developement that could avoid those difficulties ?