The category of types with binary relations as morphisms.

def CategoryTheory.RelCat : Type (u + 1)

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

Equations

• CategoryTheory.RelCat = Type u

instance CategoryTheory.RelCat.inhabited : Inhabited CategoryTheory.RelCat

Equations

• CategoryTheory.RelCat.inhabited = id inferInstance

instance CategoryTheory.rel : CategoryTheory.LargeCategory CategoryTheory.RelCat

The category of types with binary relations as morphisms.

Equations

• CategoryTheory.rel = CategoryTheory.Category.mk @CategoryTheory.rel.proof_1 @CategoryTheory.rel.proof_2 @CategoryTheory.rel.proof_3