Lemma shift_iter_map_forms_ptd_alg (A : C) : is_ptd_alg F (make_ptd_alg_data F (F^ω A) (shift_iter_map A)). Proof. unfold is_ptd_alg; simpl. set (s := shift_iter_map A). apply pathsinv0, colim_endo_is_identity. intro i. rewrite assoc. rewrite point_naturality. rewrite <- assoc. rewrite shift_iter_map_restricts'. simpl. rewrite <- iter_chain_mor_is_point. apply (colimInCommutes (CC A) i (1+i) (idpath _)). 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.