fact: Definition comppathcomphom {X Y : UU} {f g h : X → Y} (p : f = g) (q : g = h) : ∏ x : X, (homotcomp (toforallpaths _ f g p) (toforallpaths _ g h q)) x = toforallpaths _ f h (pathscomp0 p q) x.
imports: UniMath.Foundations.All UniMath.Induction.PolynomialFunctors UniMath.CategoryTheory.Core.Functors UniMath.Induction.FunctorAlgebras_legacy