Theorem free_ptd_alg_forgetful_form_adjunction : form_adjunction free_ptd_alg (forget_ptd_alg F) free_ptd_alg_unit free_ptd_alg_counit. Proof. split; red. + intro A. apply ptd_alg_mor_eq, pathsinv0; simpl. apply colim_endo_is_identity. intros i. rewrite assoc. rw_left_comp (free_ptd_alg_mor_restricts (colimIn (CC A) 0) i). rewrite <- assoc. rw_right_comp (free_ptd_alg_counit_map_restricts (free_ptd_alg_ob A) i). set (ɛ := free_ptd_alg_counit_cocone_arrows). induction i; simpl. { apply id_right. } rewrite assoc, <- functor_comp. apply (transportb (λ x, # F x · _ = _) IHi). apply shift_iter_map_restricts. + intro X. simpl. apply (free_ptd_alg_counit_map_restricts X 0). 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.