Library UniMath.Bicategories.Modifications.Modification
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).
Show 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).
use vcomp_move_L_pM.
{ is_iso. }
rewrite vassocr.
use vcomp_move_R_Mp.
{ is_iso. }
exact (modnaturality_of m X Y f).
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'.
Show 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.
{ 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.
Definition isaset_modification
{B B' : bicat}
{F G : psfunctor B B'}
(σ τ : pstrans F G)
: isaset (modification σ τ).
Show 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.
- 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.
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.
Show proof.
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 σ τ.
Show proof.
intro X.
exact (m X).
exact (m X).
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).
Show 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).
use make_is_invertible_2cell.
- exact ((Hm^-1 : modification _ _) X).
- exact (modcomponent_eq (vcomp_rinv Hm) X).
- exact (modcomponent_eq (vcomp_linv Hm) X).
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.
Show 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)).
- 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)).
Definition invertible_modcomponent_of
{B B' : bicat}
{F G : psfunctor B B'}
{σ τ : pstrans F G}
(m : invertible_modification σ τ)
: ∏ (X : B), invertible_2cell (σ X) (τ X).
Show 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).
use make_invertible_2cell.
- exact ((cell_from_invertible_2cell m : modification _ _) X).
- apply is_invertible_modcomponent_of.
exact (property_from_invertible_2cell m).
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 σ τ.
Show proof.
use make_invertible_2cell.
- use make_modification.
+ unfold modification_data.
apply m.
+ exact Hm.
- apply make_is_invertible_modification.
intro.
apply m.
- use make_modification.
+ unfold modification_data.
apply m.
+ exact Hm.
- apply make_is_invertible_modification.
intro.
apply m.
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 σ τ.
Show proof.
{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 σ τ.
Show proof.