Lemma subst_interchange_law_slice {Γ : SET_over_sort} (L : wellsorted_in Γ) (N : wellsorted_in (sorted_option_functor (sort_in L) Γ)) (M : wellsorted_in (sorted_option_functor (sort_in N) (sorted_option_functor (sort_in L) Γ))) : subst_slice L (subst_slice N M) = subst_slice_eqn (subst_slice L N) (subst_slice_eqn (mweak_slice _ _ L) (mexch_slice M) (mweak_slice_ok _ L)) (subst_slice_ok L N). Proof. set (ls := subst_slice L (subst_slice N M)). set (rs1 := subst_slice_eqn (mweak_slice _ _ L) (mexch_slice M) (mweak_slice_ok _ L)). set (rs2 := subst_slice L N). simpl in rs1. Admitted. *) Context {Γ : HSET_over_sort} (L : wellsorted_in Γ) (N : wellsorted_in (sorted_option_functor (sort_in L) Γ)) (M : wellsorted_in (sorted_option_functor (sort_in N) (sorted_option_functor (sort_in L) Γ))). Local Definition LHS : wellsorted_in Γ := subst_slice L (subst_slice N M). Local Definition RHS : wellsorted_in Γ := subst_slice_eqn (subst_slice L N) (subst_slice_eqn (mweak_slice_as_bind_slice _ _ L) (mexch_slice M) (mweak_slice_as_bind_slice_ok _ L)) (subst_slice_ok L N). Local Lemma same_sort_LHS_RHS : sort_in LHS = sort_in RHS. Proof. unfold LHS. rewrite subst_slice_ok. rewrite subst_slice_ok. unfold RHS. do 2 rewrite subst_slice_eqn_ok. apply pathsinv0. apply mexch_slice_ok. 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.