Lemma bind_bind_slice {A1: hSet} {f1: A1 -> sort} {A2: hSet} {f2: A2 -> sort} {Γ3: HSET_over_sort} (f : A1 -> wellsorted_in (A2,,f2)) (H1: forall a1:A1, sort_in (f a1) = f1 a1) (g : A2 -> wellsorted_in Γ3) (H2: forall a2:A2, sort_in (g a2) = f2 a2) (HH: forall a1:A1, sort_in (bind_slice g H2 (f a1)) = f1 a1) (M: wellsorted_in (A1,,f1)) : bind_slice g H2 (bind_slice f H1 M) = bind_slice (λ a1:A1, bind_slice g H2 (f a1)) HH M. Proof. unfold bind_slice. intermediate_path (pr1 (bind_instantiated (aux_fh f H1) · bind_instantiated (aux_fh g H2)) M). + apply idpath. + apply (maponpaths (λ f, f M)). apply maponpaths. unfold bind_instantiated. rewrite bind_bind. 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.