Definition subst_slice_as_bind_slice {Γ: HSET_over_sort} (N : wellsorted_in Γ) (M : wellsorted_in (sorted_option_functor (sort_in N) Γ)): wellsorted_in Γ. Proof. use (bind_slice (BinCoproductArrow (BinCoproductsHSET _ _) (λ _, N) (η_slice(Γ:=Γ))) _ M). abstract(intro a1; induction a1 as [u | a1]; [apply idpath | unfold BinCoproductArrow; simpl; now rewrite η_slice_ok]). Defined.
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.