proposition: Corollary finite_equiv_equiv X Y : (X <~> Y) -> (Finite X <~> Finite Y).
proof: Proof. intros ?; apply equiv_iff_hprop; apply finite_equiv'; [ assumption | symmetry; assumption ]. Defined.
imports: Basics Types HSet Spaces.Nat.Core HFiber Factorization Truncations Colimits.Quotient Projective Fin