# Library UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat

Discrete displayed bicategories
Given a displayed category on some bicategory, we construct a displayed bicategory from it. The 2-cells are from the unit type.
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.DisplayedCats.Auxiliary.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.Initial.
Require Import UniMath.Bicategories.Core.Examples.Final.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles.
Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.

Local Open Scope cat.
Local Open Scope mor_disp_scope.

Definition is_chaotic
{C : bicat}
(D : disp_bicat C)
: UU
:= (a b : C) (f g : a --> b) (α : f ==> g)
(aa : D a) (bb : D b)
(ff : aa -->[ f ] bb) (gg : aa -->[ g ] bb),
iscontr (ff ==>[ α ] gg).

Definition isaprop_is_chaotic
{C : bicat}
(D : disp_bicat C)
: isaprop (is_chaotic D).
Proof.
repeat (apply impred ; intro).
apply isapropiscontr.
Qed.

Section Disp_Prebicat_Cells_Unit.
Context {C : bicat} (D : disp_cat_data C).

Definition disp_prebicat_cells_unit
: disp_prebicat_1_id_comp_cells C.
Proof.
D. red. intros. exact unit.
Defined.

Definition disp_prebicat_cells_unit_ops
: disp_prebicat_ops disp_prebicat_cells_unit.
Proof.
repeat use tpair; cbn; intros; exact tt.
Defined.

Definition disp_prebicat_cells_unit_data : disp_prebicat_data C
:= _ ,, disp_prebicat_cells_unit_ops.

Lemma disp_prebicat_cells_unit_laws
: disp_prebicat_laws disp_prebicat_cells_unit_data.
Proof.
repeat use tpair; red; intros; apply (proofirrelevance _ isapropunit).
Qed.

Definition disp_cell_unit_prebicat : disp_prebicat C
:= _ ,, disp_prebicat_cells_unit_laws.

Definition disp_cell_unit_bicat : disp_bicat C.
Proof.
refine (disp_cell_unit_prebicat ,, _).
intros a b f g x aa bb ff gg.
apply isasetunit.
Defined.

Local Univalence
Definition disp_cell_unit_bicat_univalent_2_1
(H : (a b : C)
(f : a --> b)
(aa : D a) (bb : D b),
isaprop (aa -->[ f] bb))
: disp_univalent_2_1 disp_cell_unit_bicat.
Proof.
intros a b f g p aa bb ff gg.
use isweqimplimpl.
- unfold idfun.
cbn in ×.
intros.
apply H.
- apply isasetaprop.
exact (H a b g aa bb).
- simple refine (isaprop_total2 (_ ,, _) (λ η , _ ,, _)).
+ exact isapropunit.
+ apply (@isaprop_is_disp_invertible_2cell C disp_cell_unit_bicat).
Defined.

Global Univalence
Definition disp_cell_unit_bicat_is_disp_invertible_2cell
{a b : C}
{f : a --> b} {g : a --> b}
(x : invertible_2cell f g)
{aa : disp_cell_unit_bicat a}
{bb : disp_cell_unit_bicat b}
{ff : aa -->[ f ] bb}
{gg : aa -->[ g ] bb}
(xx : ff ==>[ x ] gg)
: is_disp_invertible_2cell x xx.
Proof.
use tpair.
- exact tt.
- split ; apply isapropunit.
Defined.

{a b : C}
{aa : disp_cell_unit_bicat a}
{bb : disp_cell_unit_bicat b}
(ff : aa -->[ f] bb)

Proof.
intros gg.
use tpair.
- use tpair.
+ exact gg.
+ exact (tt ,, tt).
- split ; split ; cbn.
+ apply isapropunit.
+ apply isapropunit.
+ exact (disp_cell_unit_bicat_is_disp_invertible_2cell
tt).
+ exact (disp_cell_unit_bicat_is_disp_invertible_2cell
tt).
Defined.

{a b : C}
{aa : disp_cell_unit_bicat a}
{bb : disp_cell_unit_bicat b}
(ff : aa -->[ f] bb)

Proof.
intros H.
apply H.
Defined.

Definition disp_cell_unit_bicat_disp_cellset : has_disp_cellset disp_cell_unit_bicat.
Proof.
intro ; intros.
apply isasetunit.
Defined.

{a b : C}
{aa : disp_cell_unit_bicat a}
{bb : disp_cell_unit_bicat b}
(ff : aa -->[ f] bb)

Proof.
refine (disp_cell_unit_bicat_left_adjoint_equivalence f ff ,, _).
use isweq_iso.
- reflexivity.
- intros y.
use subtypePath.
+ intro.
do 2 apply isapropdirprod.
× apply disp_cell_unit_bicat_disp_cellset.
× apply disp_cell_unit_bicat_disp_cellset.
× apply isaprop_is_disp_invertible_2cell.
× apply isaprop_is_disp_invertible_2cell.
+ cbn.
use total2_paths_b.
× reflexivity.
× use total2_paths_b ; apply isapropunit.
Defined.

{a b : C}
(aa : disp_cell_unit_bicat a)
(bb : disp_cell_unit_bicat b)

Proof.
use weqfibtototal ; cbn.
intro.
Defined.

Definition disp_cell_unit_bicat_idtoiso
{a b : C}
(p : a = b)
(aa : disp_cell_unit_bicat a)
(bb : disp_cell_unit_bicat b)
: transportf disp_cell_unit_bicat p aa = bb

(aa -->[ idtoiso_2_0 _ _ p ] bb)
×
Proof.
induction p ; cbn ; unfold idfun.
intros pp.
induction pp ; cbn.
split ; apply id_disp.
Defined.

Definition disp_cell_unit_bicat_univalent_2_0
(HC : is_univalent_2_1 C)
(HDP : (a b : C)
(f : a --> b)
(aa : D a) (bb : D b),
isaprop (aa -->[ f] bb))
(Dset : (a : C), isaset (D a))
(inv : (a : C) (aa bb : disp_cell_unit_bicat a),
(aa -->[ id₁ a ] bb × bb -->[ id₁ a ] aa)

aa = bb)
: disp_univalent_2_0 disp_cell_unit_bicat.
Proof.
apply fiberwise_univalent_2_0_to_disp_univalent_2_0.
intros a aa bb.
use isweqimplimpl.
- intro η ; cbn ; unfold idfun.
apply inv.
(idtoiso_2_0 a a (idpath a))
aa bb) η).
- apply (Dset a).
- apply (isofhlevelweqf 1 (disp_cell_unit_bicat_adjoint_equivalent _ _ _)).
apply isapropdirprod ; apply HDP.
Defined.

Definition disp_cell_unit_bicat_univalent_2
(HC : is_univalent_2_1 C)
(HDP : (a b : C)
(f : a --> b)
(aa : D a) (bb : D b),
isaprop (aa -->[ f] bb))
(Dset : (a : C), isaset (D a))
(inv : (a : C) (aa bb : disp_cell_unit_bicat a),
(aa -->[ id₁ a ] bb × bb -->[ id₁ a ] aa)

aa = bb)
: disp_univalent_2 disp_cell_unit_bicat.
Proof.
split.
- apply disp_cell_unit_bicat_univalent_2_0; assumption.
- apply disp_cell_unit_bicat_univalent_2_1; assumption.
Defined.
End Disp_Prebicat_Cells_Unit.

Definition is_chaotic_disp_bicat_cells_unit
{C : bicat}
(D : disp_cat_data C)
: is_chaotic (disp_cell_unit_bicat D).
Proof.
intro ; intros.
apply iscontrunit.
Defined.

Definition disp_2cells_isaprop_cell_unit_bicat
{C : bicat}
(D : disp_cat_data C)
: disp_2cells_isaprop (disp_cell_unit_bicat D).
Proof.
intro; intros.
apply isapropifcontr.
apply (is_chaotic_disp_bicat_cells_unit D).
Qed.

Definition disp_locally_groupoid_cell_unit_bicat
{C : bicat}
(D : disp_cat_data C)
: disp_locally_groupoid (disp_cell_unit_bicat D).
Proof.
use make_disp_locally_groupoid.
- intro; intros; exact tt.
- exact (disp_2cells_isaprop_cell_unit_bicat D).
Qed.