Lemma well_pointed_image_forgetful_isaprop : ∏ A : C, isaprop (∑ X : ptd_alg F, forget_ptd_alg F X = A). Proof. intros A. refine (isofhlevelweqf 1 _ (well_pointed_has_ptd_alg_isaprop A)). use weq_iso. - intros [a ar]. exists (make_ptd_alg F A a ar). apply idpath. - intros [X h]. induction h. exists (ptd_alg_map F X). apply ptd_alg_law. - easy. - now intros [X h]; induction h. 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.