Definition mexch_slice_as_bind_slice {Γ1 Γ2 Γ3: HSET_over_sort} (M: wellsorted_in (Γ1 ⊕ (Γ2 ⊕ Γ3))) : wellsorted_in (Γ2 ⊕ (Γ1 ⊕ Γ3)). Proof. unfold BinCoproductObject in M. simpl in M. set (a1 := BinCoproductIn1 (BinCoproductsHSET _ _) · BinCoproductIn2 (BinCoproductsHSET _ _): HSET⟦pr1 Γ1, pr1(Γ2 ⊕ (Γ1 ⊕ Γ3))⟧). set (a21 := BinCoproductIn1 (BinCoproductsHSET _ _): HSET⟦pr1 Γ2, pr1(Γ2 ⊕ (Γ1 ⊕ Γ3))⟧). set (a22 := BinCoproductIn2 (BinCoproductsHSET _ _) · BinCoproductIn2 (BinCoproductsHSET _ _): HSET⟦pr1 Γ3, pr1(Γ2 ⊕ (Γ1 ⊕ Γ3))⟧). use (bind_slice ((BinCoproductArrow _ a1 (BinCoproductArrow _ a21 a22)) · η_slice(Γ:=Γ2 ⊕ (Γ1 ⊕ Γ3))) _ M). intro x. induction x as [x1 | x2]. + unfold BinCoproductArrow. simpl. unfold compose. simpl. now rewrite η_slice_ok. + induction x2 as [x21 | x22]. * unfold BinCoproductArrow. simpl. unfold compose. simpl. now rewrite η_slice_ok. * unfold BinCoproductArrow. simpl. unfold compose. 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.