Lemma mweak_slice_as_bind_slice_agrees (Γ1: HSET_over_sort) {Γ2: HSET_over_sort} (M: wellsorted_in Γ2) : mweak_slice_as_bind_slice Γ1 Γ2 M = mweak_slice Γ1 Γ2 M. Proof. unfold mweak_slice_as_bind_slice, mweak_slice. unfold bind_slice, mweak_instantiated. apply (maponpaths (λ f, f M)). apply maponpaths. unfold mweak, bind_instantiated. apply maponpaths. now apply eq_mor_slicecat. Qed.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Slice. Require Import UniMath.CategoryTheory.slicecat.