Library UniMath.Bicategories.Transformations.Examples.Unitality
Unitality laws
*********************************************************************************
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.Core.Unitors.
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.PseudoFunctors.Examples.Identity.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition.
Require Import UniMath.Bicategories.Transformations.PseudoTransformation.
Local Open Scope cat.
Section LeftUnitality.
Context {B₁ B₂ : bicat}.
Variable (F : psfunctor B₁ B₂).
Definition lunitor_pstrans_data
: pstrans_data (comp_psfunctor (id_psfunctor B₂) F) F.
Show proof.
use make_pstrans_data.
- exact (λ X, id₁ (F X)).
- intros X Y f ; cbn.
use make_invertible_2cell.
+ exact (lunitor _ • rinvunitor _).
+ is_iso.
- exact (λ X, id₁ (F X)).
- intros X Y f ; cbn.
use make_invertible_2cell.
+ exact (lunitor _ • rinvunitor _).
+ is_iso.
Definition lunitor_pstrans_is_pstrans
: is_pstrans lunitor_pstrans_data.
Show proof.
repeat split.
- intros X Y f g α ; cbn.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
- intros X ; cbn.
rewrite id2_left.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite lunitor_runitor_identity.
rewrite rinvunitor_natural.
rewrite lunitor_V_id_is_left_unit_V_id.
rewrite rwhisker_hcomp.
apply idpath.
- intros X Y Z f g ; cbn.
rewrite id2_left.
rewrite <- lwhisker_vcomp, <- rwhisker_vcomp.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite lunitor_triangle.
rewrite !vassocl.
apply maponpaths.
pose (triangle_r_inv (#F g) (#F f)) as p.
rewrite <- lwhisker_hcomp, <- rwhisker_hcomp in p.
rewrite !vassocr.
refine (!_).
etrans.
{
do 4 apply maponpaths_2.
exact (!p).
}
rewrite lwhisker_vcomp.
rewrite linvunitor_lunitor, lwhisker_id2, id2_left.
rewrite rinvunitor_triangle.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
- intros X Y f g α ; cbn.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
- intros X ; cbn.
rewrite id2_left.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite lunitor_runitor_identity.
rewrite rinvunitor_natural.
rewrite lunitor_V_id_is_left_unit_V_id.
rewrite rwhisker_hcomp.
apply idpath.
- intros X Y Z f g ; cbn.
rewrite id2_left.
rewrite <- lwhisker_vcomp, <- rwhisker_vcomp.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite lunitor_triangle.
rewrite !vassocl.
apply maponpaths.
pose (triangle_r_inv (#F g) (#F f)) as p.
rewrite <- lwhisker_hcomp, <- rwhisker_hcomp in p.
rewrite !vassocr.
refine (!_).
etrans.
{
do 4 apply maponpaths_2.
exact (!p).
}
rewrite lwhisker_vcomp.
rewrite linvunitor_lunitor, lwhisker_id2, id2_left.
rewrite rinvunitor_triangle.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
Definition lunitor_pstrans
: pstrans (comp_psfunctor (id_psfunctor B₂) F) F.
Show proof.
Definition linvunitor_pstrans_data
: pstrans_data F (comp_psfunctor (id_psfunctor B₂) F).
Show proof.
use make_pstrans_data.
- exact (λ X, id₁ (F X)).
- intros X Y f ; cbn.
use make_invertible_2cell.
+ exact (lunitor _ • rinvunitor _).
+ is_iso.
- exact (λ X, id₁ (F X)).
- intros X Y f ; cbn.
use make_invertible_2cell.
+ exact (lunitor _ • rinvunitor _).
+ is_iso.
Definition linvunitor_pstrans_is_pstrans
: is_pstrans linvunitor_pstrans_data.
Show proof.
repeat split.
- intros X Y f g α ; cbn.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
- intros X ; cbn.
rewrite id2_left.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite lunitor_runitor_identity.
rewrite rinvunitor_natural.
rewrite lunitor_V_id_is_left_unit_V_id.
rewrite rwhisker_hcomp.
apply idpath.
- intros X Y Z f g ; cbn.
rewrite id2_left.
rewrite <- lwhisker_vcomp, <- rwhisker_vcomp.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite lunitor_triangle.
rewrite !vassocl.
apply maponpaths.
pose (triangle_r_inv (#F g) (#F f)) as p.
rewrite <- lwhisker_hcomp, <- rwhisker_hcomp in p.
rewrite !vassocr.
refine (!_).
etrans.
{
do 4 apply maponpaths_2.
exact (!p).
}
rewrite lwhisker_vcomp.
rewrite linvunitor_lunitor, lwhisker_id2, id2_left.
rewrite rinvunitor_triangle.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
- intros X Y f g α ; cbn.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
- intros X ; cbn.
rewrite id2_left.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite lunitor_runitor_identity.
rewrite rinvunitor_natural.
rewrite lunitor_V_id_is_left_unit_V_id.
rewrite rwhisker_hcomp.
apply idpath.
- intros X Y Z f g ; cbn.
rewrite id2_left.
rewrite <- lwhisker_vcomp, <- rwhisker_vcomp.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite lunitor_triangle.
rewrite !vassocl.
apply maponpaths.
pose (triangle_r_inv (#F g) (#F f)) as p.
rewrite <- lwhisker_hcomp, <- rwhisker_hcomp in p.
rewrite !vassocr.
refine (!_).
etrans.
{
do 4 apply maponpaths_2.
exact (!p).
}
rewrite lwhisker_vcomp.
rewrite linvunitor_lunitor, lwhisker_id2, id2_left.
rewrite rinvunitor_triangle.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
Definition linvunitor_pstrans
: pstrans F (comp_psfunctor (id_psfunctor B₂) F).
Show proof.
End LeftUnitality.
Section RightUnitality.
Context {B₁ B₂ : bicat}.
Variable (F : psfunctor B₁ B₂).
Definition runitor_pstrans_data
: pstrans_data (comp_psfunctor F (id_psfunctor B₁)) F.
Show proof.
use make_pstrans_data.
- exact (λ X, id₁ (F X)).
- intros X Y f ; cbn.
use make_invertible_2cell.
+ exact (lunitor _ • rinvunitor _).
+ is_iso.
- exact (λ X, id₁ (F X)).
- intros X Y f ; cbn.
use make_invertible_2cell.
+ exact (lunitor _ • rinvunitor _).
+ is_iso.
Definition runitor_pstrans_is_pstrans
: is_pstrans runitor_pstrans_data.
Show proof.
repeat split.
- intros X Y f g α ; cbn.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
- intros X ; cbn.
rewrite psfunctor_id2, id2_right.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite lunitor_runitor_identity.
rewrite rinvunitor_natural.
rewrite lunitor_V_id_is_left_unit_V_id.
rewrite rwhisker_hcomp.
apply idpath.
- intros X Y Z f g ; cbn.
rewrite psfunctor_id2, id2_right.
rewrite <- lwhisker_vcomp, <- rwhisker_vcomp.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite lunitor_triangle.
rewrite !vassocl.
apply maponpaths.
pose (triangle_r_inv (#F g) (#F f)) as p.
rewrite <- lwhisker_hcomp, <- rwhisker_hcomp in p.
rewrite !vassocr.
refine (!_).
etrans.
{
do 4 apply maponpaths_2.
exact (!p).
}
rewrite lwhisker_vcomp.
rewrite linvunitor_lunitor, lwhisker_id2, id2_left.
rewrite rinvunitor_triangle.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
- intros X Y f g α ; cbn.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
- intros X ; cbn.
rewrite psfunctor_id2, id2_right.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite lunitor_runitor_identity.
rewrite rinvunitor_natural.
rewrite lunitor_V_id_is_left_unit_V_id.
rewrite rwhisker_hcomp.
apply idpath.
- intros X Y Z f g ; cbn.
rewrite psfunctor_id2, id2_right.
rewrite <- lwhisker_vcomp, <- rwhisker_vcomp.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite lunitor_triangle.
rewrite !vassocl.
apply maponpaths.
pose (triangle_r_inv (#F g) (#F f)) as p.
rewrite <- lwhisker_hcomp, <- rwhisker_hcomp in p.
rewrite !vassocr.
refine (!_).
etrans.
{
do 4 apply maponpaths_2.
exact (!p).
}
rewrite lwhisker_vcomp.
rewrite linvunitor_lunitor, lwhisker_id2, id2_left.
rewrite rinvunitor_triangle.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
Definition runitor_pstrans
: pstrans (comp_psfunctor F (id_psfunctor B₁)) F.
Show proof.
Definition rinvunitor_pstrans_data
: pstrans_data F (comp_psfunctor F (id_psfunctor B₁)).
Show proof.
use make_pstrans_data.
- exact (λ X, id₁ (F X)).
- intros X Y f ; cbn.
use make_invertible_2cell.
+ exact (lunitor _ • rinvunitor _).
+ is_iso.
- exact (λ X, id₁ (F X)).
- intros X Y f ; cbn.
use make_invertible_2cell.
+ exact (lunitor _ • rinvunitor _).
+ is_iso.
Definition rinvunitor_pstrans_is_pstrans
: is_pstrans rinvunitor_pstrans_data.
Show proof.
repeat split.
- intros X Y f g α ; cbn.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
- intros X ; cbn.
rewrite psfunctor_id2, id2_right.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite lunitor_runitor_identity.
rewrite rinvunitor_natural.
rewrite lunitor_V_id_is_left_unit_V_id.
rewrite rwhisker_hcomp.
apply idpath.
- intros X Y Z f g ; cbn.
rewrite psfunctor_id2, id2_right.
rewrite <- lwhisker_vcomp, <- rwhisker_vcomp.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite lunitor_triangle.
rewrite !vassocl.
apply maponpaths.
pose (triangle_r_inv (#F g) (#F f)) as p.
rewrite <- lwhisker_hcomp, <- rwhisker_hcomp in p.
rewrite !vassocr.
refine (!_).
etrans.
{
do 4 apply maponpaths_2.
exact (!p).
}
rewrite lwhisker_vcomp.
rewrite linvunitor_lunitor, lwhisker_id2, id2_left.
rewrite rinvunitor_triangle.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
- intros X Y f g α ; cbn.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
- intros X ; cbn.
rewrite psfunctor_id2, id2_right.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite !vassocl.
rewrite lunitor_runitor_identity.
rewrite rinvunitor_natural.
rewrite lunitor_V_id_is_left_unit_V_id.
rewrite rwhisker_hcomp.
apply idpath.
- intros X Y Z f g ; cbn.
rewrite psfunctor_id2, id2_right.
rewrite <- lwhisker_vcomp, <- rwhisker_vcomp.
rewrite !vassocr.
rewrite vcomp_lunitor.
rewrite lunitor_triangle.
rewrite !vassocl.
apply maponpaths.
pose (triangle_r_inv (#F g) (#F f)) as p.
rewrite <- lwhisker_hcomp, <- rwhisker_hcomp in p.
rewrite !vassocr.
refine (!_).
etrans.
{
do 4 apply maponpaths_2.
exact (!p).
}
rewrite lwhisker_vcomp.
rewrite linvunitor_lunitor, lwhisker_id2, id2_left.
rewrite rinvunitor_triangle.
rewrite rinvunitor_natural.
rewrite rwhisker_hcomp.
apply idpath.
Definition rinvunitor_pstrans
: pstrans F (comp_psfunctor F (id_psfunctor B₁)).
Show proof.
End RightUnitality.