Skeleton: FinOrd

FinOrd is a skeleton of FinSet; FinOrd is equivalent to FinSet but has no isomorphisms. Less cryptically, isomorphic objects in FinSet are mapped to single objects in FinOrd representing their equivalence classes.

Skeletons are not quite functorial, because their construction requires the Axiom of Choice.

skeletons: FinSet

This data as json