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
- category_theory.Rel = Type u
@[instance]
Equations
- category_theory.Rel.inhabited = category_theory.Rel.inhabited._proof_1.mpr sort.inhabited
@[instance]
The category of types with binary relations as morphisms.
Equations
- category_theory.rel = {to_category_struct := {to_has_hom := {hom := λ (X Y : category_theory.Rel), X → Y → Prop}, id := λ (X : category_theory.Rel) (x y : X), x = y, comp := λ (X Y Z : category_theory.Rel) (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) (z : Z), ∃ (y : Y), f x y ∧ g y z}, id_comp' := category_theory.rel._proof_1, comp_id' := category_theory.rel._proof_2, assoc' := category_theory.rel._proof_3}