proposition: Lemma isaset_ringfun (X Y : ring) : isaset (ringfun X Y).
proof: Proof. apply (isofhleveltotal2 2). - use impred_isaset. intro x. apply setproperty. - intro f. apply isasetaprop. apply isapropisrigfun. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids