proposition: Lemma weqABStrengthLaxMorphismActegories : actionbased_strength Mon_endo' (ActionBasedStrengthOnHomsInBicat.domain_action C D') (ActionBasedStrengthOnHomsInBicat.target_action C D) H ≃ lineator_lax Mon_ptdendo (actegoryPtdEndosOnFunctors D') (actegoryPtdEndosOnFunctors D) H.
proof: Proof. unfold actionbased_strength. unfold actionbased_strength_nat. unfold nat_trans. eapply weqcomp. { apply weqtotal2asstor. } cbn. unfold actionbased_strength_triangle_eq, actionbased_strength_pentagon_eq. cbn. unfold lineator_lax. use weqbandf. - use weq_iso. + intros α v f. exact (α (f,,v)). + intros β fv. induction fv as [f v]. exact (β v f). + intro α. cbn. apply idpath. + intro β. cbn. apply idpath. - intro γ. cbn. use weqimplimpl. 4: { apply isaprop_lineator_laxlaws. } 3: { apply isapropdirprod ; [| apply isapropdirprod]; repeat (apply impred; intro); apply isaset_nat_trans; apply D. } + intro Hyps. induction Hyps as [Hypnat [Hyptriangle Hyppentagon]]. red in Hypnat; cbn in Hypnat. repeat split. * intros v f1 f2 β. cbn. apply (nat_trans_eq D). intro x. cbn. assert (Hypnatinst := toforallpaths _ _ _ (maponpaths pr1 (Hypnat (f1,,v) (f2,,v) (β,,identity(C:=PointedFunctors.category_Ptd C) v))) x). cbn in Hypnatinst. rewrite (functor_id (H f1)) in Hypnatinst. rewrite post_whisker_identity in Hypnatinst. rewrite id_left in Hypnatinst. etrans. { exact Hypnatinst. } apply maponpaths. apply (maponpaths (fun z => pr1(# H z) x)). apply (@id_left [C,D'] _ _ ((pre_whisker (pr11 v)) β: functor_composite (pr1 v) f1 ⟹ functor_composite (pr1 v) f2)). * intros v1 v2 f α. cbn. apply (nat_trans_eq D). intro x. cbn. assert (Hypnatinst0 := Hypnat (f,,v1) (f,,v2)). transparent assert (αbetter : (PointedFunctors.category_Ptd C ⟦v1,v2⟧)). { use tpair. - exact (pr1 α). - intro c. unfold PointedFunctors.ptd_pt. apply (toforallpaths _ _ _ (maponpaths pr1 (pr2 α)) c). } assert (Hypnatinst := toforallpaths _ _ _ (maponpaths pr1 (Hypnat (f,,v1) (f,,v2) (catbinprodmor (identity(C:=functor_category C D') f) αbetter))) x). cbn in Hypnatinst. rewrite (functor_id (H)) in Hypnatinst. rewrite pre_whisker_identity in Hypnatinst. rewrite id_right in Hypnatinst. etrans. { exact Hypnatinst. } apply maponpaths. apply (maponpaths (fun z => pr1(# H z) x)). apply (@id_right [C,D'] _ _ ((post_whisker (pr1 α)) f: functor_composite (pr1 v1) f ⟹ functor_composite (pr1 v2) f)). * clear Hyptriangle. intros v w f. cbn. repeat rewrite post_whisker_identity. apply (nat_trans_eq D). intro x. cbn. assert (Hyppentagoninst0 := Hyppentagon f w v). clear Hyppentagon. repeat rewrite post_whisker_identity in Hyppentagoninst0. repeat rewrite pre_whisker_identity in Hyppentagoninst0. assert (Hyppentagoninst := toforallpaths _ _ _ (maponpaths pr1 Hyppentagoninst0) x). clear Hyppentagoninst0. cbn in Hyppentagoninst. rewrite id_right. rewrite id_left. do 4 rewrite id_left in Hyppentagoninst. unfold PointedFunctorsComposition.ptd_compose in Hyppentagoninst. cbn in Hyppentagoninst. unfold post_whisker_in_funcat, pre_whisker_in_funcat, PointedFunctors.ptd_pt in Hyppentagoninst. set (aux1 := pr1 (#H (identity(C:=[C,D']) (functor_composite (pr1 v) ((pr1 w) · f)) · (identity _ · identity(C:=[C,D']) (functor_compose (pr1 v) (pr1 w) ∙ f)))) x). match goal with |[ H1 : _ = _ · ?f |- _ = _ ] => change f with aux1 in H1 end. unfold aux1 in Hyppentagoninst. clear aux1. rewrite (functor_comp H) in Hyppentagoninst. rewrite id_left in Hyppentagoninst. rewrite (functor_id H) in Hyppentagoninst. rewrite id_left in Hyppentagoninst. set (aux2 := nat_trans_data_from_nat_trans_funclass (γ (f,,functor_compose (pr1 v) (pr1 w),, identity(C:=[C,C]) _ · nat_trans_comp (post_whisker_in_funcat C C C (PointedFunctors.ptd_pt C v) (functor_identity C)) (pre_whisker_in_funcat C C C (pr1 v) (PointedFunctors.ptd_pt C w))))). match goal with | [ |- ?l _ · _ = _ ] => change l with aux2 end. unfold aux2. rewrite id_left. clear aux2. etrans. { apply cancel_postcomposition. exact Hyppentagoninst. } clear Hyppentagoninst. repeat rewrite assoc'. apply maponpaths. etrans. 2: { apply id_right. } apply maponpaths. match goal with | [ |- _ ?l1 _ · _ ?l2 _ = _] => set (Hl1 := l1); set (Hl2 := l2) end. assert (aux5: Hl1 · Hl2 = identity _). { apply functor_comp_id. apply (nat_trans_eq D'). intro x'. cbn. rewrite id_left. apply id_left. } exact (toforallpaths _ _ _ (maponpaths pr1 aux5) x). * clear Hyppentagon. intro f. cbn. do 2 rewrite post_whisker_identity. unfold total_unit. apply (nat_trans_eq D). intro x. cbn. rewrite id_left. assert (Hyptriangleinst0 := Hyptriangle f). clear Hyptriangle. repeat rewrite pre_whisker_identity in Hyptriangleinst0. assert (Hyptriangleinst := toforallpaths _ _ _ (maponpaths pr1 Hyptriangleinst0) x). clear Hyptriangleinst0. cbn in Hyptriangleinst. rewrite (functor_id (H f)) in Hyptriangleinst. do 2 rewrite id_left in Hyptriangleinst. etrans. 2: { exact Hyptriangleinst. } clear Hyptriangleinst. apply maponpaths. set (aux3 := nat_trans_data_from_nat_trans_funclass (# H ((identity (functor_compose (functor_identity C) f)) · (identity f)))). match goal with | [ |- ?l _ = _ ] => change l with aux3 end. unfold aux3; clear aux3. rewrite id_left. rewrite functor_id. set (argtoH := nat_trans_comp (nat_trans_comp (post_whisker (nat_z_iso_to_trans_inv (make_nat_z_iso (functor_identity C) (functor_identity C) (nat_trans_id (functor_identity_data C)) (is_nat_z_iso_nat_trans_id (functor_identity C)))) f) (nat_trans_id (functor_composite_data (functor_identity_data C) (pr1 f)))) (nat_trans_id (pr1 f))). match goal with | [ |- _ = _ ?r _ ] => change r with (# H argtoH) end. assert (G2: # H argtoH = identity(C:=[C,D]) (H (functor_identity C ∙ f))). { apply functor_id_id. apply nat_trans_eq_alt; intro c. cbn. do 2 rewrite id_right. apply functor_id. } rewrite G2. apply idpath. + intro Hyps. induction Hyps as [Hypnatleft [Hypnatright [Hypactor Hypunitor]]]. repeat split. * red. intros f1v1 f2v2 βα. induction f1v1 as [f1 v1]; induction f2v2 as [f2 v2]; induction βα as [β α]. cbn. red in Hypnatleft. assert (Hypnatleftinst := Hypnatleft v2 f1 f2 β). clear Hypnatleft. cbn in Hypnatleftinst. transparent assert (αbetter : (ptdendo ⟦v1,v2⟧)). { use tpair. - exact (pr1 α). - cbn. apply (nat_trans_eq C). intro c. cbn. apply (pr2 α). } assert (Hypnatrightinst := Hypnatright v1 v2 f1 αbetter). clear Hypnatright. cbn in Hypnatrightinst. change (((post_whisker_in_funcat _ _ _ (pr1 α) (H f1)) · (pre_whisker_in_funcat _ _ _ (pr1 v2) (# H β))) · (γ (f2,, v2)) = nat_trans_comp (γ (f1,, v1)) (# H ((post_whisker_in_funcat _ _ _ (pr1 α) f1) · (pre_whisker_in_funcat _ _ _ (pr1 v2) β)))). rewrite assoc'. rewrite functor_comp. etrans. { apply maponpaths. exact Hypnatleftinst. } clear Hypnatleftinst. apply (nat_trans_eq D); intro x. cbn. repeat rewrite assoc. apply cancel_postcomposition. exact (toforallpaths _ _ _ (maponpaths pr1 Hypnatrightinst) x). * clear Hypnatleft Hypnatright Hypactor. intro f. do 2 rewrite pre_whisker_identity. apply (nat_trans_eq D); intro x. cbn. rewrite (functor_id (H f)). do 2 rewrite id_left. assert (Hypunitorinst0 := Hypunitor f). cbn in Hypunitorinst0. do 2 rewrite post_whisker_identity in Hypunitorinst0. assert (Hypunitorinst := toforallpaths _ _ _ (maponpaths pr1 Hypunitorinst0) x). clear Hypunitorinst0. cbn in Hypunitorinst. rewrite id_right in Hypunitorinst. unfold total_unit in Hypunitorinst. etrans. 2: { exact Hypunitorinst. } clear Hypunitorinst. apply maponpaths. set (aux3 := # H ((identity (functor_compose (functor_identity C) f)) · (identity(C:=[C,D']) f))). match goal with | [ |- _ = _ ?r _ ] => change r with aux3 end. unfold aux3; clear aux3. rewrite id_left. rewrite functor_id. set (argtoH := nat_trans_comp (nat_trans_comp (post_whisker (nat_z_iso_to_trans_inv (make_nat_z_iso (functor_identity C) (functor_identity C) (nat_trans_id (functor_identity_data C)) (is_nat_z_iso_nat_trans_id (functor_identity C)))) f) (nat_trans_id (functor_composite_data (functor_identity_data C) (pr1 f)))) (nat_trans_id (pr1 f))). match goal with | [ |- _ ?l _ = _ ] => change l with (# H argtoH) end. assert (G2': # H argtoH = identity(C:=[C,D]) (H (functor_identity C ∙ f))). { apply functor_id_id. apply nat_trans_eq_alt; intro c. cbn. do 2 rewrite id_right. apply functor_id. } rewrite G2'. apply idpath. * clear Hypnatleft Hypnatright Hypunitor. intros f w v. assert (Hypactorinst0 := Hypactor v w f). cbn in Hypactorinst0. repeat rewrite post_whisker_identity in Hypactorinst0. do 3 rewrite post_whisker_identity. do 2 rewrite pre_whisker_identity. apply (nat_trans_eq D); intro x. cbn. repeat rewrite id_left. assert (Hypactorinst := toforallpaths _ _ _ (maponpaths pr1 Hypactorinst0) x). clear Hypactorinst0. cbn in Hypactorinst. do 2 rewrite id_left in Hypactorinst. etrans. 2: { apply cancel_postcomposition. exact Hypactorinst. } clear Hypactorinst. rewrite assoc'. etrans. { apply pathsinv0, id_right. } set (aux6 := nat_trans_data_from_nat_trans_funclass (γ (f,,functor_compose (pr1 v) (pr1 w),, identity(C:=[C,C]) _ · nat_trans_comp (post_whisker_in_funcat C C C (PointedFunctors.ptd_pt C v) (functor_identity C)) (pre_whisker_in_funcat C C C (pr1 v) (PointedFunctors.ptd_pt C w))))). match goal with | [ |- _ = ?r _ · _ ] => change r with aux6 end. unfold aux6. clear aux6. rewrite id_left. apply maponpaths. set (aux5' := pr1 (#H (identity(C:=[C,D']) (functor_composite (pr1 v) (functor_composite (pr1 w) f)) · (identity (C:=[C,D'])(functor_composite (functor_composite (pr1 v) (pr1 w)) f) · identity(C:=[C,D']) (functor_compose (pr1 v) (pr1 w) ∙ f)))) x). match goal with |[ |- _ = _ · ?f ] => change f with aux5' end. unfold aux5'. clear aux5'. rewrite (functor_comp H). rewrite id_left. rewrite (functor_id H). rewrite id_left. apply pathsinv0. match goal with | [ |- _ ?l1 _ · _ ?l2 _ = _] => set (Hl1 := l1); set (Hl2 := l2) end. assert (aux7: nat_trans_comp Hl1 Hl2 = nat_trans_id _). 2: { exact (toforallpaths _ _ _ (maponpaths pr1 aux7) x). } apply functor_comp_id_lax_specialized. apply nat_trans_eq_alt. intro x'. cbn. rewrite id_left. apply id_left. Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.Bicategories.MonoidalCategories.PointedFunctorsMonoidal UniMath.Bicategories.MonoidalCategories.Actions UniMath.Bicategories.MonoidalCategories.ConstructionOfActions UniMath.Bicategories.MonoidalCategories.ActionOfEndomorphismsInBicat UniMath.Bicategories.MonoidalCategories.ActionBasedStrength UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory UniMath.Bicategories.MonoidalCategories.ActionBasedStrongFunctorCategory UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfCats UniMath.CategoryTheory.Monoidal.Examples.EndofunctorsMonoidalElementary UniMath.CategoryTheory.Actegories.Examples.ActionOfEndomorphismsInCATElementary UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.ActionBasedStrengthOnHomsInBicat UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.CategoryTheory.Actegories.ConstructionOfActegories UniMath.CategoryTheory.coslicecat UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects UniMath.Bicategories.MonoidalCategories.PointedFunctorsWhiskeredMonoidal UniMath.Bicategories.MonoidalCategories.ActionOfEndomorphismsInBicatWhiskered UniMath.Bicategories.MonoidalCategories.BicatOfActegories