proposition: Lemma is_preinitial_to_is_initial (X : algebra_ob F) : is_preinitial X -> (∏ Y, isaprop (algebra_mor F X Y)) -> is_initial X.
proof: Proof. exact (λ is_pre is_prop Y, iscontraprop1 (is_prop Y) (is_pre Y)). Defined.
imports: UniMath.Foundations.PartD UniMath.Induction.FunctorAlgebras_legacy UniMath.Induction.PolynomialFunctors