Homotopy Type Theory Rel > history (Rev #4)

1. Idea

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

2. Definition

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

3. See also

• HilbR
• SEAR