fact: Definition isbinopfun_twooutof3b {A B C : setwithbinop} (f : A -> B) (g : B -> C) (H : issurjective f) : isbinopfun (g ∘ f)%functions -> isbinopfun f -> isbinopfun g.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions