Documentation

Mathlib.CategoryTheory.Category.RelCat

The category of types with binary relations as morphisms.

source
def CategoryTheory.RelCat :
Type (u + 1)

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

Instances For
    source
    instance CategoryTheory.RelCat.inhabited :
    Inhabited CategoryTheory.RelCat
    source
    instance CategoryTheory.rel :
    CategoryTheory.LargeCategory CategoryTheory.RelCat

    The category of types with binary relations as morphisms.