1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
Section unit_op.
Context {T : Type}.
Variable op : T -> T -> T.
Variable u : T.
Variable equ : T -> T -> Prop.
Class LeftUnit : Type :=
lunit : forall a, equ (op u a) a.
Class RightUnit : Type :=
runit : forall a, equ (op a u) a.
End unit_op.
Section comm_op.
Context {T U : Type}.
Variable op : T -> T -> U.
Variable equ : U -> U -> Prop.
Class Commutative : Type :=
commut : forall a b, equ (op a b) (op b a).
End comm_op.
Section assoc_op.
Context {T : Type}.
Variable op : T -> T -> T.
Variable equ : T -> T -> Prop.
Class Associative : Type :=
assoc : forall a b c, equ (op (op a b) c) (op a (op b c)).
End assoc_op.
|
