Refactor sub bicategories

[nmvdw]

In this PR:

• The notion of subbicategory (subbicat) is made more general
• I added two examples displayed bicategories over the bicategory of categories (not necessarily univalent ones). Both of these are about terminal objects: one is for chosen terminal objects, the other is for existing terminal objects.

The main reason to look at these bicategories is to study how it interacts with the Rezk completion. More specifically, what can we say about the Rezk completion of a category with a terminal object? Does it matter whether the terminal object is chosen or just exists?

[benediktahrens]

It seems to me that this file shows what happens when one does not use access functions. Could we add access functions instead of those projections?

[nmvdw]

The nicest way to do so, would be as follows:

#[nonuniform] Coercion univ_cat_of_univ_cat_with_terminal_obj
         (C : univ_cat_with_terminal_obj)
  : univalent_category
  := pr1 C.

Definition terminal_of_univ_cat_with_terminal_obj
           (C : univ_cat_with_terminal_obj)
  : Terminal C
  := pr12 C.

#[nonuniform] Coercion functor_of_univ_cat_with_terminal_obj_mor
         {C₁ C₂ : univ_cat_with_terminal_obj}
         (F : C₁ --> C₂)
  : C₁ ⟶ C₂
  := pr1 F.

Definition preserves_terminal_univ_cat_with_terminal_obj_mor
           {C₁ C₂ : univ_cat_with_terminal_obj}
           (F : C₁ --> C₂)
  : preserves_terminal F
  := pr22 F.

Both coercions don't respect the uniform inheritance condition, so I needed to add #[nonuniform] in order to suppress the warning arising from that (they do work though).

Would this solution be fine?

[benediktahrens]

Yes, I think that's good!

[nmvdw]

Okay, I tried it further and by adding these coercions to univ_cat_with_binprod,

#[nonuniform] Coercion univ_cat_of_univ_cat_with_binprod
         (C : univ_cat_with_binprod)
  : univalent_category
  := pr1 C.

Definition binprod_of_univ_cat_with_binprod
           (C : univ_cat_with_binprod)
  : BinProducts C
  := pr12 C.

The second definition is not accepted, and the first one gives the following warning:

univ_cat_of_univ_cat_with_binprod is defined
Warning:
New coercion path [univ_cat_of_univ_cat_with_binprod] : ob >-> univalent_category (reversible) is ambiguous with existing 
[univ_cat_of_univ_cat_with_terminal_obj] : ob >-> univalent_category (reversible).
[ambiguous-paths,typechecker]
univ_cat_of_univ_cat_with_binprod is now a coercion

The error for the second definition is:

Error:
In environment
C : univ_cat_with_binprod
The term "C" has type "ob univ_cat_with_binprod" while it is expected to have type "category".

So: it is not a good idea to have a coercion from the objects of a bicategory to something, because this coercion seem as a coercion from ob to categories and it does not take the bicategory into account.

Note that this idea was already used in:
https://github.com/UniMath/UniMath/blob/master/UniMath/Bicategories/DaggerCategories/BicatOfDaggerCats.v#L73
Now I think we should delete that coercion.

[nmvdw]

By deleting all coercions completely we would get the following:

Definition univ_cat_of_univ_cat_with_terminal_obj
           (C : univ_cat_with_terminal_obj)
  : univalent_category
  := pr1 C.

Definition terminal_of_univ_cat_with_terminal_obj
           (C : univ_cat_with_terminal_obj)
  : Terminal (univ_cat_of_univ_cat_with_terminal_obj C)
  := pr12 C.

Definition functor_of_univ_cat_with_terminal_obj_mor
           {C₁ C₂ : univ_cat_with_terminal_obj}
           (F : C₁ --> C₂)
  : univ_cat_of_univ_cat_with_terminal_obj C₁
    ⟶
    univ_cat_of_univ_cat_with_terminal_obj C₂
  := pr1 F.

Definition preserves_terminal_univ_cat_with_terminal_obj_mor
           {C₁ C₂ : univ_cat_with_terminal_obj}
           (F : C₁ --> C₂)
  : preserves_terminal (functor_of_univ_cat_with_terminal_obj_mor F)
  := pr22 F.

[benediktahrens]

I am not fully understanding the matter of coercions, but would like to. Could we discuss this in a meeting sometime?

Anyway, this is possibly something that is separate from the current PR. I would be happy with a solution without coercions for now. Also, the substitution of projections for access functions could happen in a later PR.

[nmvdw]

I am not fully understanding the matter of coercions, but would like to. Could we discuss this in a meeting sometime?

Sure.

Anyway, this is possibly something that is separate from the current PR. I would be happy with a solution without coercions for now. Also, the substitution of projections for access functions could happen in a later PR.

I think that is fine.

[benediktahrens]

lgtm, modulo #1709 to be addressed later