Lemma lifting_from_distr_law_data_aux {C D: category} {F: functor C C} {G: functor D D} {H: functor C D} (lambda : DistrLaw G F H H)(Aa Bb : algebra_ob F)(h : algebra_mor F Aa Bb) : is_algebra_mor G (lifting_from_distr_law_data_on_ob lambda Aa) (lifting_from_distr_law_data_on_ob lambda Bb) (#H h). Proof. unfold is_algebra_mor. simpl. set (ax := nat_trans_ax lambda). apply pathsinv0. etrans. { rewrite assoc. apply cancel_postcomposition. apply ax. } rewrite <- assoc. apply pathsinv0. rewrite <- assoc. apply cancel_precomposition. set (h_commutes := algebra_mor_commutes _ _ _ h). rewrite <- functor_comp. apply pathsinv0. change (# (F ∙ H) h) with (# H (# F h)). etrans. { apply pathsinv0. apply (functor_comp H). } apply maponpaths. apply pathsinv0. apply h_commutes. 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.