Definition isfinite_isaset (X : UU) : isfinite X -> isaset X. Proof. intros isfin. use(factor_through_squash (isapropisaset X) _ isfin). intros f. use(isofhlevelweqf 2 _ (isasetstn (finstruct_cardinality f))). apply f. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.