Lean4
/-- The relation on `Prequotient` saying when two expressions are equal
because of the monoid laws, or
because one element is mapped to another by a morphism in the diagram.
-/
inductive Relation :
Prequotient F →
Prequotient F →
Prop -- Make it an equivalence relation:
| refl : ∀ x, Relation x x
| symm : ∀ (x y) (_ : Relation x y), Relation y x
| trans : ∀ (x y z) (_ : Relation x y) (_ : Relation y z), Relation x z
|
map :
∀ (j j' : J) (f : j ⟶ j') (x : F.obj j),
Relation (Prequotient.of j' ((F.map f) x))
(Prequotient.of j x) -- Then one relation per operation, describing the interaction with `of`
| mul : ∀ (j) (x y : F.obj j), Relation (Prequotient.of j (x * y)) (mul (Prequotient.of j x) (Prequotient.of j y))
| one : ∀ j, Relation (Prequotient.of j 1) one
| mul_1 : ∀ (x x' y) (_ : Relation x x'), Relation (mul x y) (mul x' y)
|
mul_2 :
∀ (x y y') (_ : Relation y y'),
Relation (mul x y)
(mul x y')
-- And one relation per axiom
| mul_assoc : ∀ x y z, Relation (mul (mul x y) z) (mul x (mul y z))
| one_mul : ∀ x, Relation (mul one x) x
| mul_one : ∀ x, Relation (mul x one) x
