Lemma ChurchInfinity_body_sortToC_rec_eq (ξ : sortToC) (s : sort) : ChurchInfinity_body_sortToC_rec_eq_statement ξ s. Proof. assert (aux := toforallpaths _ _ _ (maponpaths pr1 (toforallpaths _ _ _ (maponpaths pr1 IterateInfinite_rec_eq) (ctx_ext (ctx_ext ξ (s ⇒ s)) s))) s). red. change (ChurchInfinity_body ξ s) with (ChurchInfinity_body_sortToC_data_data ξ s). unfold ChurchInfinity_body_sortToC_data_data. etrans. { apply maponpaths. exact aux. } clear aux. unfold app_map_coind, app_map_gen, STLC_tau_gen. change (SigmaMonoid_τ θSTLC σcoind) with (@BinCoproductIn2 _ _ _ (BCsortToC2 _ _) · out_STLC_coind). match goal with |[ |- _ = _ · ?sndmor ] => set (thesndmor := sndmor) end. change thesndmor with (CoproductIn (inl (s,, s)) · (BinCoproductIn2 · pr1 (pr1 out_STLC_coind (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) s)). clear thesndmor. match goal with |[ |- _ · ?sndmor = _ ] => set (thesndmor := sndmor) end. change thesndmor with (pr1 (pr1 IterateInfinite_rec_coalg (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) s · pr1 (pr1 (# STLC_Functor_Id_H (BinCoproductArrow (BCsortToC2 corecsource STLC_coind) IterateInfinite (identity STLC_coind))) (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) s · pr1 (pr1 out_STLC_coind (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) s). clear thesndmor. repeat rewrite assoc. apply cancel_postcomposition. change (pr1 (pr1 IterateInfinite_rec_coalg (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) s) with (IterateInfinite_rec_coalg_data_data (ctx_ext (ctx_ext ξ (s ⇒ s)) s) s). unfold IterateInfinite_rec_coalg_data_data. Opaque IterateInfinite. etrans. { repeat rewrite assoc'. do 5 apply maponpaths. etrans. { apply maponpaths. apply BinCoproductIn2Commutes. } match goal with |[ |- _ · ?sndmor = _] => set (thesndmor := sndmor) end. change thesndmor with (pr1 (pr1 (# STLC_Functor_H (BinCoproductArrow (BCsortToC2 corecsource STLC_coind) IterateInfinite (identity STLC_coind))) (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) s · BinCoproductIn2(CC:=BC (pr1 (Id (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) s) (pr1 (pr1 (pr1 STLC_Functor_H STLC_coind) (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) s))). clear thesndmor. rewrite assoc. apply cancel_postcomposition. unfold STLC_Functor_H, MultiSorted_actegorical.MultiSortedSigToFunctor', ContinuityOfMultiSortedSigToFunctor.MultiSortedSigToFunctor'. etrans. { apply maponpaths. apply coproduct_of_functors_sortToC3_mor. } refine (CoproductOfArrowsIn _ _ _ _ _ (inl (s,, s))). } repeat rewrite assoc. do 2 apply cancel_postcomposition. match goal with |[ |- _ · ?sndmor = _] => set (thesndmor := sndmor) end. set (aux2 := BinProductOfArrows _ (BP) (BP) (CoproductOfArrows (s=s) C (CC (s=s) (Hsort s s) _) (CC (s=s) (Hsort s s) _) (fun _ => pr1 (pr1 (BinCoproductArrow (BCsortToC2 corecsource STLC_coind) IterateInfinite (identity STLC_coind)) (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) (s ⇒ s))) (CoproductOfArrows (s=s) C (CC (s=s) (Hsort s s) _) (CC (s=s) (Hsort s s) _) (fun _ => pr1 (pr1 (BinCoproductArrow (BCsortToC2 corecsource STLC_coind) IterateInfinite (identity STLC_coind)) (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) s))). change thesndmor with aux2. clear thesndmor. etrans. { repeat rewrite assoc'. do 4 apply maponpaths. apply postcompWithBinProductArrow. } clear aux2. etrans. { repeat rewrite assoc. apply precompWithBinProductArrow. } apply maponpaths_12. - repeat rewrite assoc'. do 4 apply maponpaths. etrans. { apply maponpaths. use (CoproductOfArrowsIn _ _ _ _ _ (idpath s)). } etrans. { rewrite assoc. apply cancel_postcomposition. match goal with |[ |- _ · ?sndmor = _] => set (thesndmor := sndmor) end. change thesndmor with (BinCoproductArrow (BC _ _) (pr1 (pr1 IterateInfinite (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) (s ⇒ s)) (pr1 (pr1 (identity STLC_coind) (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) (s ⇒ s))). apply BinCoproductIn2Commutes. } apply id_left. - repeat rewrite assoc'. do 4 apply maponpaths. etrans. { apply maponpaths. use (CoproductOfArrowsIn _ _ _ _ _ (idpath s)). } etrans. { rewrite assoc. apply cancel_postcomposition. match goal with |[ |- _ · ?sndmor = _] => set (thesndmor := sndmor) end. change thesndmor with (BinCoproductArrow (BC _ _) (pr1 (pr1 IterateInfinite (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) s) (pr1 (pr1 (identity STLC_coind) (ctx_ext (ctx_ext ξ (s ⇒ s)) s)) s)). apply BinCoproductIn1Commutes. } 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.