Definition IterateInfinite_rec_coalg_data_data (ξ : sortToC) (s : sort) : C⟦pr1 (pr1 corecsource ξ) s, pr1 (pr1 (STLC_Functor_Id_H (BCsortToC2 corecsource STLC_coind)) ξ) s⟧. Proof. refine (_ · BinCoproductIn2 _). refine (_ · CoproductIn _ _ _ (ii1 (s,,s))). use BinProductArrow. - refine (_ · CoproductIn _ _ _ (idpath _)). change (C ⟦ pr1 (pr1 corecsource ξ) s, pr1 (pr111 (BCsortToC2 corecsource STLC_coind) ξ) (s ⇒ s)⟧). apply BinCoproductIn2. - refine (_ · CoproductIn _ _ _ (idpath _)). change (C ⟦ pr1 (pr1 corecsource ξ) s, pr1 (pr111 (BCsortToC2 corecsource STLC_coind) ξ) s⟧). apply BinCoproductIn1. Defined.
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.