Library UniMath.CategoryTheory.Bicategories.Bicategories.Unitors

Bicategories

Benedikt Ahrens, Marco Maggesi April 2018
We formalize the proof showing that in a bicategory, left and right unitor coincide on the identity. We follow Joyal and Ross' Braided Tensor Categories, Proposition 1.1
*********************************************************************************
The triangle with "?" in the proof of the Proposition

Lemma runitor_rwhisker_rwhisker {a b c d: C} (f : Ca, b)
      (g : Cb, c) (h : Cc, d)
  : (rassociator f g (identity c) h) ((f runitor g) h) =
    runitor (f · g) h.
Proof.
rewrite with uppler left triangle
  apply pathsinv0.
  etrans.
  { apply pathsinv0. apply lunitor_lwhisker. }

  
attach rassociator on both sides
  apply (vcomp_rcancel (rassociator _ _ _ )).
  { apply is_invertible_2cell_rassociator. }

  
rewrite upper right square
  etrans.
  { apply vassocl. }
  etrans.
  { apply maponpaths.
    apply pathsinv0, lwhisker_lwhisker_rassociator.
  }

  
rewrite lower middle square
  apply pathsinv0.
  etrans. { apply vassocl. }
  etrans.
  { apply maponpaths.
    apply pathsinv0, rwhisker_lwhisker_rassociator.
  }

  
rewrite lower right triangle
  etrans.
  { do 3 apply maponpaths.
    apply pathsinv0.
    apply lunitor_lwhisker.
  }

  
distribute the whiskering
  etrans.
  { do 2 apply maponpaths.
    apply pathsinv0, lwhisker_vcomp.
  }

  
remove trailing lunitor
  etrans. { apply vassocr. }
  etrans. { apply vassocr. }

  apply pathsinv0.
  etrans. { apply vassocr. }
  apply maponpaths_2.

turn the rassociators into lassociators
  use inv_cell_eq.
  - use is_invertible_2cell_vcomp.
    + apply is_invertible_2cell_rassociator.
    + apply is_invertible_2cell_rassociator.
  - use is_invertible_2cell_vcomp.
    + use is_invertible_2cell_vcomp.
      × apply is_invertible_2cell_rwhisker.
        apply is_invertible_2cell_rassociator.
      × apply is_invertible_2cell_rassociator.
    + apply is_invertible_2cell_lwhisker.
      apply is_invertible_2cell_rassociator.
  - cbn.
    apply pathsinv0.
    etrans. apply vassocr.
    apply lassociator_lassociator.
Qed.

Lemma rwhisker_id_inj {a b : C} (f g : Ca, b)
      (x y : f ==> g)
  : x identity b = y identity b x = y.
Proof.
  intro H.
  apply (vcomp_lcancel (runitor _)).
  - apply is_invertible_2cell_runitor.
  - etrans. apply pathsinv0, vcomp_runitor.
    etrans. 2: apply vcomp_runitor.
    apply maponpaths_2. apply H.
Qed.

Lemma lwhisker_id_inj {a b : C} (f g : Ca, b)
      (x y : f ==> g)
  : identity a x = identity a y x = y.
Proof.
  intro H.
  apply (vcomp_lcancel (lunitor _)).
  - apply is_invertible_2cell_lunitor.
  - etrans. apply pathsinv0, vcomp_lunitor.
    etrans. 2: apply vcomp_lunitor.
    apply maponpaths_2. apply H.
Qed.

The first triangle in the Proposition a · (1 ⊗ r) = r
Lemma runitor_triangle {a b c: C} (f : Ca, b) (g : Cb, c)
  : rassociator f g (identity c) (f runitor g) = runitor (f · g).
Proof.
  apply rwhisker_id_inj.
  etrans. 2: apply runitor_rwhisker_rwhisker.
  apply pathsinv0, rwhisker_vcomp.
Qed.

The square in the Proposition
r = r ⊗ 1
Lemma runitor_is_runitor_rwhisker (a : C)
  : runitor (identity a · identity a) = runitor (identity a) (identity a).
Proof.
  apply (vcomp_rcancel (runitor _ )).
  - apply is_invertible_2cell_runitor.
  - apply pathsinv0. apply vcomp_runitor .
Qed.

l = 1 ⊗ l
Lemma lunitor_is_lunitor_lwhisker (a : C)
  : lunitor (identity a · identity a) = identity a lunitor (identity a).
Proof.
  apply (vcomp_rcancel (lunitor _ )).
  - apply is_invertible_2cell_lunitor.
  - apply pathsinv0. apply vcomp_lunitor .
Qed.

1 ⊗ r = 1 ⊗ l
Lemma lwhisker_runitor_lunitor (a : C)
  : identity a runitor (identity a) = identity a lunitor (identity a).
Proof.
  apply (vcomp_lcancel (rassociator _ _ _ )).
  - apply is_invertible_2cell_rassociator.
  - rewrite runitor_triangle.
    rewrite lunitor_lwhisker.
    apply runitor_is_runitor_rwhisker.
Qed.

Lemma runitor_lunitor_identity (a : C)
  : runitor (identity a) = lunitor (identity a).
Proof.
  apply (vcomp_lcancel (lunitor _ )).
  { apply is_invertible_2cell_lunitor. }
  etrans. { apply pathsinv0. apply vcomp_lunitor. }
  etrans. { apply maponpaths_2. apply lwhisker_runitor_lunitor. }
  apply maponpaths_2. apply (!lunitor_is_lunitor_lwhisker _).
Qed.

Lemma lunitor_runitor_identity (a : C)
  : lunitor (identity a) = runitor (identity a).
Proof.
  apply (! runitor_lunitor_identity _ ).
Qed.

End unitors.

Examples of laws derived by reversing morphisms or cells.


Definition rinvunitor_triangle (C : bicat) (a b c : C) (f : Ca,b) (g : Cb,c)
  : (f rinvunitor g) lassociator f g (identity c) = rinvunitor (f · g)
  := runitor_triangle (C := op2_bicat C) f g.

Definition lunitor_triangle (C : bicat) (a b c : C) (f : Ca,b) (g : Cb,c)
  : lassociator (identity a) f g (lunitor f g) = lunitor (f · g)
  := runitor_triangle (C := op1_bicat C) g f.