WIP: identifies developments that can be done with CAT

[rmatthes]

CAT = the bicategory of categories

This means, without taking univalent categories (UCAT) but just precategories with homsets.

The new files are simple adaptations of the respective files without "WithoutUnivalence" in their name.

Biadjunction.v now does not refer to UCAT but to CAT, this needed more material in BicatOfCatsWithoutUnivalence.v to be taken from the development for UCAT.

Final.v and Initial.v did not even depend on UCAT (a redundant import)
Strictness.v only depends on UCAT for an example (better, a counter-example)
Monads.v: disp_2cells_isaprop_monad does not need the hypothesis is_univalent_2 C
MonadKtripleBiequiv.v: adapted to that change in Monads.v

[benediktahrens]

What is the status of this PR? Is the goal to have it merged? Or is it only a basis for discussion?
Also, will it be in conflict with #1391 ?

[rmatthes]

It is rather a request for comments. No conflict with #1391 envisaged.

The main question: is it good to have two separate strands instead of first developing the stuff without univalence and then taking the full sub-bicategory. The current PR shows to what extent one can proceed without univalence. The untouched files did not promise to me a good version without univalence. But experts on the bicategories library will be in a better position to judge.

[nmvdw]

It is rather a request for comments. No conflict with #1391 envisaged.

The main question: is it good to have two separate strands instead of first developing the stuff without univalence and then taking the full sub-bicategory. The current PR shows to what extent one can proceed without univalence. The untouched files did not promise to me a good version without univalence. But experts on the bicategories library will be in a better position to judge.

This is something we considered in the development of the library of bicategories. Because the bicategory of univalent categories is quite important in this library, we would like that it is convenient to use it. In addition, we want to be able to make use of displayed machinery (displayed bicategories, displayed pseudofunctors and so on) as much as possible. This is useful for proving the univalence of bicategories and for constructing pseudofunctors, biadjunctions, biequivalences and so on.

For this reason, we first of all decided to define the full subbicategory via displayed bicategories. This has consequences on what the actual full subbicategory looks like: if we have a bicategory B and a predicate P on the objects of B, then the full subbicategory (as we defined in UniMath) looks as follows:

• its objects are objects x of B for which P is satisfied
• the morphisms are morphisms in B together with an inhabitant of the unit type
• the 2-cells are 2-cells in B together with an inhabitant of the unit type
  These inhabitants from the unit type come from the fact that we defined the full subbicategory via displayed bicategories. The relevant parts in the code are:

• UniMath/UniMath/Bicategories/DisplayedBicats/Examples/FullSub.v

  Line 35 in 2075f7d

  Definition disp_fullsubprebicat : disp_prebicat C

• UniMath/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedCatToBicat.v

  Line 43 in 2075f7d

  Section Disp_Prebicat_Cells_Unit.

For this reason, if we define the bicategory of univalent categories using a full subbicategory, the 1-cells are functors together with an inhabitant of the unit type. Hence, if you use the full subbicategory as defined currently in UniMath, then I suspect there are some difficulties in modifying the code. Of course, these can be solved, but using the bicategory of univalent categories will be more tedious in this case.

However, it is also possible to define the full subbicategory directly and without using displayed machinery. If this approach is used, then I think there won't be many technical difficulties. As a result, there will be 2 definitions of the full subbicategory though.

[rmatthes]

Good explanation. I cannot decide on that matter. Is the code copying acceptable in the present form - hence with rather long file names? Would more of the developments involving UCAT as I called it above be possible with CAT, maybe with some extra effort? I am thinking in particular of Bicategories/DisplayedBicats/Examples/MonadKtripleBiequiv.v .

[benediktahrens]

There are two orthogonal, but intersecting, questions:

1. What is the right notion of category?
2. Should one formalize stuff in terms of displayed machinery?

The answer to 1 is clear: the unadorned "categories" are not the right thing. It might have been a strategic mistake to use the vocabulary "category" and "univalent category" instead of "precategory" and "category". Sticking with the former, it is clear that many constructions can be done on categories, not requiring the univalence property. Instead of univalence being a useful property, it is an obligation: we have to show that new categories we construct are univalent. The univalence property is not optional.

The answer to 2 is less clear: defining the type of objects by itself, instead of as part of a (displayed) (bi)category, has performance benefits, since otherwise referring to the objects always requires forgetting the whole category structure. I hence think that having a stand-alone definition of the objects can be very useful. Occasionally, an equivalence of types between the stand-alone definition and the type of objects of a (total) (bi)category might be required - this equivalence can be used as an interface to the objects of the (bi)category, allowing us to forget about spurious unit types.

[rmatthes]

I am trying to resolve the conflicts still today.

[rmatthes]

Should be fine again.