Library UniMath.Bicategories.PseudoFunctors.Representable
Representable pseudofunctor, pseudotransformation, and modifications
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.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Isos.
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.Core.Examples.OpMorBicat.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Transformations.PseudoTransformation.
Require Import UniMath.Bicategories.Modifications.Modification.
Local Open Scope bicategory_scope.
Local Open Scope cat.
Section RepresentableFunctor.
Context {C : bicat}.
Variable (C_is_univalent_2_1 : is_univalent_2_1 C).
Definition pspsh := psfunctor (op1_bicat C) bicat_of_univ_cats.
Definition representable_data_cat (X Y : C) : univalent_category
:= univ_hom C_is_univalent_2_1 Y X.
Definition representable_data_fun (X Y Z : C) (f : op1_bicat C ⟦ Y, Z ⟧)
: bicat_of_univ_cats ⟦ representable_data_cat X Y, representable_data_cat X Z ⟧.
Show proof.
simpl in f.
use make_functor.
- use make_functor_data.
+ intro g.
exact (f · g).
+ intros g h.
exact (lwhisker f).
- split.
+ exact (lwhisker_id2 f).
+ intros g h k η φ.
exact (! (lwhisker_vcomp f η φ)).
use make_functor.
- use make_functor_data.
+ intro g.
exact (f · g).
+ intros g h.
exact (lwhisker f).
- split.
+ exact (lwhisker_id2 f).
+ intros g h k η φ.
exact (! (lwhisker_vcomp f η φ)).
Definition representable_data_nat (X Y Z : C) (f g : op1_bicat C ⟦ Y, Z ⟧)
: f ==> g → representable_data_fun X Y Z f ==> representable_data_fun X Y Z g.
Show proof.
intro η.
use make_nat_trans.
- intro h.
exact (rwhisker h η).
- intros h k φ.
exact (! (@vcomp_whisker C Z Y X f g h k η φ)).
use make_nat_trans.
- intro h.
exact (rwhisker h η).
- intros h k φ.
exact (! (@vcomp_whisker C Z Y X f g h k η φ)).
Definition representable_data (X : C) : psfunctor_data (op1_bicat C) bicat_of_univ_cats.
Show proof.
use make_psfunctor_data.
- exact (representable_data_cat X).
- exact (representable_data_fun X).
- exact (representable_data_nat X).
- intro Y.
use make_nat_trans.
+ exact linvunitor.
+ abstract (intros f g η ;
simpl in * ;
rewrite lwhisker_hcomp ;
apply linvunitor_natural).
- intros Y Z W f g.
use make_nat_trans.
+ intro h. simpl.
cbn in *.
apply lassociator.
+ intros h k η.
simpl.
apply lwhisker_lwhisker.
- exact (representable_data_cat X).
- exact (representable_data_fun X).
- exact (representable_data_nat X).
- intro Y.
use make_nat_trans.
+ exact linvunitor.
+ abstract (intros f g η ;
simpl in * ;
rewrite lwhisker_hcomp ;
apply linvunitor_natural).
- intros Y Z W f g.
use make_nat_trans.
+ intro h. simpl.
cbn in *.
apply lassociator.
+ intros h k η.
simpl.
apply lwhisker_lwhisker.
Definition representable_laws (X : C) : psfunctor_laws (representable_data X).
Show proof.
repeat split; cbn.
- intros Y Z f.
use nat_trans_eq.
+ exact (pr2 C Z X).
+ intro g. cbn.
apply id2_rwhisker.
- intros Y Z f g h η φ.
use nat_trans_eq.
+ exact (pr2 C Z X).
+ intro k. cbn.
symmetry.
apply rwhisker_vcomp.
- intros Y Z f.
use nat_trans_eq.
+ exact (pr2 C Z X).
+ intro g. cbn.
rewrite <- vassocr.
rewrite runitor_rwhisker.
rewrite lwhisker_vcomp.
rewrite linvunitor_lunitor.
symmetry.
apply lwhisker_id2.
- intros Y Z f.
use nat_trans_eq.
+ exact (pr2 C Z X).
+ intro g. cbn.
rewrite linvunitor_assoc.
refine (!(_@ _)).
{
apply maponpaths_2.
rewrite <- vassocr.
rewrite rassociator_lassociator.
apply id2_right.
}
rewrite rwhisker_vcomp.
rewrite linvunitor_lunitor.
apply id2_rwhisker.
- intros Y Z W V f g h.
use nat_trans_eq.
+ exact (pr2 C V X).
+ intro k.
cbn in *.
rewrite id2_left.
pose (pentagon_2 k f g h) as p.
rewrite lwhisker_hcomp,rwhisker_hcomp.
rewrite <- vassocr.
exact (! p).
- intros Y Z W f g h η.
use nat_trans_eq.
+ exact (pr2 C W X).
+ intro k.
cbn in *.
apply rwhisker_rwhisker.
- intros Y Z W f g h η.
use nat_trans_eq.
+ exact (pr2 C W X).
+ intro k.
cbn in *.
symmetry.
apply rwhisker_lwhisker.
- intros Y Z f.
use nat_trans_eq.
+ exact (pr2 C Z X).
+ intro g. cbn.
apply id2_rwhisker.
- intros Y Z f g h η φ.
use nat_trans_eq.
+ exact (pr2 C Z X).
+ intro k. cbn.
symmetry.
apply rwhisker_vcomp.
- intros Y Z f.
use nat_trans_eq.
+ exact (pr2 C Z X).
+ intro g. cbn.
rewrite <- vassocr.
rewrite runitor_rwhisker.
rewrite lwhisker_vcomp.
rewrite linvunitor_lunitor.
symmetry.
apply lwhisker_id2.
- intros Y Z f.
use nat_trans_eq.
+ exact (pr2 C Z X).
+ intro g. cbn.
rewrite linvunitor_assoc.
refine (!(_@ _)).
{
apply maponpaths_2.
rewrite <- vassocr.
rewrite rassociator_lassociator.
apply id2_right.
}
rewrite rwhisker_vcomp.
rewrite linvunitor_lunitor.
apply id2_rwhisker.
- intros Y Z W V f g h.
use nat_trans_eq.
+ exact (pr2 C V X).
+ intro k.
cbn in *.
rewrite id2_left.
pose (pentagon_2 k f g h) as p.
rewrite lwhisker_hcomp,rwhisker_hcomp.
rewrite <- vassocr.
exact (! p).
- intros Y Z W f g h η.
use nat_trans_eq.
+ exact (pr2 C W X).
+ intro k.
cbn in *.
apply rwhisker_rwhisker.
- intros Y Z W f g h η.
use nat_trans_eq.
+ exact (pr2 C W X).
+ intro k.
cbn in *.
symmetry.
apply rwhisker_lwhisker.
Definition representable_invertible_cells (X : C) : invertible_cells (representable_data X).
Show proof.
split.
- intro Y.
use is_nat_z_iso_to_is_invertible_2cell.
intro f.
simpl.
apply is_inv2cell_to_is_z_iso.
is_iso.
- intros Y Z W f g.
use is_nat_z_iso_to_is_invertible_2cell.
intro h.
simpl.
apply is_inv2cell_to_is_z_iso.
is_iso.
- intro Y.
use is_nat_z_iso_to_is_invertible_2cell.
intro f.
simpl.
apply is_inv2cell_to_is_z_iso.
is_iso.
- intros Y Z W f g.
use is_nat_z_iso_to_is_invertible_2cell.
intro h.
simpl.
apply is_inv2cell_to_is_z_iso.
is_iso.
Definition representable (X : C) : pspsh.
Show proof.
use make_psfunctor.
- exact (representable_data X).
- exact (representable_laws X).
- exact (representable_invertible_cells X).
- exact (representable_data X).
- exact (representable_laws X).
- exact (representable_invertible_cells X).
End RepresentableFunctor.
Section RepresentableTransformation.
Context {C : bicat}{X Y : C}.
Variable (C_is_univalent_2_1 : is_univalent_2_1 C) (f : X --> Y).
Definition representable1_data :
pstrans_data (representable C_is_univalent_2_1 X) (representable C_is_univalent_2_1 Y).
Show proof.
use make_pstrans_data.
- intro Z.
cbn.
use make_functor.
+ use make_functor_data.
-- intro g.
exact (g · f).
-- intros g h η.
exact (rwhisker f η).
+ split.
-- intro g.
apply id2_rwhisker.
-- intros g h k η φ.
symmetry.
apply rwhisker_vcomp.
- intros Z W h.
cbn.
use make_invertible_2cell.
+ use make_nat_trans.
-- intro k.
apply lassociator.
-- intros k l η.
cbn in *.
apply rwhisker_lwhisker.
+ use is_nat_z_iso_to_is_invertible_2cell.
intro g.
apply is_inv2cell_to_is_z_iso.
simpl.
is_iso.
- intro Z.
cbn.
use make_functor.
+ use make_functor_data.
-- intro g.
exact (g · f).
-- intros g h η.
exact (rwhisker f η).
+ split.
-- intro g.
apply id2_rwhisker.
-- intros g h k η φ.
symmetry.
apply rwhisker_vcomp.
- intros Z W h.
cbn.
use make_invertible_2cell.
+ use make_nat_trans.
-- intro k.
apply lassociator.
-- intros k l η.
cbn in *.
apply rwhisker_lwhisker.
+ use is_nat_z_iso_to_is_invertible_2cell.
intro g.
apply is_inv2cell_to_is_z_iso.
simpl.
is_iso.
Definition representable1_is_pstrans : is_pstrans representable1_data.
Show proof.
repeat (apply tpair).
- intros Z W g h η.
use nat_trans_eq.
{ exact (pr2 C W Y). }
intro k.
simpl.
symmetry.
apply rwhisker_rwhisker.
- intro Z.
use nat_trans_eq.
{ exact (pr2 C Z Y). }
intro h.
cbn in *.
rewrite !id2_left.
rewrite linvunitor_assoc.
rewrite <- vassocr.
rewrite rassociator_lassociator.
apply id2_right.
- intros Z W V g h.
use nat_trans_eq.
{ exact (pr2 C V Y). }
intro k.
cbn in *.
rewrite id2_left , ! id2_right.
symmetry.
apply lassociator_lassociator.
- intros Z W g h η.
use nat_trans_eq.
{ exact (pr2 C W Y). }
intro k.
simpl.
symmetry.
apply rwhisker_rwhisker.
- intro Z.
use nat_trans_eq.
{ exact (pr2 C Z Y). }
intro h.
cbn in *.
rewrite !id2_left.
rewrite linvunitor_assoc.
rewrite <- vassocr.
rewrite rassociator_lassociator.
apply id2_right.
- intros Z W V g h.
use nat_trans_eq.
{ exact (pr2 C V Y). }
intro k.
cbn in *.
rewrite id2_left , ! id2_right.
symmetry.
apply lassociator_lassociator.
Definition representable1 :
pstrans (representable C_is_univalent_2_1 X) (representable C_is_univalent_2_1 Y).
Show proof.
End RepresentableTransformation.
Section RepresentableModification.
Context {C : bicat}{X Y : C}{f g : X --> Y}.
Variable (C_is_univalent_2_1 : is_univalent_2_1 C) (η : f ==> g).
Definition representable2_data
: modification_data (representable1 C_is_univalent_2_1 f)
(representable1 C_is_univalent_2_1 g).
Show proof.
intro Z.
use make_nat_trans.
- intro h.
simpl.
exact (h ◃ η).
- intros h k φ.
simpl.
apply vcomp_whisker.
use make_nat_trans.
- intro h.
simpl.
exact (h ◃ η).
- intros h k φ.
simpl.
apply vcomp_whisker.
Definition representable2_is_modification
: is_modification (σ := representable1 C_is_univalent_2_1 f) representable2_data.
Show proof.
intros Z W h.
use nat_trans_eq.
{ exact (pr2 C W Y). }
intro k.
cbn in *.
symmetry.
apply lwhisker_lwhisker.
use nat_trans_eq.
{ exact (pr2 C W Y). }
intro k.
cbn in *.
symmetry.
apply lwhisker_lwhisker.
Definition representable2 :
modification (representable1 C_is_univalent_2_1 f) (representable1 C_is_univalent_2_1 g).
Show proof.
End RepresentableModification.