{-# OPTIONS --cubical --safe #-}

module Semirings where

open import Cubical.Foundations.Prelude

record Semiring a : Set (ℓ-suc a) where
  infixl  _+_
  infixl  _*_
  field
    R : Set a
    _+_ : R → R → R
    _*_ : R → R → R
    0# : R
    1# : R
    +-assoc : ∀ x y z → (x + y) + z ≡ x + (y + z)
    *-assoc : ∀ x y z → (x * y) * z ≡ x * (y * z)
    *0 : ∀ x → x * 0# ≡ 0#
    0* : ∀ x → 0# * x ≡ 0#
    0+ : ∀ x → 0# + x ≡ x
    *1 : ∀ x → x * 1# ≡ x
    1* : ∀ x → 1# * x ≡ x
    +-comm : ∀ x y → x + y ≡ y + x
    *⟨+⟩ : ∀ x y z → x * (y + z) ≡ x * y + x * z
    ⟨+⟩* : ∀ x y z → (x + y) * z ≡ x * z + y * z
    sIsSet : isSet R
  +0 : ∀ x → x + 0# ≡ x
  +0 x = +-comm x 0# ∙ 0+ x

record IdempotentSemiring a : Set (ℓ-suc a) where
  field
    semiring : Semiring a
  open Semiring semiring public
  field
    idem : ∀ x → x + x ≡ x