proposition: Lemma mexch_slice_as_bind_slice_agrees {Γ1 Γ2 Γ3: HSET_over_sort} (M : wellsorted_in (Γ1 ⊕ (Γ2 ⊕ Γ3))) : mexch_slice_as_bind_slice M = mexch_slice M.
proof: Proof. unfold mexch_slice_as_bind_slice, mexch_slice. unfold bind_slice, mexch_instantiated. apply (maponpaths (λ f, f M)). apply maponpaths. unfold mexch, bind_instantiated. apply maponpaths. now apply eq_mor_slicecat. 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