Library UniMath.Bicategories.Morphisms.Examples.MorphismsInOp2Bicat

Morphisms in op2 bicat
Contents 1. Faithful 1-cells 2. Fully faithful 1-cells 3. Conservative 1-cells 4. Discrete 1-cells 5. Adjunctions
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.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.Core.EquivToAdjequiv.
Require Import UniMath.Bicategories.Core.Examples.OpCellBicat.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Morphisms.FullyFaithful.
Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms.

Local Open Scope cat.

1. Faithful 1-cells
Definition faithful_op2_bicat
           {B : bicat}
           {x y : B}
           {f : x --> y}
           (Hf : faithful_1cell f)
  : @faithful_1cell (op2_bicat B) _ _ f.
Show proof.
  intros z g₁ g₂ α β p.
  apply Hf.
  exact p.

2. Fully faithful 1-cells
Definition fully_faithful_op2_bicat
           {B : bicat}
           {x y : B}
           {f : x --> y}
           (Hf : fully_faithful_1cell f)
  : @fully_faithful_1cell (op2_bicat B) _ _ f.
Show proof.
  use make_fully_faithful.
  - apply faithful_op2_bicat.
    apply fully_faithful_1cell_faithful.
    exact Hf.
  - intros z g₁ g₂ αf.
    simple refine (_ ,, _).
    + exact (fully_faithful_1cell_inv_map Hf αf).
    + cbn.
      apply fully_faithful_1cell_inv_map_eq.

3. Conservative 1-cells
Definition conservative_op2_bicat
           {B : bicat}
           {x y : B}
           {f : x --> y}
           (Hf : conservative_1cell f)
  : @conservative_1cell (op2_bicat B) _ _ f.
Show proof.
  intros z g₁ g₂ α Hα.
  apply to_op2_is_invertible_2cell.
  apply Hf.
  apply from_op2_is_invertible_2cell.
  exact Hα.

4. Discrete 1-cells
Definition discrete_op2_bicat
           {B : bicat}
           {x y : B}
           {f : x --> y}
           (Hf : discrete_1cell f)
  : @discrete_1cell (op2_bicat B) _ _ f.
Show proof.
  split.
  - apply faithful_op2_bicat.
    apply Hf.
  - apply conservative_op2_bicat.
    apply Hf.

5. Adjunctions
Definition op2_left_adjoint_right_adjoint_is_left_adjoint
           {B : bicat}
           {x y : B}
           {f : x --> y}
           (Hf : @left_adjoint (op2_bicat B) _ _ f)
  : @left_adjoint B _ _ (left_adjoint_right_adjoint Hf).
Show proof.
  simple refine ((_ ,, (_ ,, _)) ,, (_ ,, _)).
  - exact f.
  - exact (left_adjoint_counit Hf).
  - exact (left_adjoint_unit Hf).
  - abstract
      (cbn ;
       rewrite !vassocl ;
       exact (internal_triangle2 Hf)).
  - abstract
      (cbn ;
       rewrite !vassocl ;
       exact (internal_triangle1 Hf)).

Definition op2_left_adjoint_to_right_adjoint
           {B : bicat}
           {x y : B}
           {f : x --> y}
           (Hf : @left_adjoint (op2_bicat B) _ _ f)
  : @internal_right_adj B _ _ f.
Show proof.
  simple refine ((_ ,, (_ ,, _)) ,, (_ ,, _)).
  - exact (left_adjoint_right_adjoint Hf).
  - exact (left_adjoint_counit Hf).
  - exact (left_adjoint_unit Hf).
  - abstract
      (cbn ;
       rewrite !vassocl ;
       exact (internal_triangle2 Hf)).
  - abstract
      (cbn ;
       rewrite !vassocl ;
       exact (internal_triangle1 Hf)).

Definition right_adjoint_to_op2_left_adjoint
           {B : bicat}
           {x y : B}
           {f : x --> y}
           (Hf : @internal_right_adj B _ _ f)
  : @left_adjoint (op2_bicat B) _ _ f.
Show proof.
  simple refine ((_ ,, (_ ,, _)) ,, (_ ,, _)).
  - exact (internal_right_adj_left_adjoint Hf).
  - exact (internal_right_adj_counit Hf).
  - exact (internal_right_adj_unit Hf).
  - abstract
      (cbn ;
       rewrite !vassocr ;
       exact (pr22 Hf)).
  - abstract
      (cbn ;
       rewrite !vassocr ;
       exact (pr12 Hf)).

Definition op2_left_adjoint_weq_right_adjoint
           {B : bicat}
           {x y : B}
           (f : x --> y)
  : @left_adjoint (op2_bicat B) _ _ f ≃ @internal_right_adj B _ _ f.
Show proof.
  use make_weq.
  - exact op2_left_adjoint_to_right_adjoint.
  - use isweq_iso.
    + exact right_adjoint_to_op2_left_adjoint.
    + abstract
        (intro Hf ;
         use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ;
         apply idpath).
    + abstract
        (intro Hf ;
         use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ;
         apply idpath).