Require Export ring.
Require Export module.
Require Export make_small_cat.
Module Small_Cat_of_Ring : A_Cat_ := (Make_Small_Cat Ring).
Test |
Module My_Ring : Coeff_Sig.
Definition R := R.
End My_Ring.
Module My_Module_Cat := (Module_Cat My_Ring).
Module My_Small_Module_Cat : A_Cat_ :=
(Make_Small_Cat My_Module_Cat).