Definition Thm47 : statement_Thm47. Proof. red. set (Mendler := GenMendlerIteration OC chC (leftwhiskering_functor F d) (omegaF d) a J OJ omegaJ). transparent assert (ψ : (ψ_source a J ⟹ ψ_target (leftwhiskering_functor F d) a J)). { use make_nat_trans. - intros y f. cbn; red. exact (h d y · (K d) ⊗^{G}_{l} f · α). - intros y y' f. cbn in f. apply funextsec. intro g. cbn in g. red in g. cbn. repeat rewrite assoc. apply cancel_postcomposition. rewrite bifunctor_leftcomp. rewrite assoc. apply cancel_postcomposition. apply pathsinv0, (pr12 h). } set (Mendlerinst := Mendler ψ). use tpair. - exists (pr11 Mendlerinst). apply pathsinv0. exact (pr21 Mendlerinst). - intro t. induction t as [β βeq]. assert (Mendlerinst2 := pr2 Mendlerinst (β,,!βeq)). use subtypePath. { intro g. apply A. } apply (maponpaths pr1) in Mendlerinst2. etrans. { exact Mendlerinst2. } apply idpath. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.Adamek. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.SubstitutionSystems.GenMendlerIteration_alt. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import BifunctorNotations.