Definition is_lifting {C D: category} {F: functor C C} {G: functor D D} (H: functor C D) (HH: functor (FunctorAlg F) (FunctorAlg G)): UU. Proof. set (UF := forget_algebras F). set (UG := forget_algebras G). exact (UF ∙ H = HH ∙ UG). Defined.
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.