fact: Definition fcard_equiv' {X Y} (e : X <~> Y) `{Finite X} `{Finite Y} : fcard X = fcard Y := fcard_equiv e.
imports: Basics Types HSet Spaces.Nat.Core HFiber Factorization Truncations Colimits.Quotient Projective Fin