proposition: Lemma bind_slice_ok {A1: hSet} {f1: A1->sort} {Γ2: HSET_over_sort} (f : A1 -> wellsorted_in Γ2) (H: forall a1:A1, sort_in (f a1) = f1 a1) (M: wellsorted_in (A1,,f1)) : sort_in (bind_slice f H M) = sort_in M.
proof: Proof. assert (H1 := pr2 (bind_instantiated (aux_fh f H))). apply toforallpaths in H1. apply pathsinv0. now rewrite H1. 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