\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 = id
  | imul-assoc : imul ∘ prodMap imul id = imul ∘ prodMap id 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 = id
  | iadd-assoc : iadd ∘ prodMap iadd id = iadd ∘ prodMap id iadd ∘ associator
  | iadd-comm : iadd ∘ pair proj2 proj1 = iadd
  | inegative-left : iadd ∘ pair inegative id = izro ∘ terminalMap

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