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