Library UniMath.CategoryTheory.BicatOfCatsElementary

the constituents of the bicategory of categories without using the package Bicategories; all is expressed with reference to the functor categories

this is useful for developments that are inspired by bicategorical insights but that are spelt out in elementary form, so as to avoid dependency on the package Bicategories, in particular used in examples of whiskered monoidal categories and actegories and in the package SubstitutionSystems

author: Ralph Matthes 2023

Require Import UniMath.Foundations.PartD.

Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.whiskering.

Local Open Scope cat.

Definition id1_CAT (C : category) : [C , C ] := functor_identity C.

the data of a prebicat_2_id_comp_struct

Definition id2_CAT {C D : category} (F : [C , D ]) : [C , D ]⟦F , F ⟧ := nat_trans_id (F : functor _ _).

Definition lunitor_CAT {C D : category} (F : [C , D ])
  : [C , D ]⟦functor_compose (id1_CAT C) F , F ⟧
  := nat_trans_id (F : functor _ _).

Definition runitor_CAT {C D : category} (F : [C , D ])
  : [C , D ]⟦functor_compose F (id1_CAT D), F ⟧
  := nat_trans_id (F : functor _ _).

Definition linvunitor_CAT {C D : category} (F : [C , D ])
  : [C , D ]⟦F , functor_compose (id1_CAT C) F ⟧
  := nat_trans_id (F : functor _ _).

Definition rinvunitor_CAT {C D : category} (F : [C , D ])
  : [C , D ]⟦F , functor_compose F (id1_CAT D)⟧
  := nat_trans_id (F : functor _ _).

Definition lassociator_CAT {C D E F : category} (X : [C , D ]) (Y : [D , E ]) (Z : [E , F ]) :
    [C , F ] ⟦functor_compose X (functor_compose Y Z), functor_compose (functor_compose X Y) Z ⟧
    := nat_trans_id (functor_composite X (functor_composite Y Z)).

Definition rassociator_CAT {C D E F : category} (X : [C , D ]) (Y : [D , E ]) (Z : [E , F ]) :
    [C , F ] ⟦functor_compose (functor_compose X Y) Z , functor_compose X (functor_compose Y Z)⟧
    := nat_trans_id (functor_composite (functor_composite X Y) Z).

Definition vcomp2_CAT {C D : category} {F G H : [C , D ]} : [C ,D ]⟦F , G ⟧ -> [C ,D ]⟦G , H ⟧ -> [C ,D ]⟦F , H ⟧.
Show proof.

intros α β. exact (nat_trans_comp _ _ _ α β).

Definition lwhisker_CAT {C D E : category} (F : [C , D ]) {G1 G2 : [D , E ]}
: [D , E ]⟦G1 , G2 ⟧ -> [C , E ]⟦functor_compose F G1 , functor_compose F G2 ⟧.
Show proof.

intro α. exact (pre_whisker (F : functor _ _) α).

Definition rwhisker_CAT {C D E : category} {F1 F2 : [C , D ]} (G : [D , E ])
: [C , D ]⟦F1 , F2 ⟧ -> [C , E ]⟦functor_compose F1 G , functor_compose F2 G ⟧.
Show proof.

intro α. exact (post_whisker α (G : functor _ _)).

the proofs required in prebicat_laws

Lemma id2_left_CAT {C D : category} {F G : [C , D ]} (α : [C , D ]⟦F , G ⟧) :
id2_CAT F · α = α.
Show proof.

apply id_left.

Lemma id2_right_CAT {C D : category} {F G : [C , D ]} (α : [C , D ]⟦F , G ⟧) :
α · id2_CAT G = α.
Show proof.

apply id_right.

Lemma vassocr_CAT {C D : category} {F G H K : [C , D ]}
(α : [C , D ]⟦F , G ⟧) (β : [C , D ]⟦G , H ⟧)(γ : [C , D ]⟦H , K ⟧) :
α · (β · γ ) = (α · β ) · γ.
Show proof.

apply assoc.

Lemma lwhisker_id2_CAT {C D E : category} (F : [C , D ]) (G : [D , E ]) :
lwhisker_CAT F (id2_CAT G) = id2_CAT _.
Show proof.

apply pre_whisker_identity.

Lemma id2_rwhisker_CAT {C D E : category} (F : [C , D ]) (G : [D , E ]) :
rwhisker_CAT G (id2_CAT F) = id2_CAT _.
Show proof.

apply post_whisker_identity.

Lemma lwhisker_vcomp_CAT {C D E : category} (F : [C , D ]) (G H I : [D , E ])
(α : [D , E ]⟦G , H ⟧) (β : [D , E ]⟦H , I ⟧) :
lwhisker_CAT F α · lwhisker_CAT F β = lwhisker_CAT F (α · β).
Show proof.

apply pathsinv0, pre_whisker_composition.

Lemma rwhisker_vcomp_CAT {C D E : category} (F G H : [C , D ]) (I : [D , E ])
(α : [C , D ]⟦F , G ⟧) (β : [C , D ]⟦G , H ⟧) :
rwhisker_CAT I α · rwhisker_CAT I β = rwhisker_CAT I (α · β).
Show proof.

apply pathsinv0, post_whisker_composition.

Lemma vcomp_lunitor_CAT {C D : category} {F G : [C , D ]} (α : [C , D ]⟦F , G ⟧) :
lwhisker_CAT (id1_CAT C) α · lunitor_CAT G = lunitor_CAT F · α.
Show proof.

apply (nat_trans_eq D); intro c.
rewrite id_left; apply id_right.

Lemma vcomp_runitor_CAT {C D : category} {F G : [C , D ]} (α : [C , D ]⟦F , G ⟧) :
rwhisker_CAT (id1_CAT D) α · runitor_CAT G = runitor_CAT F · α.
Show proof.

  apply (nat_trans_eq D); intro c.
  cbn.
  rewrite id_left. apply id_right.

Lemma lwhisker_lwhisker_CAT {A B C D : category} {F : [A , B ]} {G : [B , C ]} {H I : [C , D ]}
  (α : [C , D ]⟦H , I ⟧) :
  lwhisker_CAT F (lwhisker_CAT G α) · lassociator_CAT _ _ _ =
    lassociator_CAT _ _ _ · lwhisker_CAT (functor_compose F G) α.
Show proof.

  apply (nat_trans_eq D); intro c.
  cbn.
  rewrite id_left; apply id_right.

Lemma rwhisker_lwhisker_CAT {A B C D : category} {F : [A , B ]} {G H : [B , C ]} {I : [C , D ]}
  (α : [B , C ]⟦G , H ⟧) :
  lwhisker_CAT F (rwhisker_CAT I α) · lassociator_CAT _ _ _ =
    lassociator_CAT _ _ _ · rwhisker_CAT I (lwhisker_CAT F α).
Show proof.

  apply (nat_trans_eq D); intro c.
  cbn.
  rewrite id_left; apply id_right.

Lemma rwhisker_rwhisker_CAT {A B C D : category} {F G : [A , B ]} {H : [B , C ]} {I : [C , D ]}
  (α : [A , B ]⟦F , G ⟧) :
  lassociator_CAT _ _ _ · rwhisker_CAT I (rwhisker_CAT H α) =
    rwhisker_CAT (functor_compose H I) α · lassociator_CAT _ _ _.
Show proof.

  apply (nat_trans_eq D); intro c.
  cbn.
  rewrite id_left, id_right.
  apply idpath.

Lemma vcomp_whisker_CAT {A B C : category} {F G : [A , B ]} {H I : [B , C ]}
(α : [A , B ]⟦F , G ⟧) (β : [B , C ]⟦H , I ⟧) :
rwhisker_CAT H α · lwhisker_CAT G β = lwhisker_CAT F β · rwhisker_CAT I α.
Show proof.

apply (nat_trans_eq C); intro c.
apply (pr2 β).

Lemma lunitor_linvunitor_CAT {C D : category} (F : [C , D ]) :
lunitor_CAT F · linvunitor_CAT _ = id2_CAT _.
Show proof.

apply (nat_trans_eq D); intro c.
apply id_right.

Lemma linvunitor_lunitor_CAT {C D : category} (F : [C , D ]) :
linvunitor_CAT F · lunitor_CAT _ = id2_CAT _.
Show proof.

apply (nat_trans_eq D); intro c.
apply id_right.

Lemma runitor_rinvunitor_CAT {C D : category} (F : [C , D ]) :
runitor_CAT F · rinvunitor_CAT _ = id2_CAT _.
Show proof.

apply (nat_trans_eq D); intro c.
apply id_right.

Lemma rinvunitor_runitor_CAT {C D : category} (F : [C , D ]) :
rinvunitor_CAT F · runitor_CAT _ = id2_CAT _.
Show proof.

apply (nat_trans_eq D); intro c.
apply id_right.

Lemma lassociator_rassociator_CAT {C D E F : category} (X : [C , D ]) (Y : [D , E ]) (Z : [E , F ]) :
lassociator_CAT X Y Z · rassociator_CAT _ _ _ = id2_CAT _.
Show proof.

apply (nat_trans_eq F); intro c.
apply id_right.

Lemma rassociator_lassociator_CAT {C D E F : category} (X : [C , D ]) (Y : [D , E ]) (Z : [E , F ]) :
rassociator_CAT X Y Z · lassociator_CAT _ _ _ = id2_CAT _.
Show proof.

apply (nat_trans_eq F); intro c.
apply id_right.

Lemma runitor_rwhisker_CAT {A B C : category} (F : [A , B ]) (G : [B , C ]) :
lassociator_CAT F (id1_CAT B) G · (rwhisker_CAT G (runitor_CAT F)) =
lwhisker_CAT F (lunitor_CAT G).
Show proof.

  apply (nat_trans_eq C); intro c.
  cbn.
  rewrite id_left.
  apply functor_id.

Lemma lassociator_lassociator_CAT {A B C D E : category}
  (F : [A , B ]) (G : [B , C ]) (H : [C , D ]) (I : [D , E ]) :
  lwhisker_CAT F (lassociator_CAT G H I) · lassociator_CAT _ (functor_compose G H) _ ·
    (rwhisker_CAT I (lassociator_CAT _ _ _)) =
    lassociator_CAT F G (functor_compose H I) · lassociator_CAT (functor_compose F G) _ _.
Show proof.

  apply (nat_trans_eq E); intro c.
  cbn.
  do 3 rewrite id_left.
  apply functor_id.

now for convenience

Lemma lunitor_CAT_pointwise_is_z_iso {C D : category} (F : [C , D ]) :
is_z_isomorphism (lunitor_CAT F).
Show proof.

  exists (linvunitor_CAT F).
  split.
  - apply lunitor_linvunitor_CAT.
  - apply linvunitor_lunitor_CAT.

Lemma runitor_CAT_pointwise_is_z_iso {C D : category} (F : [C , D ]) :
is_z_isomorphism (runitor_CAT F).
Show proof.

  exists (rinvunitor_CAT F).
  split.
  - apply runitor_rinvunitor_CAT.
  - apply rinvunitor_runitor_CAT.

Definition lassociator_CAT_pointwise_is_z_iso {C D E F : category} (X : functor C D)(Y : functor D E)(Z : functor E F) :
is_z_isomorphism (lassociator_CAT X Y Z).
Show proof.

  exists (rassociator_CAT X Y Z).
  split.
  - apply lassociator_rassociator_CAT.
  - apply rassociator_lassociator_CAT.

laws that are instances of derivable rules in bicategories; here, we just prove them directly

Lemma lwhisker_lwhisker_rassociator_CAT {A B C D : category} {F : [A , B ]} {G : [B , C ]} {H I : [C , D ]}
  (α : [C , D ]⟦H , I ⟧) :
   rassociator_CAT _ _ _ · lwhisker_CAT F (lwhisker_CAT G α) =
    lwhisker_CAT (functor_compose F G) α · rassociator_CAT _ _ _ .
Show proof.

  apply (nat_trans_eq D); intro c.
  cbn.
  rewrite id_right; apply id_left.

Lemma rwhisker_lwhisker_rassociator_CAT {A B C D : category} {F : [A , B ]} {G H : [B , C ]} {I : [C , D ]}
  (α : [B , C ]⟦G , H ⟧) :
  rassociator_CAT _ _ _ · lwhisker_CAT F (rwhisker_CAT I α) =
    rwhisker_CAT I (lwhisker_CAT F α) · rassociator_CAT _ _ _.
Show proof.

  apply (nat_trans_eq D); intro c.
  cbn.
  rewrite id_right; apply id_left.

Lemma rwhisker_rwhisker_alt_CAT {A B C D : category} {F : [B , A ]} {G : [C , B ]} {H I : [D , C ]}
  (α : [D , C ]⟦H , I ⟧) :
  rwhisker_CAT F (rwhisker_CAT G α) · rassociator_CAT _ _ _ =
    rassociator_CAT _ _ _ · rwhisker_CAT (functor_compose G F) α.
Show proof.

  apply (nat_trans_eq A); intro d.
  cbn.
  rewrite id_left; apply id_right.

Lemma lunitor_lwhisker_CAT {A B C : category} (F : [A , B ]) (G : [B , C ]) :
rassociator_CAT F (id1_CAT B) G · (lwhisker_CAT F (lunitor_CAT G)) =
rwhisker_CAT G (runitor_CAT F).
Show proof.

  apply (nat_trans_eq C); intro c.
  cbn.
  rewrite id_left.
  apply pathsinv0, functor_id.

Lemma rassociator_rassociator_CAT {A B C D E : category}
  (F : [A , B ]) (G : [B , C ]) (H : [C , D ]) (I : [D , E ]) :
  rwhisker_CAT I (rassociator_CAT F G H) · rassociator_CAT _ (functor_compose G H) _ ·
    (lwhisker_CAT F (rassociator_CAT _ _ _)) =
    rassociator_CAT (functor_compose F G) H I · rassociator_CAT F G (functor_compose H I).
Show proof.

  apply (nat_trans_eq E); intro c.
  cbn.
  do 3 rewrite id_right.
  apply functor_id.