**groupoid**if and only if

(1) | $X$ is a D11: Set |

(2) | $f : X \times X \to Y$ is an D20: Enclosed binary operation on $X$ |

▾ Set of symbols

▾ Alphabet

▾ Deduction system

▾ Theory

▾ Zermelo-Fraenkel set theory

▾ Set

▾ Binary cartesian set product

▾ Binary relation

▾ Map

▾ Operation

▾ N-operation

▾ Binary operation

▾ Enclosed binary operation

▾ Alphabet

▾ Deduction system

▾ Theory

▾ Zermelo-Fraenkel set theory

▾ Set

▾ Binary cartesian set product

▾ Binary relation

▾ Map

▾ Operation

▾ N-operation

▾ Binary operation

▾ Enclosed binary operation

Formulation 0

An D548: Ordered pair $G = (X, f)$ is a **groupoid** if and only if

(1) | $X$ is a D11: Set |

(2) | $f : X \times X \to Y$ is an D20: Enclosed binary operation on $X$ |

Child definitions