Theorem fusion_law : ∏ (C : category) (F : functor C C) (μF_Initial : Initial (category_FunctorAlg F)) (C' : category) (X X' : C') (L : functor C C') (is_left_adj_L : is_left_adjoint L) (ψ : ψ_source C C' X L ⟹ ψ_target C F C' X L) (L' : functor C C') (is_left_adj_L' : is_left_adjoint L') (ψ' : ψ_source C C' X' L' ⟹ ψ_target C F C' X' L') (Φ : yoneda_objects C' X • functor_opp L ⟹ yoneda_objects C' X' • functor_opp L'), let T:= (` (InitialObject μF_Initial)) in ψ T · Φ (F T) = Φ T · ψ' T → Φ T (It μF_Initial X L is_left_adj_L ψ) = It μF_Initial X' L' is_left_adj_L' ψ'. Proof. apply fusion_law. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.BinSumOfSignatures. Require Import UniMath.SubstitutionSystems.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.GenMendlerIteration. Require Import UniMath.CategoryTheory.RightKanExtension. Require Import UniMath.SubstitutionSystems.GenMendlerIteration. Require Import UniMath.SubstitutionSystems.LiftingInitial. Require Import UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems. Require Import UniMath.SubstitutionSystems.LamSignature. Require Import UniMath.SubstitutionSystems.Lam. Require Import UniMath.SubstitutionSystems.Notation.