Lemma subst_slice_eqn_ok {Γ: HSET_over_sort} (N : wellsorted_in Γ) {s : sort} (M : wellsorted_in (sorted_option_functor s Γ)) (H: sort_in N = s) : sort_in (subst_slice_eqn N M H) = sort_in M. Proof. unfold subst_slice_eqn. rewrite subst_slice_ok. now induction H. 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.