Lemma subst_interchange_law_gen (c b a : C) (e : C⟦c,T (b ⊕ a)⟧) (f : C⟦b,T a⟧): (monadSubstGen _ e) · (monadSubstGen _ f) = (mexch c b a) · (monadSubstGen _ (f · (mweak c a))) · (monadSubstGen _ (e · (monadSubstGen _ f))). Proof. unfold monadSubstGen, mexch. do 3 rewrite bind_bind. apply maponpaths. apply BinCoproductArrowsEq. + do 4 rewrite assoc. do 2 rewrite BinCoproductIn1Commutes. rewrite <- assoc. rewrite bind_bind. rewrite <- assoc. rewrite (η_bind(a:=let (pr1, _) := pr1 (BC b (c ⊕ a)) in pr1)). rewrite <- assoc. apply pathsinv0. eapply pathscomp0. * apply cancel_precomposition. rewrite assoc. rewrite BinCoproductIn2Commutes. rewrite (η_bind(a:=(c ⊕ a))). apply idpath. * now rewrite BinCoproductIn1Commutes. + rewrite assoc. rewrite BinCoproductIn2Commutes. rewrite (η_bind(a:=b ⊕ a)). do 3 rewrite assoc. rewrite BinCoproductIn2Commutes. apply BinCoproductArrowsEq. * rewrite BinCoproductIn1Commutes. rewrite <- assoc. rewrite bind_bind. do 2 rewrite assoc. rewrite BinCoproductIn1Commutes. rewrite <- assoc. rewrite (η_bind(a:=let (pr1, _) := pr1 (BC b (c ⊕ a)) in pr1)). rewrite assoc. rewrite BinCoproductIn1Commutes. unfold mweak. rewrite <- assoc. rewrite bind_bind. apply pathsinv0. apply remove_id_right; try now idtac. rewrite <- bind_η. apply maponpaths. rewrite <- assoc. rewrite (η_bind(a:=let (pr1, _) := pr1 (BC c a) in pr1)). now rewrite BinCoproductIn2Commutes. * rewrite BinCoproductIn2Commutes. rewrite <- assoc. rewrite bind_bind. do 2 rewrite assoc. rewrite BinCoproductIn2Commutes. do 2 rewrite <- assoc. rewrite (η_bind(a:=let (pr1, _) := pr1 (BC b (c ⊕ a)) in pr1)). apply pathsinv0. eapply pathscomp0. - apply cancel_precomposition. rewrite assoc. rewrite BinCoproductIn2Commutes. rewrite (η_bind(a:=(c ⊕ a))). apply idpath. - now rewrite BinCoproductIn2Commutes. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Core.Univalence.