1-- Group definitions2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Group.Defs8import Foundation910-- Operation graphs and carriers are sets. These predicates are the explicit11-- set-theoretic counterparts of algebraic interfaces.12predicate LeftCancellation (A op : Set) :=∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, op(a, b) = op(a, c) → b = c13predicate RightCancellation (A op : Set) :=∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, op(b, a) = op(c, a) → b = c14predicate CancelMagma (A op : Set) := IsMagma(A, op) ∧ (LeftCancellation(A, op) ∧ RightCancellation(A, op))15predicate CancelMonoid (A op unit : Set) := IsMonoid(A, op, unit) ∧ CancelMagma(A, op)16predicate IsInverse (A op unit a b : Set) := a ∈ A ∧ (b ∈ A ∧ (op(b, a) = unit ∧ op(a, b) = unit))17