---

Step * 1 1 of Lemma mk_imon

.....set predicate..... 
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. le : T ⟶ T ⟶ 𝔹
4. op : T ⟶ T ⟶ T
5. id : T
6. inv : T ⟶ T
7. Assoc(T;op)
8. Ident(T;op;id)
⊢ IsMonoid(|<T, eq, le, op, id, inv>|;*;e)
BY
{ AbReduce 0 }

1
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. le : T ⟶ T ⟶ 𝔹
4. op : T ⟶ T ⟶ T
5. id : T
6. inv : T ⟶ T
7. Assoc(T;op)
8. Ident(T;op;id)
⊢ IsMonoid(T;op;id)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  T  :  Type
2.  eq  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
3.  le  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
4.  op  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
5.  id  :  T
6.  inv  :  T  {}\mrightarrow{}  T
7.  Assoc(T;op)
8.  Ident(T;op;id)
\mvdash{}  IsMonoid(|<T,  eq,  le,  op,  id,  inv>|;*;e)


By

---

Latex:
AbReduce  0

---

Home Index