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