Lemma liftings_from_distr_laws_compose {C C' C'': category} {F: functor C C} {F': functor C' C'} {F'': functor C'' C''} {H: functor C C'} {H': functor C' C''} (lambda : DistrLaw F' F H H)(lambda' : DistrLaw F'' F' H' H'): lifting_from_distr_law lambda ∙ lifting_from_distr_law lambda' = lifting_from_distr_law (H := H ∙ H') (comp_distr_laws lambda' lambda). Proof. apply functor_eq. { apply homset_property. } simpl. get_sides_of_eq. set (left' := functor_composite_data (lifting_from_distr_law_data lambda) (lifting_from_distr_law_data lambda')). set (right' := lifting_from_distr_law_data (comp_distr_laws lambda' lambda) : functor_data (FunctorAlg F) (FunctorAlg F'')). transparent assert (okonobs: (functor_on_objects left' ~ functor_on_objects right')). { intro alg. cbn. unfold lifting_from_distr_law_data_on_ob. cbn. apply (maponpaths (λ p, tpair _ (H' (H (alg_carrier F alg))) p )). abstract ( repeat rewrite id_left; rewrite id_right; rewrite <- assoc; apply maponpaths; apply functor_comp ). } apply (functor_data_eq_from_nat_trans _ _ _ _ okonobs). red. intros alg1 alg2 m. apply algebra_mor_eq. simpl. etrans. { apply cancel_precomposition. UniMath.MoreFoundations.Tactics.show_id_type. apply (idtomor_FunctorAlg_commutes _ _ _ (okonobs alg2)). } etrans. 2: { apply cancel_postcomposition. UniMath.MoreFoundations.Tactics.show_id_type. apply pathsinv0. apply (idtomor_FunctorAlg_commutes _ _ _ (okonobs alg1)). } assert (Hyp: (idtomor (maponpaths (alg_carrier F'') (okonobs alg1)) = identity _) × (idtomor (maponpaths (alg_carrier F'') (okonobs alg2)) = identity _)). { unfold okonobs; split. - etrans. { apply maponpaths. apply (maponpathscomp (λ p : C'' ⟦ F'' (H' (H (alg_carrier F alg1))), H' (H (alg_carrier F alg1)) ⟧, tpair (fun X: C'' => C'' ⟦ F'' X, X ⟧) (H' (H (alg_carrier F alg1))) p) (alg_carrier F'')). } unfold funcomp. simpl. rewrite UniMath.MoreFoundations.PartA.maponpaths_for_constant_function. apply idpath. - etrans. { apply maponpaths. apply (maponpathscomp (λ p : C'' ⟦ F'' (H' (H (alg_carrier F alg2))), H' (H (alg_carrier F alg2)) ⟧, tpair (fun X: C'' => C'' ⟦ F'' X, X ⟧) (H' (H (alg_carrier F alg2))) p) (alg_carrier F'')). } unfold funcomp. simpl. rewrite UniMath.MoreFoundations.PartA.maponpaths_for_constant_function. apply idpath. } induction Hyp as [Hyp1 Hyp2]. rewrite Hyp1. rewrite Hyp2. rewrite id_right. apply pathsinv0. apply id_left. Qed.
Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Adjunctions.Core.