fact: Definition make_hom {σ: signature} {A1 A2: algebra σ} {f: sfun A1 A2} (is: ishom f): A1 ↷ A2 := f ,, is.
imports: UniMath.Foundations.All UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Signatures