Lemma Carrier_detype_data_coind_is_functor : is_functor Carrier_detype_data_coind. Proof. split ; red. - intro ξ. apply nat_trans_eq. { exact has_homsets_HSET. } intro x. apply funextfun. intro elem. unfold functor_on_morphisms. unfold Carrier_detype_data_coind. unfold make_functor_data. unfold nat_trans_functor_path_pregroupoid. unfold make_nat_trans. unfold nat_trans_data_from_nat_trans_funclass. unfold pr1. unfold pr2. change (Down_Context_on_mor (identity ξ)) with (# Down_Context_functor (identity ξ)). rewrite (functor_id). rewrite (functor_id UntypedForests.UntypedForest_coind). apply idpath. - intros ξ1 ξ2 ξ3 f g. apply nat_trans_eq. { exact has_homsets_HSET. } intro x. apply funextfun. intro elem. unfold functor_on_morphisms. unfold Carrier_detype_data_coind. unfold make_functor_data. unfold nat_trans_functor_path_pregroupoid. unfold make_nat_trans. unfold nat_trans_data_from_nat_trans_funclass. unfold pr1. unfold pr2. change (Down_Context_on_mor (f · g)) with (# Down_Context_functor (f · g)). rewrite functor_comp. rewrite (functor_comp UntypedForests.UntypedForest_coind). apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartB. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.FunctorCoalgebras. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.Cochains. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.SubstitutionSystems.SigmaMonoids. Require Import UniMath.SubstitutionSystems.MultiSortedBindingSig. Require Import UniMath.SubstitutionSystems.MultiSorted_alt. Require Import UniMath.SubstitutionSystems.MultiSorted_actegorical. Require Import UniMath.SubstitutionSystems.MultiSortedMonadConstruction_actegorical. Require Import UniMath.SubstitutionSystems.MultiSortedMonadConstruction_coind_actegorical. Require Import UniMath.SubstitutionSystems.ContinuitySignature.InstantiateHSET. Require Import UniMath.SubstitutionSystems.MultiSortedEmbeddingIndCoindHSET. Require Import UniMath.SubstitutionSystems.SortIndexing.