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).
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.
Definition cat_to_prebicat_2_id_comp_struct
: prebicat_2_id_comp_struct cat_to_prebicat_1_id_comp_cells.
Show proof.
Definition cat_to_prebicat_data
: prebicat_data.
Show proof.
Proposition cat_to_prebicat_laws
: prebicat_laws cat_to_prebicat_data.
Show proof.
Definition cat_to_prebicat
: prebicat.
Show proof.
Definition cat_to_bicat
: bicat.
Show proof.
: prebicat_1_id_comp_cells.
Show proof.
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).
- 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.
- 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.
Definition cat_to_prebicat
: prebicat.
Show proof.
Definition cat_to_bicat
: bicat.
Show proof.
refine (cat_to_prebicat ,, _).
abstract
(intros x y f g p q ;
apply isasetaprop ;
apply homset_property).
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.
Proposition locally_groupoid_cat_to_bicat
: locally_groupoid cat_to_bicat.
Show proof.
Proposition is_univalent_2_1_cat_to_bicat
: is_univalent_2_1 cat_to_bicat.
Show proof.
Proposition is_discrete_cat_to_bicat
: is_discrete_bicat cat_to_bicat.
Show proof.
: isaprop_2cells cat_to_bicat.
Show proof.
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.
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.
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.- exact is_univalent_2_1_cat_to_bicat.
- exact locally_groupoid_cat_to_bicat.
- exact isaprop_2cells_cat_to_bicat.