Library UniMath.CategoryTheory.Bicategories.Discreteness

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Bicat. Import Bicat.Notations.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Unitors.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.BicategoryLaws.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Adjunctions.

Local Open Scope cat.

Lemma is_z_isomorphism_weq_is_iso {C:category} {a b} (f : C⟦a,b⟧)
  : is_z_isomorphism f ≃ is_iso f.
Proof.
  apply weqimplimpl.
  - apply is_iso_from_is_z_iso.
  - apply is_z_iso_from_is_iso.
  - apply isaprop_is_z_isomorphism, C.
  - apply isaprop_is_iso.
Defined.

Definition idto2cell {C : prebicat_data} {a b} {f g : C⟦a,b⟧}
  : (f = g) → f ==> g
  := paths_rect (C ⟦ a, b ⟧)
                f
                (λ (g0 : C ⟦ a, b ⟧) (_ : f = g0), f ==> g0)
                (id₂ f)
                g.

Definition has_trivial_2cells (C : prebicat_data)
  : UU
  := ∏ a b (f g : C⟦a,b⟧), isweq (λ p : f = g, idto2cell p).

Definition has_trivial_2cells_equality {C : prebicat_data}
           (disc : has_trivial_2cells C)
           {a b} {f g : C⟦a,b⟧}
  : (f ==> g) → (f = g)
  := invmap (weqpair (λ p : f = g, idto2cell p) (disc a b f g)).

Definition is_discrete_bicategory (C : prebicat_data)
  : UU
  := (∏ a b (f g : C⟦a,b⟧), isaprop (f ==> g))
     × has_trivial_2cells C.

Definition is_discrete_bicategory_cellprop {C : prebicat_data}
           (disc : is_discrete_bicategory C)
  : (∏ a b (f g : C⟦a,b⟧), isaprop (f ==> g))
  := pr1 disc.

Coercion is_discrete_bicategory_trivial_2cells {C : prebicat_data}
         (disc : is_discrete_bicategory C)
  : has_trivial_2cells C
  := pr2 disc.

Lemma has_trivial_2cells_discrete_prebicat (C : category)
  : has_trivial_2cells (discrete_prebicat C).
Proof.
  intros a b f g.
  use weqhomot.
  - exact (idweq (f = g)).
  - intro e. induction e. apply idpath.
Qed.

Lemma is_discrete_discrete_bicategory (C : category)
  : is_discrete_bicategory (discrete_prebicat C).
Proof.
  split.
  - intros. cbn in a, b, f, g. apply homset_property.
  - apply has_trivial_2cells_discrete_prebicat.
Qed.

Definition precategory_of_discrete_bicategory {C : prebicat_data}
           (disc : is_discrete_bicategory C)
  : precategory.
Proof.
  use tpair.
  - exact C.
  - repeat split; intros; apply disc.
    + apply lunitor.
    + apply runitor.
    + apply lassociator.
    + apply rassociator.
Defined.

Lemma is_discrete_bicategory_has_homsets {C : prebicat_data}
      (disc : is_discrete_bicategory C)
  : has_homsets C.
Proof.
  intros a b f g.
  refine (isofhlevelweqb 1 _ _).
  - apply (weqpair idto2cell), disc.
  - apply (is_discrete_bicategory_cellprop disc).
Qed.

Definition category_of_discrete_bicategory {C : prebicat_data}
           (disc : is_discrete_bicategory C)
  : category.
Proof.
  use tpair.
  - exact (precategory_of_discrete_bicategory disc).
  - exact (is_discrete_bicategory_has_homsets disc).
Defined.

Lemma is_discrete_bicategory_iscontr_is_invertible_2cell {C : bicat}
      (disc : is_discrete_bicategory C)
      {a b : C} {f g : C ⟦ a, b ⟧}
      (x : f ==> g)
  : iscontr (is_invertible_2cell x).
Proof.
  induction (has_trivial_2cells_equality disc x).
  apply unique_exists with x.
  - split; apply (is_discrete_bicategory_cellprop disc).
  - intro. apply isapropdirprod; apply C.
  - intros. apply (is_discrete_bicategory_cellprop disc).
Qed.

Lemma is_adjointequivalence_discrete_weq_iso {C : bicat}
      (disc : is_discrete_bicategory C)
      {a b} (f : C⟦a,b⟧)
  : left_adjoint_equivalence f
    ≃
    is_iso (C := category_of_discrete_bicategory disc) f.
Proof.
  eapply weqcomp.
  2: apply is_z_isomorphism_weq_is_iso.
  unfold left_adjoint_equivalence, is_z_isomorphism.
  eapply weqcomp.
  { apply weqfibtototal. intro. apply weqdirprodcomm. }
  eapply weqcomp.
  { apply (weqtotal2asstol _
             (λ x : (∑ y : left_adjoint_data f, left_equivalence_axioms y),
               left_adjoint_axioms (pr1 x))). }
  eapply weqcomp.
  { apply weqpr1. induction z as [la le].
    apply (isofhleveldirprod 0); cbn; apply (is_discrete_bicategory_cellprop disc). }
  eapply weqcomp.
  { apply weqtotal2asstor. }
  apply weqfibtototal. intro g.
  unfold is_inverse_in_precat.
  eapply weqcomp.
  { apply weqpr1.
    induction z as [η ε].
    apply (isofhleveldirprod 0); cbn;
      apply (is_discrete_bicategory_iscontr_is_invertible_2cell disc). }
  apply weqdirprod.
  { eapply weqcomp. 2: apply weqpathsinv0.
    apply invweq.
    apply (weqpair _ (is_discrete_bicategory_trivial_2cells disc _ _ _ _)). }
  apply invweq.
  apply (weqpair _ (is_discrete_bicategory_trivial_2cells disc _ _ _ _)).
Defined.