proposition: Theorem fusion_law : Φ μF (It X L IL HL ψ) = It X' L' IL' HL' ψ'.
proof: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.Adamek UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.whiskering