Lemma old_Church_gen_sortToSet_data_ok (n : nat) (ξ ξ' : sortToSet) (f : sortToSet ⟦ ξ, ξ' ⟧): old_Church_gen_sortToSet_data n ξ · # (pr1 (functor_compose STLC_gen (projSortToSetvariable (λ s : sort, (s ⇒ s) ⇒ s ⇒ s)))) f = old_Church_gen_sortToSet_data n ξ'. Proof. apply nat_trans_eq; try apply HSET. intros s. apply funextfun. intros one. cbn in one. induction one. simpl. unfold compose. simpl. induction n. - change (pr1 (# (pr1 STLC_gen) f) ((s ⇒ s) ⇒ s ⇒ s) (ChurchZero_gen s ξ) = ChurchZero_gen s ξ'). unfold ChurchZero_gen. rewrite <- lam_map_gen_natural_ppointwise. apply maponpaths. use dirprodeq. + apply idpath. + unfold pr2. etrans. { apply lam_source_gen_mor_pr2. } unfold pr2. etrans. { apply postcomp_with_projSortToSet_on_mor. } unfold functor_compose. etrans. match goal with |[ |- _ ?arg = _] => set (thearg := arg) end. use (maponpaths (fun x : SET ⟦ pr1 (pr1 (sorted_option_functorSet (s ⇒ s) ∙ STLC_gen) ξ) (s ⇒ s), pr1 (pr1 (sorted_option_functorSet (s ⇒ s) ∙ STLC_gen) ξ') (s ⇒ s) ⟧ => x thearg)). 2: { apply sortToSet2_comp_on_mor. } etrans. { apply pathsinv0, lam_map_gen_natural_ppointwise. } apply maponpaths. use dirprodeq. * apply idpath. * unfold pr2. etrans. { apply lam_source_gen_mor_pr2. } unfold pr2. etrans. { apply postcomp_with_projSortToSet_on_mor. } etrans. match goal with |[ |- _ ?arg = _] => set (thearg := arg) end. use (maponpaths (fun x : SET ⟦ pr1 (pr1 (functor_compose (sorted_option_functorSet s) STLC_gen) (pr1 (sorted_option_functorSet (s ⇒ s)) ξ)) s, pr1 (pr1 (functor_compose (sorted_option_functorSet s) STLC_gen) (pr1 (sorted_option_functorSet (s ⇒ s)) ξ')) s ⟧ => x thearg)). 2: { apply sortToSet2_comp_on_mor. } etrans. { apply pathsinv0, STLC_eta_gen_natural'_ppointwise. } apply maponpaths. apply idpath. - induction n. + change (pr1 (# (pr1 STLC_gen) f) ((s ⇒ s) ⇒ s ⇒ s) (ChurchOne_gen s ξ) = ChurchOne_gen s ξ'). unfold ChurchOne_gen. rewrite <- lam_map_gen_natural_ppointwise. apply maponpaths. use dirprodeq. * apply idpath. * unfold pr2. etrans. { apply lam_source_gen_mor_pr2. } unfold pr2. etrans. { apply postcomp_with_projSortToSet_on_mor. } unfold functor_compose. etrans. match goal with |[ |- _ ?arg = _] => set (thearg := arg) end. use (maponpaths (fun x : SET ⟦ pr1 (pr1 (sorted_option_functor sort Hsort SET TerminalHSET BinCoproductsHSET CoproductsHSET (s ⇒ s) ∙ STLC_gen) ξ) (s ⇒ s), pr1 (pr1 (sorted_option_functor sort Hsort SET TerminalHSET BinCoproductsHSET CoproductsHSET (s ⇒ s) ∙ STLC_gen) ξ') (s ⇒ s) ⟧ => x thearg)). 2: { apply sortToSet2_comp_on_mor. } rewrite <- lam_map_gen_natural_ppointwise. apply maponpaths. use dirprodeq. -- apply idpath. -- unfold pr2. etrans. { apply lam_source_gen_mor_pr2. } unfold pr2. etrans. { apply postcomp_with_projSortToSet_on_mor. } unfold functor_compose. etrans. match goal with |[ |- _ ?arg = _] => set (thearg := arg) end. use (maponpaths (fun x : SET ⟦ pr1 (pr1 (sorted_option_functorSet s ∙ STLC_gen) (pr1 (sorted_option_functorSet (s ⇒ s)) ξ)) s, pr1 (pr1 (sorted_option_functorSet s ∙ STLC_gen) (pr1 (sorted_option_functorSet (s ⇒ s)) ξ')) s ⟧ => x thearg)). 2: { apply sortToSet2_comp_on_mor. } rewrite <- app_map_gen_natural_ppointwise. apply maponpaths. use dirprodeq; [unfold pr1 | unfold pr2]. ++ rewrite app_source_gen_mor_pr1. unfold pr1. use dirprodeq. --- apply idpath. --- unfold pr2. etrans. 2: { apply pathsinv0, (STLC_eta_gen_natural'_ppointwise _ _ (# (sorted_option_functorSet s) (# (sorted_option_functorSet (s ⇒ s)) f)) (s ⇒ s) (inr (inl (idpath (s ⇒ s),, tt)))). } apply idpath. ++ rewrite app_source_gen_mor_pr2. unfold pr2. use dirprodeq. --- apply idpath. --- unfold pr2. etrans. 2: { apply pathsinv0, (STLC_eta_gen_natural'_ppointwise _ _ (# (sorted_option_functorSet s) (# (sorted_option_functorSet (s ⇒ s)) f)) s (inl (idpath s,, tt))). } apply idpath. + admit. Abort. (* Definition old_Church_gen_sortToSet (n : nat) : global_element TsortToSet2 (functor_compose STLC_gen (projSortToSetvariable (fun s => (s ⇒ s) ⇒ (s ⇒ s)))). Proof. use make_global_element_functor_precat. - exact (old_Church_gen_sortToSet_data n). - exact (old_Church_gen_sortToSet_data_ok n). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. 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.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.