Lemma IterateInfinite_rec_coalg_data_ok : is_nat_trans _ _ IterateInfinite_rec_coalg_data. Proof. intros ξ ξ' f. apply nat_trans_eq; try apply C. intro s. change (pr1 (# (pr1 corecsource) f · IterateInfinite_rec_coalg_data ξ') s = pr1 (IterateInfinite_rec_coalg_data ξ · # (pr1 (STLC_Functor_Id_H (BCsortToC2 corecsource STLC_coind))) f) s). change (pr1 (# (pr1 STLC_coind) f) (s ⇒ s) · IterateInfinite_rec_coalg_data_data ξ' s = IterateInfinite_rec_coalg_data_data ξ s · pr1 (# (pr1 (STLC_Functor_Id_H ((BCsortToC2 corecsource STLC_coind) : sortToC2))) f) s). unfold IterateInfinite_rec_coalg_data_data. etrans. 2: { repeat rewrite assoc'. do 2 apply maponpaths. apply pathsinv0. apply BinCoproductOfArrowsIn2. } repeat rewrite assoc. apply cancel_postcomposition. etrans. 2: { repeat rewrite assoc'. apply maponpaths. apply pathsinv0. refine (CoproductOfArrowsIn _ _ _ _ _ (inl (s,, s))). } repeat rewrite assoc. apply cancel_postcomposition. match goal with |[ |- _ =_ · ?sndmor] => set (thesndmor := sndmor) end. change thesndmor with (BinProductOfArrows _ (BP) (BP) (pr1 (# (hat_functorC s) (pr1 (# (pr1 ((BCsortToC2 corecsource STLC_coind) : sortToC2)) f) (s ⇒ s))) s) (pr1 (# (hat_functorC s) (pr1 (# (pr1 ((BCsortToC2 corecsource STLC_coind) : sortToC2)) f) s)) s)). etrans. 2: { apply pathsinv0, postcompWithBinProductArrow. } etrans. { apply precompWithBinProductArrow. } apply maponpaths_12. - etrans. 2: { rewrite assoc'. apply maponpaths, pathsinv0. use (CoproductOfArrowsIn _ _ _ _ _ (idpath s)). } repeat rewrite assoc. apply cancel_postcomposition. apply pathsinv0, BinCoproductOfArrowsIn2. - etrans. 2: { rewrite assoc'. apply maponpaths, pathsinv0. use (CoproductOfArrowsIn _ _ _ _ _ (idpath s)). } repeat rewrite assoc. apply cancel_postcomposition. apply pathsinv0, BinCoproductOfArrowsIn1. 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.