Definition kernel_ideal {R S : rig} (f : rigfun R S) : @ideal R. Proof. use make_ideal. - use make_submonoid. + exact (@monoid_kernel_hsubtype (rigaddabmonoid R) (rigaddabmonoid S) (rigaddfun f)). + apply kernel_issubmonoid. - intros r s ss; cbn in *. refine (monoidfunmul (rigmultfun f) _ _ @ _); cbn. refine (maponpaths _ ss @ _). refine (rigmultx0 _ (pr1 f r) @ _). reflexivity. - intros r s ss; cbn in *. refine (monoidfunmul (rigmultfun f) _ _ @ _); cbn. abstract (rewrite ss; refine (rigmult0x _ (pr1 f r) @ _); reflexivity). Defined.
Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.MoreFoundations.Notations.