In mathematics, the Rel has the class of sets as and binary relations as .
A morphism (or arrow) R : A → B in this category is a relation between the sets A and B, so R ⊆ A × B.
The composition of two relations R: A → B and S: B → C is given by
(a, c) ∈ S o R ⇔ for some b ∈ B, (a, b) ∈ R and (b, c) ∈ S.
Rel has also been called the "category of correspondences of sets".
The category Rel has the Set as a (wide) , where the arrow f : X → Y in Set corresponds to the relation F ⊆ X × Y defined by (x, y) ∈ F ⇔ f(x) = y.
A morphism in Rel is a relation, and the corresponding morphism in the to Rel has arrows reversed, so it is the converse relation. Thus Rel contains its opposite and is .
The involution represented by taking the converse relation provides the dagger to make Rel a .
The category has two functors into itself given by the hom functor: A binary relation R ⊆ A × B and its transpose RT ⊆ B × A may be composed either as R RT or as RT R. The first composition results in a homogeneous relation on A and the second is on B. Since the images of these hom functors are in Rel itself, in this case hom is an internal hom functor. With its internal hom functor, Rel is a , and furthermore a .
The category Rel can be obtained from the category Set as the for the whose functor corresponds to power set, interpreted as a covariant functor.
Perhaps a bit surprising at first sight is the fact that in Rel is given by the disjoint union (rather than the cartesian product as it is in Set), and so is the coproduct.
Rel is , if one defines both the monoidal product A ⊗ B and the internal hom A ⇒ B by the cartesian product of sets. It is also a if one defines the monoidal product by the disjoint union of sets.
The category Rel was the prototype for the algebraic structure called an by Peter J. Freyd and Andre Scedrov in 1990. Starting with a and a functor F: A → B, they note properties of the induced functor Rel(A,B) → Rel(FA, FB). For instance, it preserves composition, conversion, and intersection.