proposition: Lemma is_prefinal_to_is_final (X : coalgebra F) : is_prefinal X -> (∏ Y, isaprop (coalgebra_homo F Y X)) -> is_final X.
proof: Proof. exact (λ is_pre is_prop Y, iscontraprop1 (is_prop Y) (is_pre Y)). Defined.
imports: UniMath.Foundations.PartD UniMath.Induction.FunctorCoalgebras_legacy UniMath.Induction.PolynomialFunctors