Homotopy Type Theory Rel > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Idea

$Rel$ is the category of sets, with morphisms the relations between sets.

Definition

$Rel$ is a well-pointed W-topical extensional dagger 2-poset.

See also

• HilbR
• SEAR