Lemma ChurchInfinity_body_sortToC_data_ok (ξ ξ' : sortToC) (f : sortToC ⟦ξ,ξ'⟧) : ChurchInfinity_body_sortToC_data ξ · # (pr1 (Church_gen_body_target σcoind)) f = ChurchInfinity_body_sortToC_data ξ'. Proof. apply nat_trans_eq; try apply C. intros s. change (((((CoproductIn (idpath _) · BinCoproductIn1) · BinCoproductIn2) · pr1 (pr1 (STLC_eta_gen σcoind) (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) (s ⇒ s)) · pr1 (pr1 IterateInfinite (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) s) · pr1 (#(pr1 (Church_gen_body_target σcoind)) f) s = (((CoproductIn (idpath _) · BinCoproductIn1) · BinCoproductIn2) · pr1 (pr1 (STLC_eta_gen σcoind) (ctx_ext (ctx_ext ξ' (s ⇒ s)) s)) (s ⇒ s)) · pr1 (pr1 IterateInfinite (ctx_ext (ctx_ext ξ' (s ⇒ s)) s)) s). repeat rewrite assoc'. apply maponpaths. etrans. { do 3 apply maponpaths. assert (aux := nat_trans_ax IterateInfinite _ _ (# (sorted_option_functor sort Hsort C TC BC CC s) (# (sorted_option_functor sort Hsort C TC BC CC (s ⇒ s)) f))). apply pathsinv0, (nat_trans_eq_weq C _ _ aux). } etrans. { do 3 apply maponpaths. exact (sortToC_comp (# (pr1 corecsource) (# (sorted_option_functor sort Hsort C TC BC CC s) (# (sorted_option_functor sort Hsort C TC BC CC (s ⇒ s)) f))) (pr1 IterateInfinite (sorted_option_functor sort Hsort C TC BC CC s (sorted_option_functor sort Hsort C TC BC CC (s ⇒ s) ξ'))) s). } repeat rewrite assoc. apply cancel_postcomposition. etrans. { repeat rewrite assoc'. do 2 apply maponpaths. apply pathsinv0. exact (STLC_eta_gen_natural'_pointwise σcoind _ _ (# (sorted_option_functor sort Hsort C TC BC CC s) (# (sorted_option_functor sort Hsort C TC BC CC (s ⇒ s)) f)) (s ⇒ s)). } repeat rewrite assoc. apply cancel_postcomposition. etrans. { rewrite assoc'. apply maponpaths. apply BinCoproductIn2Commutes. } simpl. rewrite assoc. etrans. { apply cancel_postcomposition. apply BinCoproductIn1Commutes. } rewrite (id_left(C:=sortToC)). apply idpath. 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.