mathlib documentation

category_theory.category.Rel

The category of types with binary relations as morphisms.

def category_theory.Rel  :
Type (u+1)

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

Equations
@[instance]
Equations
@[instance]

The category of types with binary relations as morphisms.

Equations