α ≃ β is the type of functions from α → β with a two-sided inverse.

perm α is the type of bijections from α to itself.

If the outer subtype has more restrictive predicate than the inner one, then we can drop the latter.

If a proposition holds for all elements, then the subtype is equivalent to the original type.

A subtype of a sigma-type is a sigma-type over a subtype.

A sigma type over a subtype is equivalent to the sigma set over the original type, if the fiber is empty outside of the subset

swap a b is the permutation that swaps a and b and leaves other values as is.

Augment an equivalence with a prescribed mapping f a = b

Quotients are congruent on equivalences under equality of their relation. An alternative is just to use rewriting with eq, but then computational proofs get stuck.