Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored
Monoidal categories
Based on an implementation by Anthony Bordg.
Behaviour w.r.t. to swapped tensor product added by Ralph Matthes in 2019
Isos replaced by z_isos in 2021
Require Import UniMath.Foundations.PartD.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.ProductCategory.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.whiskering.
Local Open Scope cat.
Notation "'id' X" := (identity X) (at level 30).
Notation "C ⊠ D" := (category_binproduct C D) (at level 38).
Notation "( c , d )" := (make_catbinprod c d).
Notation "( f #, g )" := (catbinprodmor f g).
Section Monoidal_Precat.
Context {C : category} (tensor : C ⊠ C ⟶ C) (I : C).
Notation "X ⊗ Y" := (tensor (X, Y)).
Notation "f #⊗ g" := (#tensor (f #, g)) (at level 31).
Lemma tensor_id {X Y : C} : id X #⊗ id Y = id (X ⊗ Y).
Show proof.
Lemma tensor_comp {X Y Z X' Y' Z' : C} (f : X --> Y) (g : Y --> Z) (f' : X' --> Y') (g' : Y' --> Z') :
(f · g) #⊗ (f' · g') = f #⊗ f' · g #⊗ g'.
Show proof.
Definition is_z_iso_tensor_z_iso {X Y X' Y' : C} {f : X --> Y} {g : X' --> Y'}
(f_is_z_iso : is_z_isomorphism f) (g_is_z_iso : is_z_isomorphism g) : is_z_isomorphism (f #⊗ g).
Show proof.
Definition I_pretensor : C ⟶ C := functor_fix_fst_arg _ _ _ tensor I.
Lemma I_pretensor_ok: functor_on_objects I_pretensor = λ c, I ⊗ c.
Show proof.
Definition left_unitor : UU :=
nat_z_iso I_pretensor (functor_identity C).
Definition left_unitor_funclass (λ' : left_unitor):
∏ x : ob C, I_pretensor x --> x
:= pr1 (nat_z_iso_to_trans λ').
Coercion left_unitor_funclass : left_unitor >-> Funclass.
Definition left_unitor_to_nat_trans (λ' : left_unitor): nat_trans I_pretensor (functor_identity C)
:= nat_z_iso_to_trans λ'.
Coercion left_unitor_to_nat_trans: left_unitor >-> nat_trans.
Definition I_posttensor : C ⟶ C := functor_fix_snd_arg _ _ _ tensor I.
Lemma I_posttensor_ok: functor_on_objects I_posttensor = λ c, c ⊗ I.
Show proof.
Definition right_unitor : UU :=
nat_z_iso I_posttensor (functor_identity C).
Definition right_unitor_funclass (ρ' : right_unitor):
∏ x : ob C, I_posttensor x --> x
:= pr1 (nat_z_iso_to_trans ρ').
Coercion right_unitor_funclass : right_unitor >-> Funclass.
Definition right_unitor_to_nat_trans (ρ' : right_unitor): nat_trans I_posttensor (functor_identity C)
:= nat_z_iso_to_trans ρ'.
Coercion right_unitor_to_nat_trans: right_unitor >-> nat_trans.
Definition assoc_left : (C ⊠ C) ⊠ C ⟶ C :=
functor_composite (pair_functor tensor (functor_identity _)) tensor.
Lemma assoc_left_ok: functor_on_objects assoc_left =
λ c, (ob1 (ob1 c) ⊗ ob2 (ob1 c)) ⊗ ob2 c.
Show proof.
Definition assoc_right : (C ⊠ C) ⊠ C ⟶ C :=
functor_composite
(precategory_binproduct_unassoc _ _ _)
(functor_composite (pair_functor (functor_identity _) tensor) tensor).
Lemma assoc_right_ok: functor_on_objects assoc_right =
λ c, ob1 (ob1 c) ⊗ (ob2 (ob1 c) ⊗ ob2 c).
Show proof.
Definition associator : UU :=
nat_z_iso assoc_left assoc_right.
Definition associator_funclass (α' : associator):
∏ x : ob ((C ⊠ C) ⊠ C), assoc_left x --> assoc_right x
:= pr1 (nat_z_iso_to_trans α').
Coercion associator_funclass : associator >-> Funclass.
Definition associator_to_nat_trans (α' : associator): nat_trans assoc_left assoc_right
:= nat_z_iso_to_trans α'.
Coercion associator_to_nat_trans: associator >-> nat_trans.
Definition triangle_eq (λ' : left_unitor) (ρ' : right_unitor) (α' : associator) : UU :=
∏ (a b : C), pr1 ρ' a #⊗ id b = pr1 α' ((a, I), b) · id a #⊗ pr1 λ' b.
Definition pentagon_eq (α' : associator) : UU :=
∏ (a b c d : C), pr1 α' ((a ⊗ b, c), d) · pr1 α' ((a, b), c ⊗ d) =
pr1 α' ((a, b), c) #⊗ id d · pr1 α' ((a, b ⊗ c), d) · id a #⊗ pr1 α' ((b, c), d).
Definition is_strict (eq_λ : I_pretensor = functor_identity C) (λ' : left_unitor)
(eq_ρ : I_posttensor = functor_identity C) (ρ' : right_unitor)
(eq_α : assoc_left = assoc_right) (α' : associator) : UU :=
(is_nat_z_iso_id eq_λ λ') × (is_nat_z_iso_id eq_ρ ρ') × (is_nat_z_iso_id eq_α α').
End Monoidal_Precat.
Definition monoidal_cat : UU :=
∑ C : category, ∑ tensor : C ⊠ C ⟶ C, ∑ I : C,
∑ λ' : left_unitor tensor I,
∑ ρ' : right_unitor tensor I,
∑ α' : associator tensor,
(triangle_eq tensor I λ' ρ' α') × (pentagon_eq tensor α').
Definition make_monoidal_cat (C: category)(tensor: C ⊠ C ⟶ C)(I: C)
(λ': left_unitor tensor I)(ρ': right_unitor tensor I)(α': associator tensor)
(eq1: triangle_eq tensor I λ' ρ' α')(eq2: pentagon_eq tensor α'): monoidal_cat :=
(C,, (tensor,, (I,, (λ',, (ρ',, (α',, (eq1,, eq2))))))).
Definition monoidal_cat_cat (M : monoidal_cat) : category := pr1 M.
Coercion monoidal_cat_cat : monoidal_cat >-> category.
Section Monoidal_Cat_Accessors.
Context (M : monoidal_cat).
it is important that no new coercions are used in the given types in the following projections
Definition monoidal_cat_tensor : pr1 M ⊠ pr1 M ⟶ pr1 M := pr1 (pr2 M).
Definition monoidal_cat_unit : pr1 M := pr1 (pr2 (pr2 M)).
Definition monoidal_cat_left_unitor : left_unitor (pr1 (pr2 M)) (pr1 (pr2 (pr2 M))) := pr1 (pr2 (pr2 (pr2 M))).
Definition monoidal_cat_right_unitor : right_unitor (pr1 (pr2 M)) (pr1 (pr2 (pr2 M))) := pr1 (pr2 (pr2 (pr2 (pr2 M)))).
Definition monoidal_cat_associator : associator (pr1 (pr2 M)) := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 M))))).
Definition monoidal_cat_triangle_eq : triangle_eq (pr1 (pr2 M)) (pr1 (pr2 (pr2 M))) (pr1 (pr2 (pr2 (pr2 M)))) (pr1 (pr2 (pr2 (pr2 (pr2 M))))) (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 M)))))) := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 M)))))).
Definition monoidal_cat_pentagon_eq : pentagon_eq (pr1 (pr2 M)) (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 M)))))) := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 M)))))).
End Monoidal_Cat_Accessors.
Definition strict_monoidal_cat : UU :=
∑ M : monoidal_cat,
∏ (eq_λ : I_pretensor (monoidal_cat_tensor M) (monoidal_cat_unit M) =
functor_identity (pr1 M)),
∏ (eq_ρ : I_posttensor (monoidal_cat_tensor M) (monoidal_cat_unit M) =
functor_identity (pr1 M)),
∏ (eq_α : assoc_left (monoidal_cat_tensor M) =
assoc_right (monoidal_cat_tensor M)),
is_strict (monoidal_cat_tensor M) (monoidal_cat_unit M) eq_λ (monoidal_cat_left_unitor M) eq_ρ (monoidal_cat_right_unitor M) eq_α (monoidal_cat_associator M).
Section swapped_tensor.
Context (M : monoidal_cat).
Definition swapping_of_tensor: M ⊠ M ⟶ M := functor_composite binswap_pair_functor (monoidal_cat_tensor M).
Definition associator_swapping_of_tensor: associator swapping_of_tensor.
Show proof.
set (α := monoidal_cat_associator M).
set (α' := nat_z_iso_to_trans_inv α).
red.
set (trafo := (pre_whisker reverse_three_args α'): (assoc_left swapping_of_tensor) ⟹ (assoc_right swapping_of_tensor)).
assert (tisziso: is_nat_z_iso trafo).
{ red. intro c. set (aux := pr2 (nat_z_iso_inv α)).
apply (pre_whisker_on_nat_z_iso reverse_three_args α' aux).
}
exact (trafo,, tisziso).
set (α' := nat_z_iso_to_trans_inv α).
red.
set (trafo := (pre_whisker reverse_three_args α'): (assoc_left swapping_of_tensor) ⟹ (assoc_right swapping_of_tensor)).
assert (tisziso: is_nat_z_iso trafo).
{ red. intro c. set (aux := pr2 (nat_z_iso_inv α)).
apply (pre_whisker_on_nat_z_iso reverse_three_args α' aux).
}
exact (trafo,, tisziso).
Lemma triangle_eq_swapping_of_tensor: triangle_eq swapping_of_tensor (monoidal_cat_unit M)
(monoidal_cat_right_unitor M) (monoidal_cat_left_unitor M) associator_swapping_of_tensor.
Show proof.
red. intros a b. cbn.
set (H := monoidal_cat_triangle_eq M).
unfold triangle_eq in H.
etrans.
2: { apply cancel_precomposition.
apply pathsinv0.
apply H. }
clear H.
rewrite assoc.
etrans.
{ apply pathsinv0.
apply id_left. }
apply cancel_postcomposition.
apply pathsinv0.
set (f := nat_z_iso_pointwise_z_iso (monoidal_cat_associator M)((b, monoidal_cat_unit M), a)).
apply (z_iso_after_z_iso_inv f).
set (H := monoidal_cat_triangle_eq M).
unfold triangle_eq in H.
etrans.
2: { apply cancel_precomposition.
apply pathsinv0.
apply H. }
clear H.
rewrite assoc.
etrans.
{ apply pathsinv0.
apply id_left. }
apply cancel_postcomposition.
apply pathsinv0.
set (f := nat_z_iso_pointwise_z_iso (monoidal_cat_associator M)((b, monoidal_cat_unit M), a)).
apply (z_iso_after_z_iso_inv f).
Lemma pentagon_eq_swapping_of_tensor: pentagon_eq swapping_of_tensor associator_swapping_of_tensor.
Show proof.
red. intros a b c d. cbn.
set (H := monoidal_cat_pentagon_eq M).
unfold pentagon_eq in H.
set (f := nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((d, c), monoidal_cat_tensor M (b, a))).
apply (z_iso_inv_on_right _ _ _ f).
apply pathsinv0.
set (f' := nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((monoidal_cat_tensor M (d, c), b), a)).
apply (inv_z_iso_unique' _ _ _ f').
unfold precomp_with.
rewrite assoc.
etrans.
{ apply cancel_postcomposition.
apply H. }
clear H.
repeat rewrite assoc.
etrans.
{ do 2 apply cancel_postcomposition.
rewrite <- assoc.
apply cancel_precomposition.
apply pathsinv0.
apply (functor_comp (functor_fix_fst_arg _ _ _ (monoidal_cat_tensor M) d)).
}
etrans.
{ do 2 apply cancel_postcomposition.
apply cancel_precomposition.
apply maponpaths.
apply (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((c, b), a))). }
rewrite functor_id.
rewrite id_right.
etrans.
{ apply cancel_postcomposition.
rewrite <- assoc.
apply cancel_precomposition.
apply (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((d, monoidal_cat_tensor M (c, b)), a))). }
rewrite id_right.
etrans.
apply pathsinv0.
apply (functor_comp (functor_fix_snd_arg _ _ _ (monoidal_cat_tensor M) a)).
etrans.
{ apply maponpaths.
apply (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((d, c), b))). }
cbn.
unfold functor_fix_snd_arg_mor.
use functor_id.
set (H := monoidal_cat_pentagon_eq M).
unfold pentagon_eq in H.
set (f := nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((d, c), monoidal_cat_tensor M (b, a))).
apply (z_iso_inv_on_right _ _ _ f).
apply pathsinv0.
set (f' := nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((monoidal_cat_tensor M (d, c), b), a)).
apply (inv_z_iso_unique' _ _ _ f').
unfold precomp_with.
rewrite assoc.
etrans.
{ apply cancel_postcomposition.
apply H. }
clear H.
repeat rewrite assoc.
etrans.
{ do 2 apply cancel_postcomposition.
rewrite <- assoc.
apply cancel_precomposition.
apply pathsinv0.
apply (functor_comp (functor_fix_fst_arg _ _ _ (monoidal_cat_tensor M) d)).
}
etrans.
{ do 2 apply cancel_postcomposition.
apply cancel_precomposition.
apply maponpaths.
apply (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((c, b), a))). }
rewrite functor_id.
rewrite id_right.
etrans.
{ apply cancel_postcomposition.
rewrite <- assoc.
apply cancel_precomposition.
apply (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((d, monoidal_cat_tensor M (c, b)), a))). }
rewrite id_right.
etrans.
apply pathsinv0.
apply (functor_comp (functor_fix_snd_arg _ _ _ (monoidal_cat_tensor M) a)).
etrans.
{ apply maponpaths.
apply (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((d, c), b))). }
cbn.
unfold functor_fix_snd_arg_mor.
use functor_id.
Definition swapping_of_monoidal_cat: monoidal_cat.
Show proof.
use (make_monoidal_cat M swapping_of_tensor).
- exact (monoidal_cat_unit M).
- apply monoidal_cat_right_unitor.
- apply monoidal_cat_left_unitor.
- exact associator_swapping_of_tensor.
- exact triangle_eq_swapping_of_tensor.
- exact pentagon_eq_swapping_of_tensor.
- exact (monoidal_cat_unit M).
- apply monoidal_cat_right_unitor.
- apply monoidal_cat_left_unitor.
- exact associator_swapping_of_tensor.
- exact triangle_eq_swapping_of_tensor.
- exact pentagon_eq_swapping_of_tensor.
End swapped_tensor.
Section coherence_lemmas.
Context {Mon_V : monoidal_cat}.
Let I : Mon_V := monoidal_cat_unit Mon_V.
Let tensor : Mon_V ⊠ Mon_V ⟶ Mon_V := monoidal_cat_tensor Mon_V.
Let α : associator tensor := monoidal_cat_associator Mon_V.
Let l_unitor : left_unitor tensor I := monoidal_cat_left_unitor Mon_V.
Let r_unitor : right_unitor tensor I := monoidal_cat_right_unitor Mon_V.
Local Notation "X ⊗ Y" := (tensor (X, Y)).
Local Notation "f #⊗ g" := (#tensor (f #, g)) (at level 31).
Lemma tensor_comp_left {X Y Z W : Mon_V} (f : X --> Y) (g : Y --> Z) : ((f · g) #⊗ id W) = (f #⊗ id W) · (g #⊗ id W).
Show proof.
rewrite <- (functor_comp tensor).
change ((?x #, ?y) · (?z #, ?w)) with (x · z #, y · w).
rewrite id_left.
apply idpath.
change ((?x #, ?y) · (?z #, ?w)) with (x · z #, y · w).
rewrite id_left.
apply idpath.
Lemma tensor_comp_right {X Y Z W : Mon_V} (f : X --> Y) (g : Y --> Z) : (id W #⊗ (f · g)) = (id W #⊗ f) · (id W #⊗ g).
Show proof.
rewrite <- (functor_comp tensor).
change ((?x #, ?y) · (?z #, ?w)) with (x · z #, y · w).
rewrite id_left.
apply idpath.
change ((?x #, ?y) · (?z #, ?w)) with (x · z #, y · w).
rewrite id_left.
apply idpath.
Lemma I_posttensor_faithful {X Y : Mon_V} {f g : X --> Y} : (f #⊗ id I) = (g #⊗ id I) -> f = g.
Show proof.
intro H.
apply (pre_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 r_unitor _))).
use (pathscomp0 (! (nat_trans_ax r_unitor _ _ f))).
use (pathscomp0 _ (nat_trans_ax r_unitor _ _ g)).
apply cancel_postcomposition.
assumption.
apply (pre_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 r_unitor _))).
use (pathscomp0 (! (nat_trans_ax r_unitor _ _ f))).
use (pathscomp0 _ (nat_trans_ax r_unitor _ _ g)).
apply cancel_postcomposition.
assumption.
Lemma I_pretensor_faithful {X Y : Mon_V} {f g : X --> Y} : (id I #⊗ f) = (id I #⊗ g) -> f = g.
Show proof.
intro H.
apply (pre_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 l_unitor _))).
use (pathscomp0 (! (nat_trans_ax l_unitor _ _ f))).
use (pathscomp0 _ (nat_trans_ax l_unitor _ _ g)).
apply cancel_postcomposition.
assumption.
apply (pre_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 l_unitor _))).
use (pathscomp0 (! (nat_trans_ax l_unitor _ _ f))).
use (pathscomp0 _ (nat_trans_ax l_unitor _ _ g)).
apply cancel_postcomposition.
assumption.
Lemma right_unitor_of_tensor (X Y : Mon_V) : r_unitor (X ⊗ Y) = α ((X, Y), I) · (id X #⊗ r_unitor Y).
Show proof.
apply I_posttensor_faithful.
rewrite tensor_comp_left.
apply (post_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 α (_, _)))).
rewrite assoc'.
apply (transportb (λ h, _ = _ · h) (nat_trans_ax α _ _ ((_#, _)#, _))).
simpl.
rewrite assoc.
apply (transportb (λ h, _ = _ · #tensor (id _ #, h)) (monoidal_cat_triangle_eq Mon_V _ _)).
apply (transportf (λ k, _ = _ · #tensor (k #, _)) (id_left (id X))).
change (?x · ?z #, ?y · ?w) with ((x #, y) · (z #, w)).
rewrite (functor_comp tensor).
apply (transportb (λ h, h · _ = _) (monoidal_cat_triangle_eq Mon_V _ _)).
apply (transportf (λ h, _ · #tensor (h #, _) · _ = _) (functor_id tensor (X, Y))).
rewrite assoc'.
apply (transportb (λ h, _ · h = _) (nat_trans_ax α _ _ ((_#, _)#, _))).
rewrite !assoc.
apply cancel_postcomposition.
apply monoidal_cat_pentagon_eq.
rewrite tensor_comp_left.
apply (post_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 α (_, _)))).
rewrite assoc'.
apply (transportb (λ h, _ = _ · h) (nat_trans_ax α _ _ ((_#, _)#, _))).
simpl.
rewrite assoc.
apply (transportb (λ h, _ = _ · #tensor (id _ #, h)) (monoidal_cat_triangle_eq Mon_V _ _)).
apply (transportf (λ k, _ = _ · #tensor (k #, _)) (id_left (id X))).
change (?x · ?z #, ?y · ?w) with ((x #, y) · (z #, w)).
rewrite (functor_comp tensor).
apply (transportb (λ h, h · _ = _) (monoidal_cat_triangle_eq Mon_V _ _)).
apply (transportf (λ h, _ · #tensor (h #, _) · _ = _) (functor_id tensor (X, Y))).
rewrite assoc'.
apply (transportb (λ h, _ · h = _) (nat_trans_ax α _ _ ((_#, _)#, _))).
rewrite !assoc.
apply cancel_postcomposition.
apply monoidal_cat_pentagon_eq.
Lemma left_unitor_right_unitor_of_unit : l_unitor I = r_unitor I.
Show proof.
apply I_pretensor_faithful.
apply (pre_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 α ((_, _), _)))).
apply (pathscomp0 (! (monoidal_cat_triangle_eq Mon_V I I))).
use (pathscomp0 _ (right_unitor_of_tensor I I)).
apply (post_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 r_unitor _))).
apply (nat_trans_ax r_unitor).
apply (pre_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 α ((_, _), _)))).
apply (pathscomp0 (! (monoidal_cat_triangle_eq Mon_V I I))).
use (pathscomp0 _ (right_unitor_of_tensor I I)).
apply (post_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 r_unitor _))).
apply (nat_trans_ax r_unitor).
Lemma left_unitor_of_tensor (X Y : Mon_V) : α ((I, X), Y) · l_unitor (X ⊗ Y) = l_unitor X #⊗ id Y.
Show proof.
apply I_pretensor_faithful.
rewrite tensor_comp_right.
apply (pre_comp_with_z_iso_is_inj (pr2 α ((I, (I ⊗ X)), Y))).
use (pathscomp0 _ (nat_trans_ax α _ _ ((_ #, _) #, _))).
simpl.
apply (pre_comp_with_z_iso_is_inj (functor_on_is_z_isomorphism (functor_fix_snd_arg _ _ _ tensor Y) (pr2 α ((I, I), X)))).
simpl.
unfold functor_fix_snd_arg_mor.
change (make_dirprod ?x ?y) with (x #, y).
rewrite !assoc.
apply (transportf (λ h, _ = h · _) (functor_comp tensor _ _)).
change ((?x #, ?y) · (?z #, ?w)) with (x · z #, y · w).
apply (transportf (λ h, h · _ = _) (monoidal_cat_pentagon_eq Mon_V I I X Y)).
rewrite assoc'.
apply (transportf (λ h, _ · h = _) (monoidal_cat_triangle_eq Mon_V _ _)).
simpl.
apply (transportf (λ h, _ · #tensor (_ #, h) = _) (functor_id tensor (X, Y))).
apply (pathscomp0 (! (nat_trans_ax α _ _ ((_ #, _) #, _)))).
simpl.
apply cancel_postcomposition.
apply pathsinv0.
apply maponpaths.
apply dirprod_paths; simpl; [|apply id_left].
apply pathsinv0.
apply monoidal_cat_triangle_eq.
rewrite tensor_comp_right.
apply (pre_comp_with_z_iso_is_inj (pr2 α ((I, (I ⊗ X)), Y))).
use (pathscomp0 _ (nat_trans_ax α _ _ ((_ #, _) #, _))).
simpl.
apply (pre_comp_with_z_iso_is_inj (functor_on_is_z_isomorphism (functor_fix_snd_arg _ _ _ tensor Y) (pr2 α ((I, I), X)))).
simpl.
unfold functor_fix_snd_arg_mor.
change (make_dirprod ?x ?y) with (x #, y).
rewrite !assoc.
apply (transportf (λ h, _ = h · _) (functor_comp tensor _ _)).
change ((?x #, ?y) · (?z #, ?w)) with (x · z #, y · w).
apply (transportf (λ h, h · _ = _) (monoidal_cat_pentagon_eq Mon_V I I X Y)).
rewrite assoc'.
apply (transportf (λ h, _ · h = _) (monoidal_cat_triangle_eq Mon_V _ _)).
simpl.
apply (transportf (λ h, _ · #tensor (_ #, h) = _) (functor_id tensor (X, Y))).
apply (pathscomp0 (! (nat_trans_ax α _ _ ((_ #, _) #, _)))).
simpl.
apply cancel_postcomposition.
apply pathsinv0.
apply maponpaths.
apply dirprod_paths; simpl; [|apply id_left].
apply pathsinv0.
apply monoidal_cat_triangle_eq.
Lemma tensor_z_isomorphism_left : ∏ (x y z : Mon_V) (f : x --> y) (f_z_iso : is_z_isomorphism f), # tensor (is_z_isomorphism_mor f_z_iso #, id z) = is_z_isomorphism_mor (functor_on_is_z_isomorphism (functor_fix_snd_arg _ _ _ tensor z) f_z_iso).
Show proof.
intros.
reflexivity.
reflexivity.
Lemma tensor_z_isomorphism_right : ∏ (x y z : Mon_V) (f : x --> y) (f_z_iso : is_z_isomorphism f), # tensor (id z #, is_z_isomorphism_mor f_z_iso) = is_z_isomorphism_mor (functor_on_is_z_isomorphism (functor_fix_fst_arg _ _ _ tensor z) f_z_iso).
Show proof.
intros.
reflexivity.
reflexivity.
Lemma monoidal_cat_triangle_eq_inv (X Y : Mon_V) : (nat_z_iso_to_trans_inv r_unitor X #⊗ id Y) · α ((X, I), Y) = (id X #⊗ nat_z_iso_to_trans_inv l_unitor Y).
Show proof.
cbn.
rewrite (tensor_z_isomorphism_right _ _ _ _ _ : #tensor _ = _).
rewrite (tensor_z_isomorphism_left _ _ _ _ _ : #tensor _ = _).
change (is_z_isomorphism_mor ?x) with (inv_from_z_iso (_,,x)).
apply z_iso_inv_on_right, z_iso_inv_on_left.
apply monoidal_cat_triangle_eq.
rewrite (tensor_z_isomorphism_right _ _ _ _ _ : #tensor _ = _).
rewrite (tensor_z_isomorphism_left _ _ _ _ _ : #tensor _ = _).
change (is_z_isomorphism_mor ?x) with (inv_from_z_iso (_,,x)).
apply z_iso_inv_on_right, z_iso_inv_on_left.
apply monoidal_cat_triangle_eq.
Corollary left_unitor_inv_right_unitor_inv_of_unit : nat_z_iso_to_trans_inv l_unitor I = nat_z_iso_to_trans_inv r_unitor _.
Show proof.
apply (post_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 l_unitor _))).
apply (pathscomp0 (is_inverse_in_precat2 (is_z_isomorphism_is_inverse_in_precat (pr2 l_unitor _)))).
apply (transportb (λ f, id _ = is_z_isomorphism_mor _ · f) left_unitor_right_unitor_of_unit).
apply pathsinv0.
apply (is_inverse_in_precat2 (is_z_isomorphism_is_inverse_in_precat (pr2 r_unitor _))).
apply (pathscomp0 (is_inverse_in_precat2 (is_z_isomorphism_is_inverse_in_precat (pr2 l_unitor _)))).
apply (transportb (λ f, id _ = is_z_isomorphism_mor _ · f) left_unitor_right_unitor_of_unit).
apply pathsinv0.
apply (is_inverse_in_precat2 (is_z_isomorphism_is_inverse_in_precat (pr2 r_unitor _))).
Corollary left_unitor_inv_of_tensor (X Y : Mon_V) : (nat_z_iso_to_trans_inv l_unitor _ #⊗ id _) · α ((_, _), _) = nat_z_iso_to_trans_inv l_unitor (X ⊗ Y).
Show proof.
simpl.
rewrite tensor_z_isomorphism_left.
change (is_z_isomorphism_mor ?x) with (inv_from_z_iso (_,,x)).
apply z_iso_inv_on_right, z_iso_inv_on_left.
apply pathsinv0.
apply left_unitor_of_tensor.
rewrite tensor_z_isomorphism_left.
change (is_z_isomorphism_mor ?x) with (inv_from_z_iso (_,,x)).
apply z_iso_inv_on_right, z_iso_inv_on_left.
apply pathsinv0.
apply left_unitor_of_tensor.
Corollary right_unitor_inv_of_tensor (X Y : Mon_V) : (id _ #⊗ nat_z_iso_to_trans_inv r_unitor _) = nat_z_iso_to_trans_inv r_unitor (X ⊗ Y) · α ((_, _), _).
Show proof.
simpl.
rewrite tensor_z_isomorphism_right.
change (is_z_isomorphism_mor ?x) with (inv_from_z_iso (_,,x)).
apply pathsinv0.
apply z_iso_inv_on_right, z_iso_inv_on_left.
apply right_unitor_of_tensor.
rewrite tensor_z_isomorphism_right.
change (is_z_isomorphism_mor ?x) with (inv_from_z_iso (_,,x)).
apply pathsinv0.
apply z_iso_inv_on_right, z_iso_inv_on_left.
apply right_unitor_of_tensor.
End coherence_lemmas.