Definition fincard {X : UU} (xf : isfinite X) : nat. Proof. apply (squash_pairs_to_set (λ n : nat, ⟦ n ⟧ ≃ X) isasetnat). { intros n n' w w'. apply weqtoeqstn. exact (invweq w' ∘ w)%weq. } assumption. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.