proposition: Lemma mweak_slice_as_bind_slice_ok (Γ1: HSET_over_sort) {Γ2: HSET_over_sort} (M: wellsorted_in Γ2) : sort_in (mweak_slice_as_bind_slice Γ1 Γ2 M) = sort_in M.
proof: Proof. rewrite mweak_slice_as_bind_slice_agrees; apply mweak_slice_ok. 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