0 = y + - x <~> x = y := @grp_moveR_1M R x y. End RingMovement. Global Instance isgraph_ring : IsGraph Ring := Build_IsGraph _ RingHomomorphism. Global Instance is01cat_ring : Is01Cat Ring := Build_Is01Cat _ _ rng_homo_id (@rng_homo_compose). Global Instance is2graph_ring : Is2Graph Ring := fun A B => isgraph_induced (@rng_homo_map A B : _ -> (group_type _ $-> _)). Global Instance is01cat_ringhomomorphism {A B : Ring} : Is01Cat (A $-> B) := is01cat_induced (@rng_homo_map A B). Global Instance is0gpd_ringhomomorphism {A B : Ring} : Is0Gpd (A $-> B) := is0gpd_induced (@rng_homo_map A B). Global Instance is0functor_postcomp_ringhomomorphism {A B C : Ring} (h : B $-> C) : Is0Functor (@cat_postcomp Ring _ _ A B C h). Proof. apply Build_Is0Functor. intros [f ?] [g ?] p a ; exact (ap h (p a)). Defined.
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.