Lemma Church_gen_body_sortToSet_data_ok (n : nat) (ξ ξ' : sortToSet) (f : sortToSet ⟦ ξ, ξ' ⟧) : Church_gen_body_sortToSet_data n ξ · # (pr1 Church_gen_body_target) f = Church_gen_body_sortToSet_data n ξ'. Proof. induction n. - apply nat_trans_eq; try apply HSET. intros s. apply funextfun. intros one. cbn in one. induction one. etrans. 2: { apply pathsinv0, (STLC_eta_gen_natural'_ppointwise _ _ (# (sorted_option_functorSet s) (# (sorted_option_functorSet (s ⇒ s)) f)) s (inl (idpath s,, tt))). } apply idpath. - apply nat_trans_eq; try apply HSET. intros s. apply funextfun. intros one. cbn in one. induction one. set (aux := (λ (s0 : path_pregroupoid sort Hsort) (_ : pr1 (pr1 (pr1 TsortToSet) s0)), Church_gen_body s0 (S n) ξ) : ∏ x : path_pregroupoid sort Hsort, SET ⟦ pr1 (pr1 TsortToSet) x, pr1 (pr1 Church_gen_body_target ξ) x ⟧). match goal with |[ |- _ = ?rhs] => set (therhs := rhs) end. change (pr1 (# (pr1 Church_gen_body_target) f) s (aux s tt) = therhs). change (pr1 (# (pr1 Church_gen_body_target) f) s (Church_gen_body s (S n) ξ) = Church_gen_body s (S n) ξ'). do 2 rewrite Church_gen_body_rec_eq. clear aux therhs. assert (IHnpointwise : pr1 (# (pr1 Church_gen_body_target) f) s (Church_gen_body s n ξ) = Church_gen_body s n ξ'). { apply (toforallpaths _ _ _ (toforallpaths _ _ _ (maponpaths pr1 IHn) s) tt). } rewrite <- IHnpointwise. clear IHnpointwise. unfold Church_gen_body_target. unfold pr1. unfold Church_gen_body_target_data. unfold make_functor_data. unfold functor_on_morphisms at 4. unfold pr2. unfold nat_trans_functor_path_pregroupoid. unfold make_nat_trans. apply pathsinv0. unfold functor_on_morphisms at 7. unfold pr2. apply pathsinv0. etrans. match goal with |[ |- _ ?arg = _] => set (thearg := arg) end. use (maponpaths (fun x : SET ⟦ pr1 (pr1 STLC_gen (sorted_option_functorSet s (sorted_option_functorSet (s ⇒ s) ξ))) s, pr1 (pr1 STLC_gen (sorted_option_functorSet s (sorted_option_functorSet (s ⇒ s) ξ'))) s ⟧ => x thearg)). 2: { apply sortToSet2_comp_on_mor. } rewrite <- app_map_gen_natural_ppointwise. apply maponpaths. use dirprodeq; [unfold pr1 | unfold pr2]. + rewrite app_source_gen_mor_pr1. unfold pr1. use dirprodeq. * apply idpath. * unfold pr2. etrans. 2: { apply pathsinv0, (STLC_eta_gen_natural'_ppointwise _ _ (# (pr1 (sorted_option_functorSet s)) (# (pr1 (sorted_option_functorSet (s ⇒ s))) f)) (s ⇒ s) (inr (inl (idpath (s ⇒ s),, tt)))). } apply idpath. + apply app_source_gen_mor_pr2. 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.