different_type.lean

prelude
import init.logic
set_option old_structure_cmd true

universe u

class comm_semigroup (α : Type u) extends has_mul α

class monoid (α : Type u) extends has_mul α, has_one α :=
(one_mul : ∀ a : α, 1 * a = a) 

class comm_monoid (α : Type u) extends comm_semigroup α, has_one α :=
(one_mul : ∀ a : α, 1 * a = a)

class X (α : Type u) extends monoid α, comm_monoid α