proposition: Lemma bind_η_slice {A1: hSet}{f1: A1 -> sort} (H: forall a1:A1, sort_in (η_slice(Γ:=(A1,,f1)) a1) = f1 a1) (M: wellsorted_in (A1,,f1)) : bind_slice (η_slice(Γ:=(A1,,f1))) H M = M.
proof: Proof. unfold bind_slice, η_slice. unfold bind_instantiated. assert (H1 : aux_fh (λ a:A1, pr1 ((Monads.η T) (A1,, f1)) a) H = (Monads.η T) (A1,, f1)). + unfold aux_fh. now apply eq_mor_slicecat. + intermediate_path (pr1 (bind ((Monads.η T) (A1,, f1))) M). * apply (maponpaths (λ f, f M)). apply maponpaths. apply maponpaths. exact H1. * now rewrite bind_η. Qed.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Slice UniMath.CategoryTheory.slicecat