proposition: Lemma signature_from_rel_strength_laws : θ_Strength1_int θ × θ_Strength2_int θ.
proof: Proof. split; red. - intro X. cbn. apply nat_trans_eq_alt; intro c. cbn. assert (Hyp := nat_trans_eq_weq (homset_property C) _ _ (ϛ_pentagon_eq X) c). cbn in Hyp. rewrite (functor_id (H X)) in Hyp. do 2 rewrite id_left in Hyp. etrans; [| exact Hyp]. clear Hyp. rewrite <- assoc. apply maponpaths. etrans. { apply pathsinv0. apply id_left. } apply cancel_postcomposition. apply pathsinv0. apply (nat_trans_eq_weq (homset_property C) _ _ (auxH1 H X) c). - intros X Z Z'. cbn. apply nat_trans_eq; try apply homset_property; intro c. cbn. rewrite id_left. assert (Hyp := nat_trans_eq_weq (homset_property C) _ _ (ϛ_rectangle_eq Z Z' X) c). cbn in Hyp. do 2 rewrite functor_id in Hyp. rewrite (functor_id (H X)) in Hyp. do 2 rewrite id_right in Hyp. do 2 rewrite id_left in Hyp. etrans; [| exact Hyp ]. clear Hyp. apply cancel_postcomposition. etrans. { apply pathsinv0. apply id_right. } apply maponpaths. apply pathsinv0. etrans. { use (maponpaths (fun x => pr1 (# H x) c)). + exact (identity (functor_compose (functor_compose (pr1 Z) (pr1 Z')) X)). + apply auxH2aux. } rewrite functor_id. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.BicatOfCatsElementary UniMath.SubstitutionSystems.Notation UniMath.SubstitutionSystems.Signatures UniMath.Bicategories.MonoidalCategories.ActionBasedStrength UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal UniMath.Bicategories.MonoidalCategories.PointedFunctorsMonoidal