Alternative Ring definition without extending duplicate hierarchy

alternativeRingDefinitionPoc.ard

\class Magma \extends BaseSet
  | \infixl 7 * : E -> E -> E

\class Monoid \extends Magma
  | ide : E
  | ide-left (x : E) : ide * x = x
  | ide-right (x : E) : x * ide = x
  | *-assoc (x y z : E) : (x * y) * z = x * (y * z)

-- Note that it does not extend Monoid
-- and that it's far from proper Ring definition :P

\class SomethingRingLike \extends BaseSet
  | additive-like : Monoid E
  | multiplicative-like : Monoid E
  | property-involving-both : multiplicative-like.ide = additive-like.ide -> Empty

-- and now Bool instances, just as a proof of concept

\instance or-Monoid : Monoid Bool
  | ide => false
  | * => Bool.or
  | ide-left _ => idp
  | ide-right (x : Bool) : (Bool.or x false = x) \elim x {
    | true => idp
    | false => idp
  }
  | *-assoc => Bool.orAssoc

\instance and-Monoid : Monoid Bool
  | ide => true
  | * => Bool.and
  | ide-left _ => idp
  | ide-right (x : Bool) : (Bool.and x true = x) \elim x {
    | true => idp
    | false => idp
  }
  | *-assoc => Bool.andAssoc

\instance Bool-SomethingRingLike : SomethingRingLike Bool
  | additive-like => or-Monoid
  | multiplicative-like => and-Monoid
  | property-involving-both p => transport T p unit

-- helper definitions, just so that example is self-contained

\class BaseSet (E : \Set)

\data Bool | true | false \where {
  \func or (a b : Bool) : Bool \elim a
    | true => true
    | false => b

  \func and (a b : Bool) : Bool \elim a
    | true => b
    | false => false

  \func neg (a : Bool) : Bool \elim a
    | true => false
    | false => true

  \func orAssoc (x y z : Bool) : Bool.or (Bool.or x y) z = Bool.or x (Bool.or y z) \elim x, y, z {
    | true, true, true => idp -- I know it looks terrible
    | true, true, false => idp -- but generating all branches and
    | true, false, true => idp -- replacing `{?}` by `idp`
    | true, false, false => idp -- was the fastest way :P
    | false, true, true => idp
    | false, true, false => idp
    | false, false, true => idp
    | false, false, false => idp
  }

  \func andAssoc (x y z : Bool) : and (and x y) z = and x (and y z) \elim x, y, z {
    | true, true, true => idp -- see above
    | true, true, false => idp
    | true, false, true => idp
    | true, false, false => idp
    | false, true, true => idp
    | false, true, false => idp
    | false, false, true => idp
    | false, false, false => idp
  }
}

\data Empty

\data Unit | unit

\func T (b : Bool) : \Type
  | true => Unit
  | false => Empty

\func transport {A : \Type} (B : A -> \Type) {a a' : A} (p : a = a') (b : B a) : B a' =>
  coe (\lam i => B (p @ i)) b right