open import Algebra using (Op₂)
import      Algebra.Definitions 
open import Level 
open import Relation.Binary using (Rel; IsEquivalence)


record Setoid α α= : Set (suc (α ⊔ α=)) where
  field
    Carrier       : Set α
    _≈_           : Rel Carrier α=
    isEquivalence : IsEquivalence _≈_

record IsMagma {α α=} (S : Setoid α α=) (_∙_ : Op₂ (Setoid.Carrier S)) :
                                                           Set (α ⊔ α=)
  where
  open Setoid S using (Carrier; _≈_)
  open Algebra.Definitions {A = Carrier} _≈_ using (Congruent₂)

  field ∙-cong : Congruent₂ _∙_
  
record Magma α α= : Set (suc (α ⊔ α=)) where
  field
    setoid : Setoid α α=

  open Setoid setoid public 

  field _∙_     : Op₂ Carrier
        isMagma : IsMagma setoid _∙_


record IsSemiring' {α α=} (+-magma : Magma α α=)
                          (_*_ : Op₂ (Magma.Carrier +-magma)) :
                                                    Set (α ⊔ α=) where
  open Magma +-magma using (Carrier; _≈_; setoid) 
  open Algebra.Definitions {A = Carrier} _≈_ using (_DistributesOver_)

  field *-isMagma   : IsMagma setoid _*_

        *-distrib-+ : _*_ DistributesOver _+_
                                     -- why is not it parsed?
--
-- A contrived version for Semiring
--
record Semiring' α α= :  Set (suc (α ⊔ α=)) where
  field
    +-magma : Magma α α=

  open Magma +-magma using (Carrier)

  field _*_         : Op₂ Carrier
        isSemiring' : IsSemiring' +-magma _*_