# Library UniMath.Bicategories.Core.BicategoryLaws

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.Bicategories.Core.Bicat. Import Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Unitors.
Local Open Scope bicategory_scope.
Local Open Scope cat.

Section laws.
Context {C : bicat}.

Definition triangle_r
{X Y Z : C}
(g : CY,Z)
(f : CX,Y)
: lunitor g ⋆⋆ id₂ f = (id₂ g ⋆⋆ runitor f) o lassociator f (id₁ Y) g.
Proof.
cbn.
apply pathsinv0.
unfold hcomp.
etrans.
{ apply maponpaths.
etrans. { apply maponpaths.
apply lwhisker_id2. }
apply id2_right. }
etrans. apply runitor_rwhisker.
apply pathsinv0.
etrans. { apply maponpaths_2. apply id2_rwhisker. }
apply id2_left.
Qed.

Definition interchange
{X Y Z : C}
{f₁ g₁ h₁ : CY,Z}
{f₂ g₂ h₂ : CX,Y}
(η₁ : f₁ ==> g₁) (η₂ : f₂ ==> g₂)
(ε₁ : g₁ ==> h₁) (ε₂ : g₂ ==> h₂)
: (ε₁ o η₁) ⋆⋆ (ε₂ o η₂) = (ε₁ ⋆⋆ ε₂) o (η₁ ⋆⋆ η₂).
Proof.
apply hcomp_vcomp.
Qed.

Definition rinvunitor_natural
{X Y : C}
{f g : CX, Y}
(η : f ==> g)
: rinvunitor g o η = (id₂ (id₁ Y) ⋆⋆ η) o rinvunitor f.
Proof.
use (vcomp_rcancel (runitor _ )).
{ apply is_invertible_2cell_runitor. }
rewrite vassocl.
rewrite rinvunitor_runitor.
use (vcomp_lcancel (runitor _ )).
{ apply is_invertible_2cell_runitor. }
repeat rewrite vassocr.
rewrite runitor_rinvunitor.
rewrite id2_left, id2_right.
apply (! runitor_natural _ _ _ _ _ ).
Qed.

Definition linvunitor_natural
{X Y : C}
{f g : CX, Y}
(η : f ==> g)
: linvunitor g o η = (η ⋆⋆ id₂ (id₁ X)) o linvunitor f.
Proof.
use (vcomp_rcancel (lunitor _ )).
{ apply is_invertible_2cell_lunitor. }
rewrite vassocl.
rewrite linvunitor_lunitor.
use (vcomp_lcancel (lunitor _ )).
{ apply is_invertible_2cell_lunitor. }
repeat rewrite vassocr.
rewrite lunitor_linvunitor.
rewrite id2_left, id2_right.
apply (! lunitor_natural _ _ _ _ _ ).
Qed.

Definition lwhisker_hcomp
{X Y Z : C}
{f g : CY,Z}
(h : CX, Y)
(α : f ==> g)
: h α = id₂ h α.
Proof.
unfold hcomp.
rewrite id2_rwhisker.
rewrite id2_left.
reflexivity.
Qed.

Definition rwhisker_hcomp
{X Y Z : C}
{f g : CX,Y}
(h : CY,Z)
(α : f ==> g)
: α h = α id₂ h.
Proof.
unfold hcomp.
rewrite lwhisker_id2.
rewrite id2_right.
reflexivity.
Qed.

Definition inverse_pentagon
{V W X Y Z : C}
(k : CY,Z) (h : CX,Y)
(g : CW,X) (f : CV,W)
: rassociator f g (k h) o rassociator (g f) h k
=
(id₂ f rassociator g h k) o (rassociator f (h g) k)
o (rassociator f g h id₂ k).
Proof.
use inv_cell_eq.
- is_iso.
- is_iso.
- cbn. rewrite <- !vassocr. apply pentagon.
Qed.

Definition inverse_pentagon_2
{V W X Y Z : C}
(k : CY,Z) (h : CX,Y)
(g : CW,X) (f : CV,W)
: rassociator (g f) h k o (lassociator f g h id2 k)
=
lassociator f g (k h) o (f rassociator g h k)
o rassociator f (h g) k.
Proof.
rewrite <- !inverse_of_assoc.
use vcomp_move_R_Mp.
{
is_iso.
}
rewrite <- vassocr.
use vcomp_move_L_pM.
{
is_iso.
}
rewrite <- vassocr.
use vcomp_move_L_pM.
{
is_iso.
}
symmetry.
pose (pentagon k h g f) as p.
unfold hcomp in p.
rewrite id2_rwhisker in p.
rewrite id2_left in p.
exact p.
Qed.

Definition inverse_pentagon_3
{V W X Y Z : C}
(k : CY,Z) (h : CX,Y)
(g : CW,X) (f : CV,W)
: rassociator f g (k h) o rassociator (g f) h k o (id₂ k ⋆⋆ lassociator f g h)
=
rassociator g h k ⋆⋆ id₂ f o rassociator f (h g) k.
Proof.
use vcomp_move_R_pM.
{
is_iso.
}
cbn.
apply inverse_pentagon.
Qed.

Definition inverse_pentagon_4
{V W X Y Z : C}
(k : CY,Z) (h : CX,Y)
(g : CW,X) (f : CV,W)
: (lassociator g h k ⋆⋆ id₂ f) o rassociator f g (k h)
=
rassociator f (h g) k o id₂ k ⋆⋆ rassociator f g h o lassociator (g f) h k.
Proof.
rewrite <- !inverse_of_assoc.
use vcomp_move_R_pM.
{
is_iso.
}
rewrite !vassocr.
use vcomp_move_L_Mp.
{
is_iso.
}
use vcomp_move_L_Mp.
{
is_iso.
}
rewrite <- !vassocr.
symmetry ; apply pentagon.
Qed.

Definition inverse_pentagon_5
{V W X Y Z : C}
(k : CY,Z) (h : CX,Y)
(g : CW,X) (f : CV,W)
: lassociator f g (k h) o (rassociator g h k ⋆⋆ id₂ f)
=
rassociator (g f) h k o (id₂ k ⋆⋆ lassociator f g h) o lassociator f (h g) k.
Proof.
rewrite <- !inverse_of_assoc.
use vcomp_move_R_pM.
{
is_iso.
}
rewrite !vassocr.
use vcomp_move_L_Mp.
{
is_iso.
}
rewrite <- !vassocr.
apply pentagon.
Qed.

Definition inverse_pentagon_6
{V W X Y Z : C}
(k : CY,Z) (h : CX,Y)
(g : CW,X) (f : CV,W)
: rassociator f (h g) k o id₂ k ⋆⋆ rassociator f g h
=
lassociator g h k ⋆⋆ id₂ f o rassociator f g (k h) o rassociator (g f) h k.
Proof.
rewrite !vassocr.
use vcomp_move_L_Mp.
{
is_iso.
}
cbn.
symmetry.
rewrite <- !vassocr.
apply inverse_pentagon.
Qed.

Definition pentagon_2
{V W X Y Z : C}
(k : CY,Z) (h : CX,Y)
(g : CW,X) (f : CV,W)
: lassociator f (h g) k o lassociator g h k ⋆⋆ id₂ f
=
id₂ k ⋆⋆ rassociator f g h o lassociator (g f) h k o lassociator f g (k h).
Proof.
rewrite <- !inverse_of_assoc.
rewrite !vassocr.
use vcomp_move_L_Mp.
{
is_iso.
}
rewrite <- !vassocr.
symmetry ; apply pentagon.
Qed.

Definition triangle_r_inv
{X Y Z : C}
(g : C Y, Z ) (f : C X, Y )
: linvunitor g ⋆⋆ id₂ f
=
rassociator _ _ _ o id₂ g ⋆⋆ rinvunitor f.
Proof.
use inv_cell_eq.
- is_iso.
- is_iso.
- cbn. apply triangle_r.
Qed.

Definition triangle_l
{X Y Z : C}
(g : CY,Z) (f : CX,Y)
: lunitor g ⋆⋆ id₂ f o rassociator _ _ _ = id₂ g ⋆⋆ runitor f.
Proof.
rewrite triangle_r.
rewrite vassocr.
rewrite <- inverse_of_assoc.
rewrite vcomp_linv.
rewrite id2_left.
reflexivity.
Qed.

Definition whisker_l_hcomp
{W X Y Z : C}
{f : CX,Y} {g : CY,Z}
(k₁ k₂ : CW,X)
(α : k₁ ==> k₂)
: lassociator _ _ _ o (g f α) = g (f α) o lassociator _ _ _.
Proof.
symmetry.
apply rwhisker_rwhisker.
Qed.

Definition whisker_r_hcomp
{W X Y Z : C}
{f : CX,Y} {g : CY,Z}
(k₁ k₂ : CZ,W)
(α : k₁ ==> k₂)
: rassociator _ _ _ o (α g f) = (α g) f o rassociator _ _ _.
Proof.
use vcomp_move_R_Mp.
{
is_iso.
}
cbn.
rewrite <- vassocr.
use vcomp_move_L_pM.
{
is_iso.
}
cbn.
symmetry.
apply @lwhisker_lwhisker.
Qed.

Definition whisker_l_natural
{X Y : C}
{f : CX,X}
(η : id₁ X ==> f)
(k₁ k₂ : CX,Y)
(α : k₁ ==> k₂)
: k₂ η o linvunitor k₂ o α = α f o (k₁ η) o linvunitor k₁.
Proof.
rewrite lwhisker_hcomp, rwhisker_hcomp.
rewrite !vassocr.
rewrite linvunitor_natural.
rewrite <- !vassocr.
apply maponpaths.
rewrite rwhisker_hcomp.
rewrite <- !interchange.
rewrite !id2_right, !id2_left.
reflexivity.
Qed.

Definition whisker_r_natural
{X Y : C}
{f : CX,X}
(η : id₁ X ==> f)
(k₁ k₂ : CY,X)
(α : k₁ ==> k₂)
: η k₂ o rinvunitor k₂ o α = (f α) o (η k₁) o rinvunitor k₁.
Proof.
rewrite lwhisker_hcomp, rwhisker_hcomp.
rewrite !vassocr.
rewrite rinvunitor_natural.
rewrite <- !vassocr.
apply maponpaths.
rewrite lwhisker_hcomp.
rewrite <- !interchange.
rewrite !id2_right, !id2_left.
reflexivity.
Qed.

Definition whisker_l_iso_id₁
{X Y : C}
{f : CX,X}
(η : id₁ X ==> f)
(k₁ k₂ : CY,X)
(α : k₁ ==> k₂)
(inv_η : is_invertible_2cell η)
: α = runitor k₂ o (inv_η^-1 k₂) o (f α) o (η k₁) o rinvunitor k₁.
Proof.
rewrite !vassocr.
use vcomp_move_L_Mp.
{
is_iso.
}
use vcomp_move_L_Mp.
{
is_iso.
}
rewrite <- !vassocr.
exact (whisker_r_natural η k₁ k₂ α).
Qed.

Definition whisker_r_iso_id₁
{X Y : C}
{f : CX,X}
(η : id₁ X ==> f)
(k₁ k₂ : CX,Y)
(α : k₁ ==> k₂)
(inv_η : is_invertible_2cell η)
: α = lunitor k₂ o (k₂ inv_η^-1) o (α f) o (k₁ η) o linvunitor k₁.
Proof.
rewrite !vassocr.
use vcomp_move_L_Mp.
{
is_iso.
}
use vcomp_move_L_Mp.
{
is_iso.
}
rewrite <- !vassocr.
exact (whisker_l_natural η k₁ k₂ α).
Qed.

Definition whisker_l_eq
{W X Y Z : C}
{f : CX,Y} {g : CY,Z}
(k₁ k₂ : CW,X)
(α β : k₁ ==> k₂)
: f α = f β (g f) α = (g f) β.
Proof.
intros Hαβ.
rewrite !rwhisker_hcomp.
rewrite !rwhisker_hcomp in Hαβ.
rewrite <- !hcomp_identity.
apply (vcomp_rcancel (lassociator _ _ _)).
{
is_iso.
}
rewrite !hcomp_lassoc.
rewrite Hαβ.
reflexivity.
Qed.

Definition whisker_r_eq
{W X Y Z : C}
{f : CY,Z} {g : CX,Y}
(k₁ k₂ : CZ,W)
(α β : k₁ ==> k₂)
: α f = β f α (f g) = β (f g).
Proof.
intros Hαβ.
rewrite !lwhisker_hcomp.
rewrite !lwhisker_hcomp in Hαβ.
rewrite <- !hcomp_identity.
apply (vcomp_lcancel (lassociator _ _ _)).
{
is_iso.
}
rewrite <- !hcomp_lassoc.
rewrite Hαβ.
reflexivity.
Qed.

Definition left_unit_assoc
{X Y Z : C}
(g : CY,Z) (f : CX,Y)
: (runitor g) f = runitor (g f) o lassociator f g (id₁ Z).
Proof.
rewrite <- runitor_triangle.
unfold assoc.
rewrite vassocr.
rewrite lassociator_rassociator.
rewrite id2_left.
reflexivity.
Qed.

Definition left_unit_inv_assoc
{X Y Z : C}
(g : CY,Z) (f : CX,Y)
: (rinvunitor g) f = rassociator _ _ _ o rinvunitor (g f).
Proof.
rewrite <- rinvunitor_triangle.
rewrite <- vassocr.
rewrite lassociator_rassociator.
rewrite id2_right.
reflexivity.
Qed.

Definition lunitor_assoc
{X Y Z : C}
(g : CY,Z) (f : CX,Y)
: lunitor (g f) = g (lunitor f) o lassociator (id₁ X) f g.
Proof.
symmetry.
apply lunitor_triangle.
Qed.

Definition linvunitor_assoc
{X Y Z : C}
(g : CY,Z) (f : CX,Y)
: linvunitor (g f) = rassociator (id₁ X) f g o (g (linvunitor f)).
Proof.
use vcomp_move_L_pM.
{
is_iso.
}
cbn.
use vcomp_move_R_Mp.
{
is_iso.
}
cbn. rewrite <- lunitor_triangle.
rewrite vassocr.
rewrite rassociator_lassociator.
rewrite id2_left.
reflexivity.
Qed.

Definition lunitor_id_is_left_unit_id
(X : C)
: lunitor (id₁ X) = runitor (id₁ X).
Proof.
apply lunitor_runitor_identity.
Qed.

Definition lunitor_V_id_is_left_unit_V_id
(X : C)
: linvunitor (id₁ X) = rinvunitor (id₁ X).
Proof.
use inv_cell_eq.
- is_iso.
- is_iso.
- cbn. apply lunitor_runitor_identity.
Qed.

Definition left_unit_inv_assoc₂
{X Y Z : C}
(g : CY,Z) (f : CX,Y)
: rinvunitor (g f) = lassociator f g (id₁ Z) o (rinvunitor g f).
Proof.
rewrite left_unit_inv_assoc.
rewrite <- !vassocr.
rewrite rassociator_lassociator.
rewrite id2_right.
reflexivity.
Qed.

Definition triangle_l_inv
{X Y Z : C}
(g : CY,Z) (f : CX,Y)
: lassociator f (id₁ Y) g o linvunitor g ⋆⋆ id₂ f = id₂ g ⋆⋆ rinvunitor f.
Proof.
use inv_cell_eq.
- is_iso.
- is_iso.
- cbn. apply triangle_l.
Qed.

End laws.