proposition: Lemma subst_slice_as_bind_slice_agrees {Γ: HSET_over_sort} (N : wellsorted_in Γ) (M : wellsorted_in (sorted_option_functor (sort_in N) Γ)) : subst_slice_as_bind_slice N M =subst_slice N M.
proof: Proof. unfold subst_slice_as_bind_slice, subst_slice. unfold bind_slice, monadSubstGen_instantiated. apply (maponpaths (λ f, f M)). apply maponpaths. unfold monadSubstGen, 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