fact: Definition comp_pred {a b c : C} : a ⇒ b → b ⇒ c → a ⇒ c → hProp := λ f g fg, make_hProp (compose f g = fg) (hsC _ _ _ _ ).
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.CategoryTheory.Core.Categories UniMath.Folds.folds_precat