feat(FiberedCategory/HasFibers): define HasFibers class

[callesonne]

We define a class HasFibers p for a given functor p : 𝒳 ⥤ 𝒮. The point of this is to give the user the option to supply their own fiber categories, as often the standard fibers will not be definitionally the same as the (equivalent) categories one is interested in.

Co-authored-by: Paul Lezeau [email protected]

---

This is the final PR in a sequence of PRs developing the theory of fibered categories that I will make for now. I will wait for the reviewing to catch up before I start working on more of these again, so as to not create too big of a backlog.

• depends on: [Merged by Bors] - feat(FiberedCategory/Fiber): define the fibers of a functor #13603
• depends on: [Merged by Bors] - feat(FiberCategory/Fibered): define fibered functors #12982
• depends on: [Merged by Bors] - feat(FiberedCategory/Fibered): define prefibered categories #13416
• depends on: [Merged by Bors] - feat(FiberedCategory/Cartesian): define strongly cartesian morphisms #13410
• depends on: [Merged by Bors] - feat(FiberedCategory/Cartesian): define cartesian morphisms #13393

[joelriou]

The HasFibers class looks good to me. However, for the future API, it would be nice to introduce also a typeclass HasPullbacks which would be the data of pullback functors (when be category is prefibered) between the categories given by the HasFibers class, along with the universal property each of these functors should satisfy. HasPullbacks may extend HasFibers.
Then, under HasPullbacks, one may define the composition morphisms (for the pullback by a composition of maps in the base), which are isomorphisms in case of fibered categories.
(The idea is that if we have a pseudofunctor, there will be an obvious HasFibers instance attached to the associated fibered category functor, and also an obvious HasPullbacks instance, with very good definitional properties. Then, there may not be good definitional properties for the composition (iso)morphisms, but still they shall be equal to those that are part of the structure of a pseudofunctor.)
(I hope this makes sense. I am not sure we discussed these details already.)

[callesonne]

The HasFibers class looks good to me. However, for the future API, it would be nice to introduce also a typeclass HasPullbacks which would be the data of pullback functors (when be category is prefibered) between the categories given by the HasFibers class, along with the universal property each of these functors should satisfy. HasPullbacks may extend HasFibers. Then, under HasPullbacks, one may define the composition morphisms (for the pullback by a composition of maps in the base), which are isomorphisms in case of fibered categories. (The idea is that if we have a pseudofunctor, there will be an obvious HasFibers instance attached to the associated fibered category functor, and also an obvious HasPullbacks instance, with very good definitional properties. Then, there may not be good definitional properties for the composition (iso)morphisms, but still they shall be equal to those that are part of the structure of a pseudofunctor.) (I hope this makes sense. I am not sure we discussed these details already.)

This is what a clivage is right? If so I think we have discussed it. I think the name HasPullbacks is better than HasClivage so maybe we can go for that one. I think that @Paul-Lez has started writing some stuff related to this, and we definitely want to PR this in the future!

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(FiberedCategory/Fiber): define the fibers of a functor #13603
• [Merged by Bors] - feat(FiberCategory/Fibered): define fibered functors #12982
• [Merged by Bors] - feat(FiberedCategory/Fibered): define prefibered categories #13416
• [Merged by Bors] - feat(FiberedCategory/Cartesian): define strongly cartesian morphisms #13410
• [Merged by Bors] - feat(FiberedCategory/Cartesian): define cartesian morphisms #13393
  By Dependent Issues (🤖). Happy coding!

[callesonne]

I've removed awaiting-author for now, or do you mean that I should add HasPullbacks already to this PR? @joelriou

[joelriou]

I think this should not be an instance, only a def.

[callesonne]

Then will it still work as a "default instance"?

[joelriou]

I am not sure exactly what default_instance do. I think we should remove it.

[joelriou]

My opinion is that I would not like to have default instances flying around... If we need a HasFibers instance in order to prove a statement (which does not already involve a HasFibers), then we may invoke this canonical in order to make the argument work. Otherwise, [HasFibers p] should be a variable.

[joelriou]

I've removed awaiting-author for now, or do you mean that I should add HasPullbacks already to this PR? @joelriou

This PR is already long enough :-)