Lemma bind_η_slice {A1: hSet}{f1: A1 -> sort} (H: forall a1:A1, sort_in (η_slice(Γ:=(A1,,f1)) a1) = f1 a1) (M: wellsorted_in (A1,,f1)) : bind_slice (η_slice(Γ:=(A1,,f1))) H M = M. Proof. unfold bind_slice, η_slice. unfold bind_instantiated. assert (H1 : aux_fh (λ a:A1, pr1 ((Monads.η T) (A1,, f1)) a) H = (Monads.η T) (A1,, f1)). + unfold aux_fh. now apply eq_mor_slicecat. + intermediate_path (pr1 (bind ((Monads.η T) (A1,, f1))) M). * apply (maponpaths (λ f, f M)). apply maponpaths. apply maponpaths. exact H1. * now rewrite bind_η. 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.