Noncoherent wild higher precategories

[fredrik-bakke]

• Large and small noncoherent wild higher precategories
• maps of globular types
• maps of noncoherent wild higher precategories
• Colax functors of noncoherent wild higher precategories
  • Induced colax functor on hom-categories
  • Composition of colax functors and identity colax functor
• Isomorphisms in noncoherent wild higher precategories (due to @VojtechStep)

[fredrik-bakke]

Turns out, to define lax functors of large wild $(∞,∞)$-precategories, we will need to define lax functors of small wild $(∞,∞)$-precategories first :/

[fredrik-bakke]

Perhaps now is a good point to pause for some feedback. It only remains to add colax functors of noncoherent large wild $(∞,∞)$-precategories before I think this PR should be merged. After this PR there are multiple branches to investigate:

• 1-coherent wild $(∞,∞)$-precategories or some other notion of coherence
• extensional wild $(∞,∞)$-precategories, i.e., wild $(∞,∞)$-categories
• wild $(∞,r)$-precategories
• wild $(∞,∞)$-precategories with weak equivalences

Currently, I am most worried about wild $(∞,r)$-precategories, because a $k$-coherent $(∞,r)$-precategory is not simply a $k$-coherent $(∞,∞)$-precategory where the higher morphisms are invertible, and induction on $r$ sounds like will cause a bit of headache, so a strategic approach may save us a lot of work. There is also a conflict with extensional wild $(∞,∞)$-precategories with weak equivalences, since the weak equivalences should coincide with the isomorphisms for these.

[fredrik-bakke]

I've been looking into whether the current definition is that of a lax or colax functor, and the majority seems to agree that it's a colax functor.

These sources suggest that the definition we have is of a colax functor:

• Urs Schreiber - Note on Lax Functors and Bimodules (https://www.math.uni-hamburg.de/home/schreiber/LaxFunc.pdf)
• Niles Johnson and Donald Yau - 2-Dimensional Categories (https://arxiv.org/pdf/2002.06055.pdf)
• LS Barbosa - A brief introduction to bicategories (https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=e035e4f40a62382c10bac021140581970f44660d)
• Stephen Lack - A 2-categories companion (https://people.math.rochester.edu/faculty/doug/otherpapers/Lack.pdf)
• Wikipedia (https://en.wikipedia.org/wiki/Lax_functor)

While this source suggests it's a lax functor:

• nlab 2-functors (https://ncatlab.org/nlab/show/2-functor#pseudofunctor_between_strict_categories)

I also checked the following sources, but they do not define lax functors

• The article Bicategories in Univalent Foundations (https://arxiv.org/abs/1903.01152) does not define lax functors, but its definition of pseudofunctor seems to suggest that our definition is that of lax functors. Interestingly, however, their formalization suggests the opposite.
• Categories for the working mathematician
• Category theory in context
• Elements of ∞-category theory

[fredrik-bakke]

Alright, I added some more explanations and I'm finally opening this PR for review.

[fredrik-bakke]

As observed by Thomas today, we also need to axiomatize a whiskering operation for our wild higher categories.

[fredrik-bakke]

Thanks for the nice review, I'll try to adress all of it right now.

[EgbertRijke]

Awesome! Let me know when you're done. This PR will be a very valuable addition to the library

[fredrik-bakke]

I'll also note here, as mentioned to me by Niels, that (co)lax functors are not a good notion, as they can in general fail to preserve good notions of equivalence. Therefore it seems we should not prioritize the lax notion and instead work with (pseudo-)functors.

[fredrik-bakke]

As observed by Thomas today, we also need to axiomatize a whiskering operation for our wild higher categories.

Although I haven't worked this out, it seems to me like whiskering should fall out of functoriality for hom.

[EgbertRijke]

That's alright. Does the concept improve if we require all the coherence cells to be isomorphisms?

[EgbertRijke]

As observed by Thomas today, we also need to axiomatize a whiskering operation for our wild higher categories.

Although I haven't worked this out, it seems to me like whiskering should fall out of functoriality for hom.

Great! Perhaps we can establish that in a subsequent PR

[fredrik-bakke]

That's alright. Does the concept improve if we require all the coherence cells to be isomorphisms?

Yes, this will always (meaning in the univalent case) be a good notion.

[fredrik-bakke]

Okay, I think I addressed it all now, @EgbertRijke. I found an indexing error in the prose about colax functors that I corrected too.

[EgbertRijke]

For merging I will remove myself as a coauthor. @VojtechStep is mentioned in the PR description, and is automatically added as a coauthor, so I will keep him on as a coauthor.

If you confirm with a thumbs-up then I will enable auto-merge.