proposition: Lemma η_slice_ok {Γ: HSET_over_sort} (a: pr1 (pr1 Γ)) : sort_in (η_slice(Γ:=Γ) a) = (pr2 Γ) a.
proof: Proof. unfold η_slice. set (H1 := pr2 ((Monads.η T) Γ)). simpl in H1. apply toforallpaths in H1. now rewrite H1. 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