📄️ Add
The "Add" typeclass just represents anything that has a + operator.
📄️ AddCommGroup
AddCommGroup represents an Abelian group. It's a commutative, additive group.
📄️ AddCommGroupHom
An additive commutative group homomorphism.
📄️ AddCommMonoid
AddCommMonoid represents a commutative, additive monoid.
📄️ AddCommMonoidHom
An additive commutative monoid homomorphism.
📄️ AddCommSemigroup
Extending the additive semigroup with commutativity.
📄️ AddGroup
An additive group is an additive monoid that also has inverses.
📄️ AddGroupHom
An additive group homomorphism that preserves the additive group structure.
📄️ AddLeftOrderedGroup
A left-ordered group is a group with a left-invariant order.
📄️ AddMonoid
An additive monoid is an additive semigroup with an identity element.
📄️ AddMonoidHom
An additive monoid homomorphism that preserves the operation and the identity.
📄️ AddOrderedGroup
An ordered group has both left and right invariance.
📄️ AddSemigroup
An additive semigroup is associative, and that's about it.
📄️ AddSubgroup
An additive subgroup of an additive group G, represented as a subset closed under the additive group operations.
📄️ AddSubmonoid
An additive submonoid of an additive monoid, represented as a subset containing zero and closed under addition.
📄️ Bijection
A bijection between two types.
📄️ Category
A category with object type O and morphism type M.
📄️ CategoryEquivalence
An equivalence of categories: a pair of functors with unit/counit natural isomorphisms.
📄️ Color
A simple enumeration type used as an example of a metric space with the discrete metric.
📄️ CommGroup
CommGroup represents an Abelian group. It's a commutative, multiplicative group.
📄️ CommMonoid
CommMonoid represents a commutative, multiplicative monoid.
📄️ CommRing
A commutative ring is a ring where multiplication is also commutative.
📄️ CommSemigroup
Extending the multiplicative semigroup with commutativity.
📄️ Complex
Complex numbers consist of a real part and an imaginary part.
📄️ DistribLattice
A lattice where meets distribute over joins and joins distribute over meets.
📄️ Field
A field is a commutative ring with multiplicative inverses for all non-zero elements.
📄️ Fin
Finite initial segment { 0, 1, ..., n - 1 }.
📄️ FiniteGroup
A group is finite if its elements can be placed in a (finite) list
📄️ FiniteSet
A finite set is a Set bundled with a finiteness proof.
📄️ FiniteSubgroup
A finite subgroup of a finite group.
📄️ Functor
A functor between two categories.
📄️ Group
A group is a monoid that also has inverses.
📄️ GroupHom
A group homomorphism that preserves the group structure.
📄️ Ideal
An ideal of a commutative ring, represented as a subset closed under addition and absorbing multiplication.
📄️ Inhabited
A type with a distinguished default element.
📄️ Int
The Int type represents integers.
📄️ Inverse
The "Inverse" typeclass represents anything that has a multiplicative inverse operator.
📄️ Iso
An isomorphism in a category, with explicit inverse data.
📄️ Join
A type with a binary join operation.
📄️ JoinSemilattice
A partially ordered type with binary least upper bounds.
📄️ LTE
The "LTE" typeclass represents anything that has a less-than-or-equal-to relation.
📄️ Lattice
A partially ordered type with binary meets and joins.
📄️ LeftOrderedGroup
A left-ordered group is a group with a left-invariant order.
📄️ LinearOrder
A linear order (total order) is a partial order where all elements are comparable.
📄️ List
A generic list data structure that can hold elements of any type.
📄️ Meet
A type with a binary meet operation.
📄️ MeetSemilattice
A partially ordered type with binary greatest lower bounds.
📄️ MetricSpace
A metric space is a set equipped with a distance function that satisfies specific axioms.
📄️ Module
A left R-module: an additive abelian group together with an action of R that is
📄️ Monoid
A multiplicative monoid is a multiplicative semigroup with an identity element.
📄️ MonoidHom
A monoid homomorphism that preserves the operation and the identity.
📄️ Mul
The "Mul" typeclass represents anything that has a binary multiplication operator.
📄️ MulAction
A left action of a group on a type.
📄️ Multiset
A multiset (bag) that can contain multiple copies of the same element.
📄️ Nat
Natural numbers, the soul of arithmetic.
📄️ NaturalTransformation
A natural transformation between two functors with matching source and target categories.
📄️ Neg
The "Neg" typeclass represents anything that has a unary negation operator.
📄️ One
The "One" typeclass represents anything that has a multiplicative identity element.
📄️ Option
Optional values that can either contain a value of type T or be empty.
📄️ OrderDualIso
An order-dual isomorphism with explicit inverse data.
📄️ OrderIso
An order isomorphism with explicit inverse data.
📄️ OrderedField
A field with a total order compatible with the field operations.
📄️ OrderedGroup
An ordered group has both left and right invariance of the order under multiplication.
📄️ Pair
An ordered pair of two values, possibly of different types.
📄️ PartialOrder
A partial order is a relation that is reflexive, transitive, and antisymmetric.
📄️ Quotient
The quotient of a type by a relation, represented by equivalence classes.
📄️ QuotientOver
A quotient element whose relation is carried as part of the element.
📄️ QuotientRelation
A relation together with the fact that it is an equivalence relation.
📄️ Rat
Rational numbers represented as fractions in reduced form.
📄️ Real
Real numbers are defined by a Dedekind cut. Specifically, using the gt_rat function which
📄️ Ring
A ring is a structure with two operations (addition and multiplication) where addition forms an abelian group,
📄️ RingHom
A ring homomorphism that preserves both addition and multiplication and the multiplicative identity.
📄️ Semigroup
The default semigroup uses the multiplication operator..
📄️ Semiring
A semiring is like a ring but without additive inverses.
📄️ SemiringHom
A semiring homomorphism preserving addition, multiplication, zero, and one.
📄️ Set
Sets with elements of type K are defined as Boolean functions over K
📄️ Subgroup
A subgroup of a group G, represented as a subset that is closed under the group operations.
📄️ Submodule
A submodule of a module, represented as a subset closed under the module operations.
📄️ Submonoid
A submonoid of a monoid M, represented as a subset closed under multiplication that contains the identity.
📄️ Subring
A subring of a ring, represented as a subset containing zero and one and closed under ring operations.
📄️ Subsemigroup
A subsemigroup of a semigroup S, represented as a subset closed under multiplication.
📄️ Sum
A value belonging to one of two types.
📄️ TwoType
A type with exactly two values.
📄️ Unit
A unit of a monoid is an element with a two-sided multiplicative inverse.
📄️ UnitType
A type with exactly one inhabitant.
📄️ Zero
The "Zero" typeclass represents anything that has an additive identity element.
📄️ Zmod
Integer residue classes modulo n.