Definition make_folds_ob_mor (ob : UU)(mor : ob → ob → UU) : folds_ob_mor := tpair _ ob mor.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.