\import Category
\import Category.Limit
\open PrecatWithBprod
\open PrecatWithTerminal
\class BaseObject {C : CartesianPrecat} (E : C)

\class CMonoidObject \extends BaseObject
  | iide : Hom terminal.apex E
  | imul : Hom (Bprod E E) E
  | iide-left : imul ∘ pair (iide ∘ terminalMap) (id E) = id E
  | imul-assoc : imul ∘ prodMap imul (id E) = imul ∘ prodMap (id E) imul ∘ associator
  | imul-comm : imul ∘ pair proj2 proj1 = imul

\class AbGroupObject \extends BaseObject
  | izro : Hom terminal.apex E
  | iadd : Hom (Bprod E E) E
  | inegative : Hom E E
  | izro-left : iadd ∘ pair (izro ∘ terminalMap) (id E) = id E
  | iadd-assoc : iadd ∘ prodMap iadd (id E) = iadd ∘ prodMap (id E) iadd ∘ associator
  | iadd-comm : iadd ∘ pair proj2 proj1 = iadd
  | inegative-left : iadd ∘ pair inegative (id E) = izro ∘ terminalMap

\class CRingObject \extends AbGroupObject, CMonoidObject
  | ildistr : imul ∘ prodMap (id E) iadd = iadd ∘ prodMap imul imul ∘ pair (prodMap (id E) proj1) (prodMap (id E) proj2)