Lemma Church_gen_body_sortToC_data_ok (n : nat) (ξ ξ' : sortToC) (f : sortToC ⟦ ξ, ξ' ⟧) : Church_gen_body_sortToC_data n ξ · # (pr1 Church_gen_body_target) f = Church_gen_body_sortToC_data n ξ'. Proof. induction n. - apply nat_trans_eq; try apply C. intros s. unfold Church_gen_body_sortToC_data. Opaque Church_gen_body Church_gen_body_target. simpl. etrans. 2: { rewrite Church_gen_body_zero. rewrite assoc'. apply maponpaths. apply pathsinv0. assert (aux := STLC_eta_gen_natural'_pointwise _ _ (# (sorted_option_functor sort Hsort C TC BC CC s) (# (sorted_option_functor sort Hsort C TC BC CC (s ⇒ s)) f)) s). apply (maponpaths (fun x => BinCoproductIn1 · x)) in aux. rewrite assoc in aux. match goal with |[ H : ?auxleft = _ |- _ ] => set (theauxleft := auxleft) end. intermediate_path theauxleft. + unfold theauxleft. apply cancel_postcomposition. unfold sorted_option_functor. unfold constcoprod_functor1. etrans. 2: { apply pathsinv0, BinCoproductIn1Commutes. } apply pathsinv0, id_left. + exact aux. } repeat rewrite assoc. apply idpath. - apply nat_trans_eq; try apply C. intros s. change (Church_gen_body s (S n) ξ · pr1 (# (pr1 Church_gen_body_target) f) s = Church_gen_body s (S n) ξ'). do 2 rewrite Church_gen_body_rec_eq. assert (IHnpointwise : Church_gen_body s n ξ · pr1 (# (pr1 Church_gen_body_target) f) s = Church_gen_body s n ξ') by apply (toforallpaths _ _ _ (maponpaths pr1 IHn) s). rewrite <- IHnpointwise. clear IHnpointwise. Transparent Church_gen_body_target. unfold Church_gen_body_target. unfold pr1. unfold Church_gen_body_target_data. unfold make_functor_data. unfold functor_on_morphisms at 7. unfold pr2. unfold make_sortToC_mor, nat_trans_functor_path_pregroupoid. unfold make_nat_trans. apply pathsinv0. unfold functor_on_morphisms at 13. unfold pr2. apply pathsinv0. etrans. { rewrite assoc'. apply maponpaths, pathsinv0, app_map_gen_natural_pointwise. } rewrite assoc. apply cancel_postcomposition. etrans. { etrans. { apply maponpaths. apply app_source_gen_mor_eq. } apply postcompWithBinProductArrow. } apply maponpaths_12. + assert (aux := STLC_eta_gen_natural'_pointwise _ _ (# (sorted_option_functor sort Hsort C TC BC CC s) (# (sorted_option_functor sort Hsort C TC BC CC (s ⇒ s)) f)) (s ⇒ s)). apply (maponpaths (fun x => BinCoproductIn1 · BinCoproductIn2 · x)) in aux. rewrite assoc in aux. etrans. 2: { apply cancel_postcomposition. do 2 rewrite assoc'. apply maponpaths. rewrite assoc. apply pathsinv0. match goal with |[ H : ?auxleft = _ |- _ ] => set (theauxleft := auxleft) end. intermediate_path theauxleft. * unfold theauxleft. apply cancel_postcomposition. rewrite assoc'. etrans. 2: { apply maponpaths. unfold sorted_option_functor. unfold constcoprod_functor1. apply pathsinv0. unfold compose. unfold functor_on_morphisms, make_functor_data. unfold make_sortToC_mor, nat_trans_functor_path_pregroupoid, make_nat_trans, nat_trans_data_from_nat_trans_funclass. apply BinCoproductIn2Commutes. } simpl. apply pathsinv0. rewrite assoc. apply cancel_postcomposition. etrans. { apply BinCoproductIn1Commutes. } rewrite (id_left(C:=sortToC)). apply idpath. * exact aux. } repeat rewrite assoc'. do 4 apply maponpaths. simple refine (CoproductOfArrowsIn (s=s) _ _ _ _ _). + repeat rewrite assoc'. apply maponpaths. simple refine (CoproductOfArrowsIn (s=s) _ _ _ _ _). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.PartA. 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.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. 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.