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

Showing changes from revision #0 to #1: Added | Removed | Changed

Idea

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

Definition

$Rel$ is a well-pointed locally Heyting-algebraic power unital tabular division semiadditive dagger 2-poset with an initial pointed unary system.

See also

• HilbR