proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.SIP UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Core.Univalence