Definition ChurchOne_gen (ξ : sortToC) : global_element TC (STLC_gen_ctx_sort ξ ((s ⇒ s) ⇒ (s ⇒ s))). Proof. refine (_ · pr1 (pr1 (lam_map_gen _ _) _) _). refine (_ · CoproductIn _ _ _ (idpath _)). refine (_ · pr1 (pr1 (lam_map_gen _ _) _) _). refine (_ · CoproductIn _ _ _ (idpath _)). refine (_ · pr1 (pr1 (app_map_gen s _) _) _). apply BinProductArrow; refine (_ · CoproductIn _ _ _ (idpath _)). - change (global_element TC (STLC_gen_ctx_sort (ctx_ext (ctx_ext ξ (s ⇒ s)) s) (s ⇒ s))). simple refine (_ · pr1 (pr1 STLC_eta_gen _) _). refine (_ · BinCoproductIn2 _). refine (_ · BinCoproductIn1 _). cbn. exact (CoproductIn _ _ _ (idpath _)). - change (global_element TC (STLC_gen_ctx_sort (ctx_ext (ctx_ext ξ (s ⇒ s)) s) s)). simple refine (_ · pr1 (pr1 STLC_eta_gen _) _). refine (_ · BinCoproductIn1 _). cbn. exact (CoproductIn _ _ _ (idpath _)). 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.