Corollary well_pointed_has_ptd_alg_isaprop (A : C) : isaprop (∑ a : F A --> A, (σ A) · a = identity A). Proof. apply invproofirrelevance; red. intros [a ar] [b br]. apply subtypeInjectivity; simpl. { intros f. apply homset_property. } set (is := (well_pointed_point_is_z_iso_at_algebra (make_ptd_alg F A a ar))). apply (pre_comp_with_z_iso_is_inj is); simpl. exact (ar @ ! br). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering.