Theorem fusion_law : Φ μF (It X L IL HL ψ) = It X' L' IL' HL' ψ'. Proof. apply path_to_ctr. assert (Φ_is_nat := nat_trans_ax Φ). assert (Φ_is_nat_inst1 := Φ_is_nat _ _ inF). assert (Φ_is_nat_inst2 := eqtohomot Φ_is_nat_inst1 (It X L IL HL ψ)). unfold compose in Φ_is_nat_inst2; simpl in Φ_is_nat_inst2. simpl. rewrite <- Φ_is_nat_inst2. assert (H_inst := eqtohomot H (It X L IL HL ψ)). unfold compose in H_inst; simpl in H_inst. rewrite <- H_inst. apply maponpaths. rewrite It_is_preIt. apply preIt_ok. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.Adamek. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.whiskering.