(** Properties of morphisms are closed under invertible 2-cells Contents: 1. Equivalences are closed under invertible 2-cells 2. Adjoint quivalences are closed under invertible 2-cells 3. Faithful 1-cells are closed under invertible 2-cells 4. Fully faithful 1-cells are closed under invertible 2-cells 5. Conservative 1-cells are closed under invertible 2-cells 6. Discrete 1-cells are closed under invertible 2-cells 7. Pseudomonic 1-cells are closed under invertible 2-cells 8. Internal Street fibrations are closed under invertible 2-cells 9. Adjunctions are closed under invertible 2-cells *) 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.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.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. Local Open Scope cat. (** 1. Equivalences are closed under invertible 2-cells *) Definition left_equivalence_invertible {B : bicat} {a b : B} {f g : a --> b} (g_equiv : left_equivalence g) {α : f ==> g} (Hα : is_invertible_2cell α) : left_equivalence f. Proof. simple refine ((_ ,, (_ ,, _)) ,, (_ ,, _)). - exact (left_adjoint_right_adjoint g_equiv). - exact ((left_adjoint_unit g_equiv) • ((Hα^-1) ▹ left_adjoint_right_adjoint g_equiv)). - exact ((left_adjoint_right_adjoint g_equiv ◃ α) • (left_adjoint_counit g_equiv)). - cbn. is_iso. apply g_equiv. - cbn. is_iso. apply g_equiv. Defined. (** 2. Adjoint quivalences are closed under invertible 2-cells *) Definition left_adjoint_equivalence_invertible {B : bicat} {a b : B} {f g : a --> b} (g_equiv : left_adjoint_equivalence g) {α : f ==> g} (Hα : is_invertible_2cell α) : left_adjoint_equivalence f. Proof. use equiv_to_adjequiv. exact (left_equivalence_invertible g_equiv Hα). Defined. (** 3. Faithful 1-cells are closed under invertible 2-cells *) Definition faithful_invertible {B : bicat} {a b : B} {f₁ f₂ : a --> b} (β : f₁ ==> f₂) (Hβ : is_invertible_2cell β) : faithful_1cell f₁ → faithful_1cell f₂. Proof. intros Hf₁ z g₁ g₂ α₁ α₂ p. apply (faithful_1cell_eq_cell Hf₁). use (vcomp_rcancel (_ ◃ β)). { is_iso. } rewrite !vcomp_whisker. rewrite p. apply idpath. Qed. (** 4. Fully faithful 1-cells are closed under invertible 2-cells *) Definition fully_faithful_invertible {B : bicat} {a b : B} {f₁ f₂ : a --> b} (β : f₁ ==> f₂) (Hβ : is_invertible_2cell β) (Hf₁ : fully_faithful_1cell f₁) : fully_faithful_1cell f₂. Proof. use make_fully_faithful. - exact (faithful_invertible β Hβ (fully_faithful_1cell_faithful Hf₁)). - intros z g₁ g₂ αf. simple refine (_ ,, _). + apply (fully_faithful_1cell_inv_map Hf₁). exact ((g₁ ◃ β) • αf • (g₂ ◃ Hβ^-1)). + abstract (cbn ; use (vcomp_rcancel (_ ◃ Hβ^-1)) ; [ is_iso | ] ; rewrite vcomp_whisker ; rewrite fully_faithful_1cell_inv_map_eq ; rewrite !vassocr ; rewrite lwhisker_vcomp ; rewrite vcomp_linv ; rewrite lwhisker_id2 ; rewrite id2_left ; apply idpath). Qed. (** 5. Conservative 1-cells are closed under invertible 2-cells *) Definition conservative_invertible {B : bicat} {a b : B} {f₁ f₂ : a --> b} (β : f₁ ==> f₂) (Hβ : is_invertible_2cell β) (Hf₁ : conservative_1cell f₁) : conservative_1cell f₂. Proof. intros x g₁ g₂ α Hα. apply Hf₁. use eq_is_invertible_2cell. - exact ((g₁ ◃ β) • (α ▹ f₂) • (g₂ ◃ Hβ^-1)). - abstract (rewrite <- vcomp_whisker ; rewrite !vassocl ; rewrite lwhisker_vcomp ; rewrite vcomp_rinv ; rewrite lwhisker_id2 ; apply id2_right). - use is_invertible_2cell_vcomp. + use is_invertible_2cell_vcomp. * is_iso. * exact Hα. + is_iso. Defined. (** 6. Discrete 1-cells are closed under invertible 2-cells *) Definition discrete_invertible {B : bicat} {a b : B} {f₁ f₂ : a --> b} (β : f₁ ==> f₂) (Hβ : is_invertible_2cell β) (Hf₁ : discrete_1cell f₁) : discrete_1cell f₂. Proof. split. - exact (faithful_invertible β Hβ (pr1 Hf₁)). - exact (conservative_invertible β Hβ (pr2 Hf₁)). Defined. (** 7. Pseudomonic 1-cells are closed under invertible 2-cells *) Definition pseudomonic_invertible {B : bicat} {a b : B} {f₁ f₂ : a --> b} (β : f₁ ==> f₂) (Hβ : is_invertible_2cell β) (Hf₁ : pseudomonic_1cell f₁) : pseudomonic_1cell f₂. Proof. use make_pseudomonic. - apply (faithful_invertible β Hβ). apply pseudomonic_1cell_faithful. exact Hf₁. - intros z g₁ g₂ αf Hαf. simple refine (_ ,, _ ,, _). + refine (pseudomonic_1cell_inv_map Hf₁ ((_ ◃ β) • αf • (_ ◃ Hβ^-1)) _). is_iso. + apply is_invertible_2cell_pseudomonic_1cell_inv_map. + abstract (simpl ; use (vcomp_lcancel (_ ◃ β)) ; [ is_iso | ] ; rewrite <- vcomp_whisker ; rewrite pseudomonic_1cell_inv_map_eq ; rewrite !vassocl ; rewrite lwhisker_vcomp ; rewrite vcomp_linv ; rewrite lwhisker_id2 ; rewrite id2_right ; apply idpath). Defined. (** 8. Internal Street fibrations are closed under invertible 2-cells *) Section Cartesian2CellInvertible. Context {B : bicat} {a b : B} {f₁ f₂ : a --> b} (β : f₁ ==> f₂) (Hβ : is_invertible_2cell β) {x : B} {g₁ g₂ : x --> a} {α : g₁ ==> g₂} (Hα : is_cartesian_2cell_sfib f₁ α). Definition is_cartesian_2cell_invertible_unique {h : x --> a} {γ : h ==> g₂} {δp : h · f₂ ==> g₁ · f₂} (q : γ ▹ f₂ = δp • (α ▹ f₂)) : isaprop (∑ (δ : h ==> g₁), δ ▹ f₂ = δp × δ • α = γ). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ]. use (is_cartesian_2cell_sfib_factor_unique _ Hα _ γ ((h ◃ β) • δp • (_ ◃ Hβ^-1))). - rewrite !vassocl. rewrite <- vcomp_whisker. rewrite !vassocr. use vcomp_move_L_Mp ; [ is_iso | ]. cbn. rewrite !vassocl. rewrite vcomp_whisker. apply maponpaths. exact q. - use vcomp_move_L_Mp ; [ is_iso | ] ; cbn. rewrite vcomp_whisker. rewrite (pr12 φ₁). apply idpath. - use vcomp_move_L_Mp ; [ is_iso | ] ; cbn. rewrite vcomp_whisker. rewrite (pr12 φ₂). apply idpath. - apply (pr22 φ₁). - apply (pr22 φ₂). Qed. Definition is_cartesian_2cell_invertible : is_cartesian_2cell_sfib f₂ α. Proof. intros h γ δp q. use iscontraprop1. - exact (is_cartesian_2cell_invertible_unique q). - simple refine (_ ,, _ ,, _). + refine (is_cartesian_2cell_sfib_factor _ Hα γ ((h ◃ β) • δp • (_ ◃ Hβ^-1)) _). abstract (rewrite !vassocl ; rewrite <- vcomp_whisker ; rewrite !vassocr ; use vcomp_move_L_Mp ; [ is_iso | ] ; cbn ; rewrite !vassocl ; rewrite vcomp_whisker ; apply maponpaths ; exact q). + abstract (use (vcomp_rcancel (_ ◃ Hβ^-1)) ; [ is_iso | ] ; rewrite vcomp_whisker ; rewrite is_cartesian_2cell_sfib_factor_over ; rewrite !vassocr ; rewrite lwhisker_vcomp ; rewrite vcomp_linv ; rewrite lwhisker_id2 ; rewrite id2_left ; apply idpath). + abstract (cbn ; apply is_cartesian_2cell_sfib_factor_comm). Defined. End Cartesian2CellInvertible. Section InvertibleFromInternalSFib. Context {B : bicat} {a b : B} {f₁ f₂ : a --> b} (β : f₁ ==> f₂) (Hβ : is_invertible_2cell β) (Hf₁ : internal_sfib f₁). Definition internal_sfib_cleaving_invertible : internal_sfib_cleaving f₂. Proof. intros x g₁ g₂ α. pose (ℓ := pr1 Hf₁ x g₁ g₂ (α • (g₂ ◃ Hβ^-1))). simple refine (_ ,, _ ,, _ ,, _ ,, _). - exact (pr1 ℓ). - exact (pr12 ℓ). - exact (comp_of_invertible_2cell (lwhisker_of_invertible_2cell _ (inv_of_invertible_2cell (β ,, Hβ))) (pr122 ℓ)). - apply (is_cartesian_2cell_invertible β Hβ). exact (pr1 (pr222 ℓ)). - abstract (simpl ; rewrite !vassocl ; use vcomp_move_L_pM ; [ is_iso | ] ; cbn ; rewrite <- vcomp_whisker ; use vcomp_move_R_Mp ; [ is_iso ; apply Hβ | ] ; cbn ; rewrite !vassocl ; exact (pr2 (pr222 ℓ))). Defined. Definition lwhisker_is_cartesian_invertible : lwhisker_is_cartesian f₂. Proof. intros x y h g₁ g₂ γ Hγ. apply (is_cartesian_2cell_invertible β Hβ). apply (pr2 Hf₁). apply (is_cartesian_2cell_invertible _ (is_invertible_2cell_inv Hβ)). exact Hγ. Defined. Definition internal_sfib_invertible : internal_sfib f₂. Proof. split. - exact internal_sfib_cleaving_invertible. - exact lwhisker_is_cartesian_invertible. Defined. End InvertibleFromInternalSFib. (** 9. Adjunctions are closed under invertible 2-cells *) Section AdjunctionInvertible. Context {B : bicat} {x y : B} {l l' : x --> y} (α : invertible_2cell l l') (Hl : left_adjoint l). Let r : y --> x := left_adjoint_right_adjoint Hl. Let η : id₁ x ==> l · r := left_adjoint_unit Hl. Let ε : r · l ==> id₁ y := left_adjoint_counit Hl. Let trl : linvunitor _ • (η ▹ _) • rassociator _ _ _ • (_ ◃ ε) • runitor _ = id₂ _ := pr12 Hl. Let trr : rinvunitor _ • (_ ◃ η) • lassociator _ _ _ • (ε ▹ _) • lunitor _ = id₂ _ := pr22 Hl. Definition left_adjoint_data_invertible : left_adjoint_data l' := r ,, (η • (α ▹ r) ,, (_ ◃ α^-1) • ε). Definition left_adjoint_axioms_invertible : left_adjoint_axioms left_adjoint_data_invertible. Proof. split ; cbn. - rewrite <- !lwhisker_vcomp. rewrite <- !rwhisker_vcomp. rewrite !vassocl. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker_alt. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. rewrite vcomp_runitor. apply idpath. } etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite lwhisker_lwhisker_rassociator. apply idpath. } rewrite !vassocl. etrans. { apply maponpaths. rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. apply idpath. } etrans. { rewrite !vassocr. rewrite lwhisker_hcomp. rewrite <- linvunitor_natural. rewrite !vassocl. apply idpath. } use vcomp_move_R_pM ; [ is_iso | ]. cbn. rewrite id2_right. refine (_ @ id2_left _). rewrite !vassocr. apply maponpaths_2. exact trl. - rewrite <- !lwhisker_vcomp. rewrite <- !rwhisker_vcomp. rewrite !vassocl. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite rwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite lwhisker_vcomp. rewrite vcomp_rinv. rewrite lwhisker_id2. rewrite id2_rwhisker. rewrite id2_left. apply idpath. } rewrite !vassocr. exact trr. Qed. Definition left_adjoint_invertible : left_adjoint l' := left_adjoint_data_invertible ,, left_adjoint_axioms_invertible. End AdjunctionInvertible.