Lemma subst_interchange_law_instantiated {t s: sort} {Γ: HSET_over_sort} (NN: HSET_over_sort⟦constHSET_slice t, T (constHSET_slice s ⊕ Γ)⟧) (LL: HSET_over_sort⟦constHSET_slice s, T Γ⟧): (monadSubstGen_instantiated _ NN) · (monadSubstGen_instantiated _ LL) = (mexch_instantiated (Γ1:=constHSET_slice t) (Γ2:=constHSET_slice s) (Γ3:=Γ)) · (monadSubstGen_instantiated _ (LL · (mweak_instantiated _))) · (monadSubstGen_instantiated _ (NN · (monadSubstGen_instantiated _ LL))). Proof. apply subst_interchange_law_gen. 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.