Library UniMath.Bicategories.Core.Examples.DiscreteBicat

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Discreteness.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Univalence.

Local Open Scope cat.

Section CatToBicat.
  Context (C : category).

1. The discrete bicategory
  Definition cat_to_prebicat_1_id_comp_cells
    : prebicat_1_id_comp_cells.
  Show proof.
    simple refine (_ ,, _).
    - exact C.
    - exact (λ x y f g, f = g).

  Definition cat_to_prebicat_2_id_comp_struct
    : prebicat_2_id_comp_struct cat_to_prebicat_1_id_comp_cells.
  Show proof.
    repeat split.
    - intros x y f ; cbn.
      apply id_left.
    - intros x y f ; cbn.
      apply id_right.
    - intros x y f ; cbn.
      exact (!(id_left _)).
    - intros x y f ; cbn.
      exact (!(id_right _)).
    - intros w x y z f g h ; cbn.
      apply assoc'.
    - intros w x y z f g h ; cbn.
      apply assoc.
    - intros x y f g h p q ; cbn.
      exact (p @ q).
    - intros x y z f g₁ g₂ p ; cbn.
      exact (maponpaths (λ z, f · z) p).
    - intros x y z f₁ f₂ g p ; cbn.
      exact (maponpaths (λ z, z · g) p).

  Definition cat_to_prebicat_data
    : prebicat_data.
  Show proof.
    simple refine (_ ,, _).
    - exact cat_to_prebicat_1_id_comp_cells.
    - exact cat_to_prebicat_2_id_comp_struct.

  Proposition cat_to_prebicat_laws
    : prebicat_laws cat_to_prebicat_data.
  Show proof.
    repeat split ; intro ; intros ; apply homset_property.

  Definition cat_to_prebicat
    : prebicat.
  Show proof.
    simple refine (_ ,, _).
    - exact cat_to_prebicat_data.
    - exact cat_to_prebicat_laws.

  Definition cat_to_bicat
    : bicat.
  Show proof.
    refine (cat_to_prebicat ,, _).
    abstract
      (intros x y f g p q ;
       apply isasetaprop ;
       apply homset_property).

2. The discrete bicategory is discrete
  Proposition isaprop_2cells_cat_to_bicat
    : isaprop_2cells cat_to_bicat.
  Show proof.
    intros x y f g p q.
    apply homset_property.

  Proposition locally_groupoid_cat_to_bicat
    : locally_groupoid cat_to_bicat.
  Show proof.
    intros x y f g α.
    refine (!α ,, _ ,, _).
    - apply isaprop_2cells_cat_to_bicat.
    - apply isaprop_2cells_cat_to_bicat.

  Proposition is_univalent_2_1_cat_to_bicat
    : is_univalent_2_1 cat_to_bicat.
  Show proof.
    intros x y f g.
    use isweqimplimpl.
    - exact (λ p, pr1 p).
    - apply homset_property.
    - use isaproptotal2.
      + intro.
        apply isaprop_is_invertible_2cell.
      + intros.
        apply homset_property.

  Proposition is_discrete_cat_to_bicat
    : is_discrete_bicat cat_to_bicat.
  Show proof.
    repeat split.
    - exact is_univalent_2_1_cat_to_bicat.
    - exact locally_groupoid_cat_to_bicat.
    - exact isaprop_2cells_cat_to_bicat.
End CatToBicat.