Definition pseudomonic_is_conservative {B : bicat} {a b : B} {f : a --> b} (Hf : pseudomonic_1cell f) : conservative_1cell f. Proof. intros x g₁ g₂ α Hα. pose (H := is_invertible_2cell_pseudomonic_1cell_inv_map Hf (α ▹ f) Hα). use make_is_invertible_2cell. - exact (H^-1). - abstract (use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite id2_left ; apply (pseudomonic_1cell_faithful Hf) ; exact (!(pseudomonic_1cell_inv_map_eq Hf (α ▹ f) Hα))). - abstract (use vcomp_move_R_pM ; [ is_iso | ] ; cbn ; rewrite id2_right ; apply (pseudomonic_1cell_faithful Hf) ; exact (!(pseudomonic_1cell_inv_map_eq Hf (α ▹ f) Hα))). Defined.
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. Require Import UniMath.Bicategories.Morphisms.FullyFaithful.