(* ******************************************************************************* *) (** * Modifications between pseudo transformations Niccolò Veltri, Niels van der Weide April 2019 ********************************************************************************* *) 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.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map2Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Identitor. Require Import UniMath.Bicategories.PseudoFunctors.Display.Compositor. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Local Open Scope cat. Definition modification {B B' : bicat} {F G : psfunctor B B'} (σ τ : pstrans F G) : UU := prebicat_cells (psfunctor_bicat B B') σ τ. Definition modification_data {B B' : bicat} {F G : psfunctor B B'} (σ τ : pstrans F G) : UU := ∏ (X : B), σ X ==> τ X. Definition is_modification {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : modification_data σ τ) : UU := ∏ (X Y : B) (f : X --> Y), psnaturality_of σ f • (m Y ▻ #F f) = #G f ◅ m X • psnaturality_of τ f. Definition modcomponent_of {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : modification σ τ) : ∏ (X : B), σ X ==> τ X := pr111 m. Coercion modcomponent_of : modification >-> Funclass. Definition modnaturality_of {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : modification σ τ) : is_modification m := pr211 m. Definition mod_inv_naturality_of {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : modification σ τ) : ∏ (X Y : B) (f : X --> Y), (m Y ▻ #F f) • (psnaturality_of τ f)^-1 = (psnaturality_of σ f)^-1 • (#G f ◅ m X). Proof. intros X Y f. use vcomp_move_L_pM. { is_iso. } rewrite vassocr. use vcomp_move_R_Mp. { is_iso. } exact (modnaturality_of m X Y f). Qed. Definition make_modification {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : modification_data σ τ) (Hm : is_modification m) : modification σ τ := (((m ,, Hm) ,, (tt ,, tt ,, tt)),, tt). Definition modification_eq {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} {m m' : modification σ τ} (p : ∏ (X : B), m X = m' X) : m = m'. Proof. use subtypePath. { intro. simpl. exact isapropunit. } use subtypePath. { intro. simpl. repeat (apply isapropdirprod) ; apply isapropunit. } use subtypePath. { intro. simpl. repeat (apply impred ; intro). apply B'. } use funextsec. exact p. Qed. Definition isaset_modification {B B' : bicat} {F G : psfunctor B B'} (σ τ : pstrans F G) : isaset (modification σ τ). Proof. repeat (apply isaset_total2). - apply impred_isaset ; intro. apply B'. - intro. repeat (apply impred_isaset ; intro). apply isasetaprop. apply B'. - intro ; simpl. repeat (apply isaset_dirprod) ; apply isasetunit. - intro ; apply isasetunit. Qed. Definition is_invertible_modification {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : modification σ τ) : UU := @is_invertible_2cell (psfunctor_bicat B B') _ _ _ _ m. Definition invertible_modification {B B' : bicat} {F G : psfunctor B B'} (σ τ : pstrans F G) : UU := @invertible_2cell (psfunctor_bicat B B') _ _ σ τ. Definition modcomponent_eq {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} {m m' : modification σ τ} (p : m = m') : ∏ (X : B), m X = m' X. Proof. intro X. induction p. apply idpath. Qed. Definition invertible_modification_data {B B' : bicat} {F G : psfunctor B B'} (σ τ : pstrans F G) : UU := ∏ (X : B), invertible_2cell (σ X) (τ X). Coercion invertible_modification_data_to_modification_data {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : invertible_modification_data σ τ) : modification_data σ τ. Proof. intro X. exact (m X). Defined. Definition is_invertible_modcomponent_of {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : modification σ τ) (Hm : is_invertible_modification m) : ∏ (X : B), is_invertible_2cell (m X). Proof. intro X. use make_is_invertible_2cell. - exact ((Hm^-1 : modification _ _) X). - exact (modcomponent_eq (vcomp_rinv Hm) X). - exact (modcomponent_eq (vcomp_linv Hm) X). Defined. Definition make_is_invertible_modification {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : modification σ τ) (Hm : ∏ (X : B), is_invertible_2cell (m X)) : is_invertible_modification m. Proof. use make_is_invertible_2cell. - use make_modification. + exact (λ X, (Hm X)^-1). + intros X Y f. simpl. use vcomp_move_R_Mp. { is_iso. } simpl. rewrite <- vassocr. use vcomp_move_L_pM. { is_iso. } symmetry. simpl. apply (modnaturality_of m). - use modification_eq. intro X. cbn. exact (vcomp_rinv (Hm X)). - use modification_eq. intro X. cbn. exact (vcomp_linv (Hm X)). Defined. Definition invertible_modcomponent_of {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : invertible_modification σ τ) : ∏ (X : B), invertible_2cell (σ X) (τ X). Proof. intro X. use make_invertible_2cell. - exact ((cell_from_invertible_2cell m : modification _ _) X). - apply is_invertible_modcomponent_of. exact (property_from_invertible_2cell m). Defined. Definition make_invertible_modification {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : invertible_modification_data σ τ) (Hm : is_modification m) : invertible_modification σ τ. Proof. use make_invertible_2cell. - use make_modification. + unfold modification_data. apply m. + exact Hm. - apply make_is_invertible_modification. intro. apply m. Defined. (** Only on data *) Definition invertible_modification_data_on_data {B B' : bicat} {F G : psfunctor_data B B'} (σ τ : pstrans_on_data F G) : UU := ∏ (X : B), invertible_2cell (pr11 σ X) (pr11 τ X). Definition invertible_modification_on_data_is_modification {B B' : bicat} {F G : psfunctor_data B B'} {σ τ : pstrans_on_data F G} (m : invertible_modification_data_on_data σ τ) : UU := ∏ (X Y : B) (f : X --> Y), pr21 σ _ _ f • (_ ◃ m Y) = (m X ▹ _) • pr21 τ _ _ f. Definition invertible_modification_on_data {B B' : bicat} {F G : psfunctor_data B B'} (σ τ : pstrans_on_data F G) : UU := ∑ (m : invertible_modification_data_on_data σ τ), invertible_modification_on_data_is_modification m. Definition make_invertible_modification_on_data {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : invertible_modification_on_data (pr1 σ) (pr1 τ)) : invertible_modification σ τ. Proof. use make_invertible_modification. - exact (pr1 m). - exact (pr2 m). Defined.