Library UniMath.Bicategories.Morphisms.FullyFaithful

Faithful and fully faithful 1-cells in bicategories
Contents: 1. Definition of faithful 1-cells 2. Characterization of faithful 1-cells 3. Fully faithful 1-cells 4. Characterization of fully faithful 1-cells 5. Pseudomonic 1-cells 6. Characterization of pseudomonic 1-cells 7. Pseudomonic 1-cells in locally groupoidal bicategories
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.

Local Open Scope cat.

1. Definition of faithful 1-cells
Definition faithful_1cell
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : UU
  := ∏ (z : B)
       (g₁ g₂ : z --> a)
       (α₁ α₂ : g₁ ==> g₂),
     α₁ ▹ f = α₂ ▹ f
     →
     α₁ = α₂.

Definition faithful_1cell_eq_cell
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf : faithful_1cell f)
           {z : B}
           {g₁ g₂ : z --> a}
           {α₁ α₂ : g₁ ==> g₂}
           (p : α₁ ▹ f = α₂ ▹ f)
  : α₁ = α₂
  := Hf _ _ _ _ _ p.

Definition isaprop_faithful_1cell
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : isaprop (faithful_1cell f).
Show proof.
  repeat (use impred ; intro).
  apply cellset_property.

2. Characterization of faithful 1-cells
Definition faithful_1cell_to_faithful
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : faithful_1cell f → ∏ (z : B), faithful (post_comp z f).
Show proof.
  intros Hf z g₁ g₂ α ; cbn in *.
  use invproofirrelevance.
  intros φ₁ φ₂ ; cbn in *.
  use subtypePath.
  {
    intro ; apply cellset_property.
  }
  apply (faithful_1cell_eq_cell Hf).
  exact (pr2 φ₁ @ !(pr2 φ₂)).

Definition faithful_to_faithful_1cell
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : (∏ (z : B), faithful (post_comp z f)) → faithful_1cell f.
Show proof.
  intros Hf z g₁ g₂ α₁ α₂ p.
  pose (proofirrelevance _ (Hf z g₁ g₂ (α₂ ▹ f)) (α₁ ,, p) (α₂ ,, idpath _)) as q.
  exact (maponpaths pr1 q).

Definition faithful_1cell_weq_faithful
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : (faithful_1cell f) ≃ (∏ (z : B), faithful (post_comp z f)).
Show proof.
  use weqimplimpl.
  - exact (faithful_1cell_to_faithful f).
  - exact (faithful_to_faithful_1cell f).
  - exact (isaprop_faithful_1cell f).
  - use impred ; intro.
    apply isaprop_faithful.

3. Fully faithful 1-cells
Definition fully_faithful_1cell
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : UU
  := (∏ (z : B)
        (g₁ g₂ : z --> a)
        (α₁ α₂ : g₁ ==> g₂),
      α₁ ▹ f = α₂ ▹ f
      →
      α₁ = α₂)
     ×
     (∏ (z : B)
        (g₁ g₂ : z --> a)
        (αf : g₁ · f ==> g₂ · f),
      ∑ (α : g₁ ==> g₂), α ▹ f = αf).

Definition fully_faithful_1cell_faithful
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf : fully_faithful_1cell f)
  : faithful_1cell f
  := pr1 Hf.

Definition fully_faithful_1cell_eq
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf : fully_faithful_1cell f)
           {z : B}
           {g₁ g₂ : z --> a}
           {α₁ α₂ : g₁ ==> g₂}
           (p : α₁ ▹ f = α₂ ▹ f)
  : α₁ = α₂
  := pr1 Hf _ _ _ _ _ p.

Definition fully_faithful_1cell_inv_map
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf : fully_faithful_1cell f)
           {z : B}
           {g₁ g₂ : z --> a}
           (αf : g₁ · f ==> g₂ · f)
  : g₁ ==> g₂
  := pr1 (pr2 Hf _ _ _ αf).

Definition fully_faithful_1cell_inv_map_eq
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf : fully_faithful_1cell f)
           {z : B}
           {g₁ g₂ : z --> a}
           (αf : g₁ · f ==> g₂ · f)
  : fully_faithful_1cell_inv_map Hf αf ▹ f = αf
  := pr2 (pr2 Hf _ _ _ αf).

Definition make_fully_faithful
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf₁ : faithful_1cell f)
           (Hf₂ : ∏ (z : B)
                    (g₁ g₂ : z --> a)
                    (αf : g₁ · f ==> g₂ · f),
                  ∑ (α : g₁ ==> g₂), α ▹ f = αf)
  : fully_faithful_1cell f
  := (Hf₁ ,, Hf₂).

Definition isaprop_fully_faithful_1cell
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : isaprop (fully_faithful_1cell f).
Show proof.
  use invproofirrelevance.
  intros φ₁ φ₂.
  use pathsdirprod.
  - apply isaprop_faithful_1cell.
  - use funextsec ; intro z.
    use funextsec ; intro g₁.
    use funextsec ; intro g₂.
    use funextsec ; intro αf.
    use subtypePath.
    {
      intro ; apply cellset_property.
    }
    pose (ψ₁ := pr2 φ₁ z g₁ g₂ αf).
    pose (ψ₂ := pr2 φ₂ z g₁ g₂ αf).
    enough (pr1 ψ₁ = pr1 ψ₂) as X.
    {
      exact X.
    }
    use (fully_faithful_1cell_eq φ₁).
    exact (pr2 ψ₁ @ !(pr2 ψ₂)).

4. Characterizations of fully faithful 1-cells
Definition fully_faithful_1cell_to_fully_faithful
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : fully_faithful_1cell f → ∏ (z : B), fully_faithful (post_comp z f).
Show proof.
  intros Hf z g₁ g₂ α ; cbn in *.
  use iscontraprop1.
  - use invproofirrelevance.
    intros φ₁ φ₂.
    use subtypePath ; [ intro ; apply cellset_property | ].
    cbn in *.
    apply (pr1 Hf).
    exact (pr2 φ₁ @ !(pr2 φ₂)).
  - exact (pr2 Hf z _ _ α).

Definition fully_faithful_to_fully_faithful_1cell
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : (∏ (z : B), fully_faithful (post_comp z f)) → fully_faithful_1cell f.
Show proof.
  intros Hf.
  use make_fully_faithful.
  - use faithful_to_faithful_1cell.
    intro z.
    apply fully_faithful_implies_full_and_faithful.
    apply Hf.
  - intros z g₁ g₂ αf.
    simple refine (_ ,, _).
    + exact (invmap (make_weq _ (Hf z g₁ g₂)) αf).
    + apply (homotweqinvweq (make_weq _ (Hf z g₁ g₂))).

Definition fully_faithful_1cell_weq_fully_faithful
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : (fully_faithful_1cell f)
    ≃
    (∏ (z : B), fully_faithful (post_comp z f)).
Show proof.
  use weqimplimpl.
  - exact (fully_faithful_1cell_to_fully_faithful f).
  - exact (fully_faithful_to_fully_faithful_1cell f).
  - exact (isaprop_fully_faithful_1cell f).
  - use impred ; intro.
    apply isaprop_fully_faithful.

5. Pseudomonic 1-cells
Definition pseudomonic_1cell
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : UU
  := (∏ (z : B)
        (g₁ g₂ : z --> a)
        (α₁ α₂ : g₁ ==> g₂),
      α₁ ▹ f = α₂ ▹ f
      →
      α₁ = α₂)
     ×
     (∏ (z : B)
        (g₁ g₂ : z --> a)
        (αf : g₁ · f ==> g₂ · f)
        (Hαf : is_invertible_2cell αf),
      ∑ (α : g₁ ==> g₂), is_invertible_2cell α × α ▹ f = αf).

Definition pseudomonic_1cell_faithful
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf : pseudomonic_1cell f)
  : faithful_1cell f
  := pr1 Hf.

Definition pseudomonic_1cell_eq
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf : pseudomonic_1cell f)
           {z : B}
           {g₁ g₂ : z --> a}
           {α₁ α₂ : g₁ ==> g₂}
           (p : α₁ ▹ f = α₂ ▹ f)
  : α₁ = α₂
  := pr1 Hf _ _ _ _ _ p.

Definition pseudomonic_1cell_inv_map
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf : pseudomonic_1cell f)
           {z : B}
           {g₁ g₂ : z --> a}
           (αf : g₁ · f ==> g₂ · f)
           (Hαf : is_invertible_2cell αf)
  : g₁ ==> g₂
  := pr1 (pr2 Hf _ _ _ αf Hαf).

Definition is_invertible_2cell_pseudomonic_1cell_inv_map
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf : pseudomonic_1cell f)
           {z : B}
           {g₁ g₂ : z --> a}
           (αf : g₁ · f ==> g₂ · f)
           (Hαf : is_invertible_2cell αf)
  : is_invertible_2cell (pseudomonic_1cell_inv_map Hf αf Hαf)
  := pr12 (pr2 Hf _ _ _ αf Hαf).

Definition pseudomonic_1cell_inv_map_eq
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf : pseudomonic_1cell f)
           {z : B}
           {g₁ g₂ : z --> a}
           (αf : g₁ · f ==> g₂ · f)
           (Hαf : is_invertible_2cell αf)
  : pseudomonic_1cell_inv_map Hf αf Hαf ▹ f = αf
  := pr22 (pr2 Hf _ _ _ αf Hαf).

Definition make_pseudomonic
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf₁ : faithful_1cell f)
           (Hf₂ : ∏ (z : B)
                    (g₁ g₂ : z --> a)
                    (αf : g₁ · f ==> g₂ · f)
                    (Hαf : is_invertible_2cell αf),
                  ∑ (α : g₁ ==> g₂),
                  is_invertible_2cell α × α ▹ f = αf)
  : pseudomonic_1cell f
  := (Hf₁ ,, Hf₂).

Definition isaprop_pseudomonic_1cell
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : isaprop (pseudomonic_1cell f).
Show proof.
  use invproofirrelevance.
  intros φ₁ φ₂.
  use pathsdirprod.
  - apply isaprop_faithful_1cell.
  - use funextsec ; intro z.
    use funextsec ; intro g₁.
    use funextsec ; intro g₂.
    use funextsec ; intro αf.
    use funextsec ; intro Hαf.
    use subtypePath.
    {
      intro.
      apply isapropdirprod.
      + apply isaprop_is_invertible_2cell.
      + apply cellset_property.
    }
    pose (ψ₁ := pr2 φ₁ z g₁ g₂ αf Hαf).
    pose (ψ₂ := pr2 φ₂ z g₁ g₂ αf Hαf).
    enough (pr1 ψ₁ = pr1 ψ₂) as X.
    {
      exact X.
    }
    use (pseudomonic_1cell_eq φ₁).
    exact (pr22 ψ₁ @ !(pr22 ψ₂)).

6. Characterization of pseudomonic 1-cells
Definition pseudomonic_1cell_to_pseudomonic
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : pseudomonic_1cell f → ∏ (z : B), pseudomonic (post_comp z f).
Show proof.
  intros Hf z.
  split.
  - apply faithful_1cell_to_faithful.
    exact (pr1 Hf).
  - intros g₁ g₂ α.
    apply hinhpr.
    simple refine (_ ,, _) ; cbn.
    + apply inv2cell_to_z_iso.
      use make_invertible_2cell.
      * use (pseudomonic_1cell_inv_map Hf (z_iso_to_inv2cell α)).
        apply property_from_invertible_2cell.
      * apply is_invertible_2cell_pseudomonic_1cell_inv_map.
    + use subtypePath ; [ intro ; apply (isaprop_is_z_isomorphism(C:=hom z b)) | ].
      cbn.
      apply pseudomonic_1cell_inv_map_eq.

Definition pseudomonic_to_pseudomonic_1cell
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : (∏ (z : B), pseudomonic (post_comp z f)) → pseudomonic_1cell f.
Show proof.
  intro H.
  use make_pseudomonic.
  - apply faithful_to_faithful_1cell.
    intro z.
    apply H.
  - intros z g₁ g₂ αf Hαf.
    pose (w := make_weq _ (isweq_functor_on_iso_pseudomonic (H z) g₁ g₂)).
    simple refine (_ ,, _ ,, _).
    + apply (invweq w).
      use inv2cell_to_z_iso.
      exact (αf ,, Hαf).
    + cbn.
      apply is_z_iso_to_is_inv2cell.
      apply (pr2 (invmap w (inv2cell_to_z_iso (αf,, Hαf)))).
    + exact (maponpaths
               pr1
               (homotweqinvweq w (inv2cell_to_z_iso (αf,, Hαf)))).

Definition pseudomonic_1cell_weq_pseudomonic
           {B : bicat}
           {a b : B}
           (f : a --> b)
  : (pseudomonic_1cell f)
    ≃
    (∏ (z : B), pseudomonic (post_comp z f)).
Show proof.
  use weqimplimpl.
  - exact (pseudomonic_1cell_to_pseudomonic f).
  - exact (pseudomonic_to_pseudomonic_1cell f).
  - exact (isaprop_pseudomonic_1cell f).
  - use impred ; intro.
    apply isaprop_pseudomonic.

7. Pseudomonic 1-cells in locally groupoidal bicategories
Definition fully_faithful_is_pseudomonic
           {B : bicat}
           {a b : B}
           {f : a --> b}
           (Hf : fully_faithful_1cell f)
  : pseudomonic_1cell f.
Show proof.
  use make_pseudomonic.
  - exact (fully_faithful_1cell_faithful Hf).
  - intros z g₁ g₂ αf ?.
    refine (fully_faithful_1cell_inv_map Hf αf ,, _ ,, _).
    + use make_is_invertible_2cell.
      * exact (fully_faithful_1cell_inv_map Hf (Hαf^-1)).
      * abstract
          (use (fully_faithful_1cell_faithful Hf) ;
           rewrite <- rwhisker_vcomp ;
           rewrite !fully_faithful_1cell_inv_map_eq ;
           rewrite id2_rwhisker ;
           apply vcomp_rinv).
      * abstract
          (use (fully_faithful_1cell_faithful Hf) ;
           rewrite <- rwhisker_vcomp ;
           rewrite !fully_faithful_1cell_inv_map_eq ;
           rewrite id2_rwhisker ;
           apply vcomp_linv).
    + exact (fully_faithful_1cell_inv_map_eq Hf αf).

Definition pseudomonic_is_fully_faithful_locally_grpd
           {B : bicat}
           (inv_B : locally_groupoid B)
           {a b : B}
           {f : a --> b}
           (Hf : pseudomonic_1cell f)
  : fully_faithful_1cell f.
Show proof.
  use make_fully_faithful.
  - exact (pr1 Hf).
  - intros z g₁ g₂ αf.
    simple refine (_ ,, _).
    + use (pseudomonic_1cell_inv_map Hf αf).
      apply inv_B.
    + apply (pseudomonic_1cell_inv_map_eq Hf).

Definition pseudomonic_weq_fully_faithful_locally_grpd
           {B : bicat}
           (inv_B : locally_groupoid B)
           {a b : B}
           (f : a --> b)
  : pseudomonic_1cell f ≃ fully_faithful_1cell f.
Show proof.
  use weqimplimpl.
  - exact (pseudomonic_is_fully_faithful_locally_grpd inv_B).
  - exact fully_faithful_is_pseudomonic.
  - apply isaprop_pseudomonic_1cell.
  - apply isaprop_fully_faithful_1cell.