fact: Definition ptd_mor_commutes {F G : ptd_obj} (α : ptd_mor F G) : ∏ c : C, ptd_pt F c · α c = ptd_pt G c.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory