# Documentation

Mathlib.CategoryTheory.Category.RelCat

The category of types with binary relations as morphisms.

A type synonym for Type, which carries the category instance for which morphisms are binary relations.

Equations

The category of types with binary relations as morphisms.

Equations