Library UniMath.Bicategories.DoubleCategories.DerivedLaws