mathlib3 documentation

category_theory.category.Rel

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
Instances for category_theory.Rel
@[protected, instance]
Equations
@[protected, instance]

The category of types with binary relations as morphisms.

Equations