Lemma Church_gen_body_target_data_ok : is_functor Church_gen_body_target_data. Proof. split; red. - intro ξ. apply nat_trans_eq; try apply HSET. intro s. apply funextfun. intro elem. unfold functor_on_morphisms. unfold Church_gen_body_target_data. unfold pr2. unfold make_functor_data. unfold nat_trans_functor_path_pregroupoid. unfold make_nat_trans. unfold nat_trans_data_from_nat_trans_funclass. unfold pr1. do 2 rewrite functor_id. rewrite (functor_id STLC_gen). apply idpath. - intros ξ1 ξ2 ξ3 f g. apply nat_trans_eq; try apply HSET. intro s. apply funextfun. intro elem. unfold functor_on_morphisms. unfold Church_gen_body_target_data. unfold make_functor_data. unfold nat_trans_functor_path_pregroupoid. unfold make_nat_trans. unfold pr2. unfold nat_trans_data_from_nat_trans_funclass. unfold pr1. do 2 rewrite functor_comp. rewrite (functor_comp STLC_gen). apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.Lists. 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.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.