Timings for Finite.v
(* -*- mode: coq; mode: visual-line -*- *)
Require Import Spaces.Nat.Core.
Require Import Factorization.
Require Import Truncations.
Require Import Colimits.Quotient.
Require Import Projective.
Local Open Scope path_scope.
Local Open Scope nat_scope.
(** ** Definition of general finite sets *)
Class Finite (X : Type) :=
{ fcard : nat ;
merely_equiv_fin : merely (X <~> Fin fcard) }.
Arguments merely_equiv_fin X {_}.
Definition issig_finite X
: { n : nat & merely (X <~> Fin n) } <~> Finite X.
(** Note that the sigma over cardinalities is not truncated. Nevertheless, because canonical finite sets of different cardinalities are not isomorphic, being finite is still an hprop. (Thus, we could have truncated the sigma and gotten an equivalent definition, but it would be less convenient to reason about.) *)
Global Instance ishprop_finite X
: IsHProp (Finite X).
refine (istrunc_equiv_istrunc _ (issig_finite X)).
apply ishprop_sigma_disjoint; intros n m Hn Hm.
refine (nat_eq_fin_equiv n m (Hm oE Hn^-1)).
(** ** Preservation of finiteness by equivalences *)
Definition finite_equiv X {Y} (e : X -> Y) `{IsEquiv X Y e}
: Finite X -> Finite Y.
refine (Build_Finite Y (fcard X) _).
assert (f := merely_equiv_fin X); strip_truncations.
exact (equiv_compose f e^-1).
Definition finite_equiv' X {Y} (e : X <~> Y)
: Finite X -> Finite Y
:= finite_equiv X e.
Corollary finite_equiv_equiv X Y
: (X <~> Y) -> (Finite X <~> Finite Y).
intros ?; apply equiv_iff_hprop; apply finite_equiv';
[ assumption | symmetry; assumption ].
Definition fcard_equiv {X Y} (e : X -> Y) `{IsEquiv X Y e}
`{Finite X} `{Finite Y}
: fcard X = fcard Y.
transitivity (@fcard Y (finite_equiv X e _)).
exact (ap (@fcard Y) (path_ishprop _ _)).
Definition fcard_equiv' {X Y} (e : X <~> Y)
`{Finite X} `{Finite Y}
: fcard X = fcard Y
:= fcard_equiv e.
(** ** Simple examples of finite sets *)
(** Canonical finite sets are finite *)
Global Instance finite_fin n : Finite (Fin n)
:= Build_Finite _ n (tr (equiv_idmap _)).
(** This includes the empty set. *)
Global Instance finite_empty : Finite Empty
:= finite_fin 0.
(** The unit type is finite, since it's equivalent to [Fin 1]. *)
Global Instance finite_unit : Finite Unit.
refine (finite_equiv' (Fin 1) _ _); simpl.
(** Thus, any contractible type is finite. *)
Global Instance finite_contr X `{Contr X} : Finite X
:= finite_equiv Unit equiv_contr_unit^-1 _.
(** Any decidable hprop is finite, since it must be equivalent to [Empty] or [Unit]. *)
Definition finite_decidable_hprop X `{IsHProp X} `{Decidable X}
: Finite X.
destruct (dec X) as [x|nx].
assert (Contr X) by exact (contr_inhabited_hprop X x).
refine (finite_equiv Empty nx^-1 _).
#[export]
Hint Immediate finite_decidable_hprop : typeclass_instances.
(** It follows that the propositional truncation of any finite set is finite. *)
Global Instance finite_merely X {fX : Finite X}
: Finite (merely X).
(** As in decidable_finite_hprop, we case on cardinality first to avoid needing funext. *)
destruct fX as [[|n] e]; refine (finite_decidable_hprop _).
intros x; strip_truncations; exact (e x).
strip_truncations; exact (tr (e^-1 (inr tt))).
(** Finite sets are closed under path-spaces. *)
Global Instance finite_paths {X} `{Finite X} (x y : X)
: Finite (x = y).
(** If we assume [Funext], then typeclass inference produces this automatically, since [X] has decidable equality and (hence) is a set, so [x=y] is a decidable hprop. But we can also deduce it without funext, since [Finite] is an hprop even without funext. *)
assert (e := merely_equiv_fin X).
refine (finite_equiv _ (ap e)^-1 _).
apply finite_decidable_hprop; exact _.
(** Finite sets are also closed under successors. *)
Global Instance finite_succ X `{Finite X} : Finite (X + Unit).
refine (Build_Finite _ (fcard X).+1 _).
pose proof (merely_equiv_fin X).
strip_truncations; apply tr.
refine (_ +E 1); assumption.
Definition fcard_succ X `{Finite X}
: fcard (X + Unit) = (fcard X).+1
:= 1.
(** ** Decidability *)
(** Like canonical finite sets, finite sets have decidable equality. *)
Global Instance decidablepaths_finite `{Funext} X `{Finite X}
: DecidablePaths X.
assert (e := merely_equiv_fin X).
refine (decidablepaths_equiv _ e^-1 _).
(** However, contrary to what you might expect, we cannot assert that "every finite set is decidable"! That would be claiming a *uniform* way to select an element from every nonempty finite set, which contradicts univalence. *)
(** One thing we can prove is that any finite hprop is decidable. *)
Global Instance decidable_finite_hprop X `{IsHProp X} {fX : Finite X}
: Decidable X.
(** To avoid having to use [Funext], we case on the cardinality of [X] before stripping the truncation from its equivalence to [Fin n]; if we did things in the other order then we'd have to know that [Decidable X] is an hprop, which requires funext. *)
strip_truncations; exact (e x).
strip_truncations; exact (e^-1 (inr tt)).
(** It follows that if [X] is finite, then its propositional truncation is decidable. *)
Global Instance decidable_merely_finite X {fX : Finite X}
: Decidable (merely X).
(** From this, it follows that any finite set is *merely* decidable. *)
Definition merely_decidable_finite X `{Finite X}
: merely (Decidable X).
apply O_decidable; exact _.
(** ** Induction over finite sets *)
(** Most concrete applications of this don't actually require univalence, but the general version does. For this reason the general statement is less useful (and less used in the sequel) than it might be. *)
Definition finite_ind_hprop `{Univalence}
(P : forall X, Finite X -> Type)
`{forall X (fX:Finite X), IsHProp (P X _)}
(f0 : P Empty _)
(fs : forall X (fX:Finite X), P X _ -> P (X + Unit)%type _)
(X : Type) `{Finite X}
: P X _.
assert (e := merely_equiv_fin X).
assert (p := transportD Finite P (path_universe e^-1) _).
refine (transport (P X) (path_ishprop _ _) (p _)).
generalize (fcard X); intros n.
refine (transport (P (Fin n.+1)) (path_ishprop _ _) (fs _ _ IH)).
(** ** The finite axiom of choice, and projectivity *)
Definition finite_choice {X} `{Finite X} : HasChoice X.
assert (e := merely_equiv_fin X).
assert (f' := (fun x => f (e^-1 x)) : forall x, merely (P' x)).
refine (Trunc_functor (X := forall x:Fin (fcard X), P' x) (-1) _ _).
intros g x; exact (eissect e x # g (e x)).
clearbody P'; clear f P e.
generalize dependent (fcard X); intros n P f.
exact (tr (Empty_ind P)).
specialize (IH (P o inl) (f o inl)).
assert (e := f (inr tt)).
exact (tr (sum_ind P IH (Unit_ind e))).
Corollary isprojective_fin_n (n : nat) : IsProjective (Fin n).
apply (iff_isoprojective_hasochoice _ (Fin n)).
(** ** Constructions on finite sets *)
(** Finite sets are closed under sums, products, function spaces, and equivalence spaces. There are multiple choices we could make regarding how to prove these facts. Since we know what the cardinalities ought to be in all cases (since we know how to add, multiply, exponentiate, and take factorials of natural numbers), we could specify those off the bat, and then reduce to the case of canonical finite sets. However, it's more amusing to instead prove finiteness of these constructions by "finite-set induction", and then *deduce* that their cardinalities are given by the corresponding operations on natural numbers (because they satisfy the same recurrences). *)
(** *** Binary sums *)
Global Instance finite_sum X Y `{Finite X} `{Finite Y}
: Finite (X + Y).
assert (e := merely_equiv_fin Y).
refine (finite_equiv _ (functor_sum idmap e^-1) _).
generalize (fcard Y); intros n.
refine (finite_equiv _ (sum_empty_r X)^-1 _).
refine (finite_equiv _ (equiv_sum_assoc X _ Unit) _).
(** Note that the cardinality function [fcard] actually computes. The same will be true of all the other proofs in this section, though we don't always verify it. *)
Goal fcard (Fin 3 + Fin 4) = 7.
Definition fcard_sum X Y `{Finite X} `{Finite Y}
: fcard (X + Y) = (fcard X + fcard Y).
refine (_ @ nat_add_comm _ _).
assert (e := merely_equiv_fin Y).
refine (fcard_equiv' (1 +E e) @ _).
refine (_ @ ap (fun y => (y + fcard X)) (fcard_equiv e^-1)).
generalize (fcard Y); intros n.
refine (fcard_equiv (sum_empty_r X)^-1).
refine (fcard_equiv (equiv_sum_assoc _ _ _)^-1 @ _).
(** *** Binary products *)
Global Instance finite_prod X Y `{Finite X} `{Finite Y}
: Finite (X * Y).
assert (e := merely_equiv_fin Y).
refine (finite_equiv _ (functor_prod idmap e^-1) _).
generalize (fcard Y); intros n.
refine (finite_equiv _ (prod_empty_r X)^-1 _).
refine (finite_equiv _ (sum_distrib_l X _ Unit)^-1 (finite_sum _ _)).
refine (finite_equiv _ (prod_unit_r X)^-1 _).
Definition fcard_prod X Y `{Finite X} `{Finite Y}
: fcard (X * Y) = fcard X * fcard Y.
assert (e := merely_equiv_fin X).
refine (fcard_equiv' (e *E 1) @ _).
refine (_ @ ap (fun x => x * fcard Y) (fcard_equiv e^-1)).
generalize (fcard X); intros n.
refine (fcard_equiv (prod_empty_l Y)).
refine (fcard_equiv (sum_distrib_r Y (Fin n) Unit) @ _).
refine (fcard_sum _ _ @ _).
refine (_ @ nat_add_comm _ _).
apply fcard_equiv', prod_unit_l.
(** *** Function types *)
(** Finite sets are closed under function types, and even dependent function types. *)
Global Instance finite_forall `{Funext} {X} (Y : X -> Type)
`{Finite X} `{forall x, Finite (Y x)}
: Finite (forall x:X, Y x).
assert (e := merely_equiv_fin X).
simple refine (finite_equiv' _
(equiv_functor_forall' (P := fun x => Y (e^-1 x)) e _) _); try exact _.
intros x; refine (equiv_transport _ (eissect e x)).
set (Y' := Y o e^-1); change (Finite (forall x, Y' x)).
assert (forall x, Finite (Y' x)) by exact _; clearbody Y'; clear e.
generalize dependent (fcard X); intros n Y' ?.
refine (finite_equiv _ (equiv_sum_ind Y') _).
refine (finite_equiv _ (@Unit_ind (fun u => Y' (inr u))) _).
refine (isequiv_unit_ind (Y' o inr)).
#[local] Hint Extern 4 => progress (cbv beta iota) : typeclass_instances.
Definition fcard_arrow `{Funext} X Y `{Finite X} `{Finite Y}
: fcard (X -> Y) = nat_exp (fcard Y) (fcard X).
assert (e := merely_equiv_fin X).
refine (fcard_equiv (functor_arrow e idmap)^-1 @ _).
refine (_ @ ap (fun x => nat_exp (fcard Y) x) (fcard_equiv e)).
generalize (fcard X); intros n.
refine (fcard_equiv (equiv_sum_ind (fun (_:Fin n.+1) => Y))^-1 @ _).
refine (fcard_prod _ _ @ _).
refine (fcard_equiv (@Unit_ind (fun (_:Unit) => Y))^-1).
(** [fcard] still computes, despite the funext: *)
Goal forall fs:Funext, fcard (Fin 3 -> Fin 4) = 64.
(** *** Automorphism types (i.e. symmetric groups) *)
Global Instance finite_aut `{Funext} X `{Finite X}
: Finite (X <~> X).
assert (e := merely_equiv_fin X).
refine (finite_equiv _
(equiv_functor_equiv e^-1 e^-1) _).
generalize (fcard X); intros n.
refine (finite_equiv _ (equiv_fin_equiv n n) _).
Definition fcard_aut `{Funext} X `{Finite X}
: fcard (X <~> X) = factorial (fcard X).
assert (e := merely_equiv_fin X).
refine (fcard_equiv
(equiv_functor_equiv e^-1 e^-1)^-1 @ _).
generalize (fcard X); intros n.
refine (fcard_equiv (equiv_fin_equiv n n)^-1 @ _).
refine (fcard_prod _ _ @ _).
(** [fcard] still computes: *)
Goal forall fs:Funext, fcard (Fin 4 <~> Fin 4) = 24.
(** ** Finite sums of natural numbers *)
(** Perhaps slightly less obviously, finite sets are also closed under sigmas. *)
Global Instance finite_sigma {X} (Y : X -> Type)
`{Finite X} `{forall x, Finite (Y x)}
: Finite { x:X & Y x }.
assert (e := merely_equiv_fin X).
refine (finite_equiv' _
(equiv_functor_sigma (equiv_inverse e)
(fun x (y:Y (e^-1 x)) => y)) _).
(** Unfortunately, because [compose] is currently beta-expanded, [set (Y' := Y o e^-1)] doesn't change the goal. *)
set (Y' := fun x => Y (e^-1 x)).
assert (forall x, Finite (Y' x)) by exact _; clearbody Y'; clear e.
generalize dependent (fcard X); intros n Y' ?.
refine (finite_equiv Empty pr1^-1 _).
refine (finite_equiv _ (equiv_sigma_sum (Fin n) Unit Y')^-1 _).
refine (finite_equiv _ (equiv_contr_sigma _)^-1 _).
(** Amusingly, this automatically gives us a way to add up a family of natural numbers indexed by any finite set. (We could of course also define such an operation directly, probably using [merely_ind_hset].) *)
Definition finadd {X} `{Finite X} (f : X -> nat) : nat
:= fcard { x:X & Fin (f x) }.
Definition fcard_sigma {X} (Y : X -> Type)
`{Finite X} `{forall x, Finite (Y x)}
: fcard { x:X & Y x } = finadd (fun x => fcard (Y x)).
set (f := fun x => fcard (Y x)).
set (g := fun x => merely_equiv_fin (Y x) : merely (Y x <~> Fin (f x))).
apply finite_choice in g; [| exact _].
refine (fcard_equiv' (equiv_functor_sigma_id g)).
(** The sum of a finite constant family is the product by its cardinality. *)
Definition finadd_const X `{Finite X} n
: finadd (fun x:X => n) = fcard X * n.
transitivity (fcard (X * Fin n)).
exact (fcard_equiv' (equiv_sigma_prod0 X (Fin n))).
exact (fcard_prod X (Fin n)).
(** Closure under sigmas and paths also implies closure under hfibers. *)
Definition finite_hfiber {X Y} (f : X -> Y) (y : Y)
`{Finite X} `{Finite Y}
: Finite (hfiber f y).
(** Therefore, the cardinality of the domain of a map between finite sets is the sum of the cardinalities of its hfibers. *)
Definition fcard_domain {X Y} (f : X -> Y) `{Finite X} `{Finite Y}
: fcard X = finadd (fun y => fcard (hfiber f y)).
refine (_ @ fcard_sigma (hfiber f)).
refine (fcard_equiv' (equiv_fibration_replacement f)).
(** In particular, the image of a map between finite sets is finite. *)
Definition finite_image
{X Y} `{Finite X} `{Finite Y} (f : X -> Y)
: Finite (himage f).
(** ** Finite products of natural numbers *)
(** Similarly, closure of finite sets under [forall] automatically gives us a way to multiply a family of natural numbers indexed by any finite set. Of course, if we defined this explicitly, it wouldn't need funext. *)
Definition finmult `{Funext} {X} `{Finite X} (f : X -> nat) : nat
:= fcard (forall x:X, Fin (f x)).
Definition fcard_forall `{Funext} {X} (Y : X -> Type)
`{Finite X} `{forall x, Finite (Y x)}
: fcard (forall x:X, Y x) = finmult (fun x => fcard (Y x)).
set (f := fun x => fcard (Y x)).
set (g := fun x => merely_equiv_fin (Y x) : merely (Y x <~> Fin (f x))).
apply finite_choice in g; [| exact _].
refine (fcard_equiv' (equiv_functor_forall' (equiv_idmap X) g)).
(** The product of a finite constant family is the exponential by its cardinality. *)
Definition finmult_const `{Funext} X `{Finite X} n
: finmult (fun x:X => n) = nat_exp n (fcard X).
refine (fcard_arrow X (Fin n)).
(** ** Finite subsets *)
(** Closure under sigmas implies that a detachable subset of a finite set is finite. *)
Global Instance finite_detachable_subset {X} `{Finite X} (P : X -> Type)
`{forall x, IsHProp (P x)} `{forall x, Decidable (P x)}
: Finite { x:X & P x }.
(** Conversely, if a subset of a finite set is finite, then it is detachable. We show first that an embedding between finite subsets has detachable image. *)
Definition detachable_image_finite
{X Y} `{Finite X} `{Finite Y} (f : X -> Y) `{IsEmbedding f}
: forall y, Decidable (hfiber f y).
assert (ff : Finite (hfiber f y)) by exact _.
right; intros u; strip_truncations; exact (e u).
left; strip_truncations; exact (e^-1 (inr tt)).
Definition detachable_finite_subset {X} `{Finite X}
(P : X -> Type) `{forall x, IsHProp (P x)}
{Pf : Finite ({ x:X & P x })}
: forall x, Decidable (P x).
refine (decidable_equiv _ (hfiber_fibration x P)^-1 _).
(* The try clause below is only needed for Coq <= 8.11 *)
refine (detachable_image_finite pr1 x); try assumption.
apply (mapinO_pr1 (Tr (-1))).
(** Why doesn't Coq find this? *)
(** ** Quotients *)
(** The quotient of a finite set by a detachable equivalence relation is finite. *)
Section DecidableQuotients.
Context `{Univalence} {X} `{Finite X}
(R : Relation X) `{is_mere_relation X R}
`{Reflexive _ R} `{Transitive _ R} `{Symmetric _ R}
{Rd : forall x y, Decidable (R x y)}.
Global Instance finite_quotient : Finite (Quotient R).
assert (e := merely_equiv_fin X).
pose (R' x y := R (e^-1 x) (e^-1 y)).
assert (is_mere_relation _ R') by exact _.
assert (Reflexive R') by (intros ?; unfold R'; apply reflexivity).
assert (Symmetric R') by (intros ? ?; unfold R'; apply symmetry).
assert (Transitive R') by (intros ? ? ?; unfold R'; apply transitivity).
assert (R'd : forall x y, Decidable (R' x y))
by (intros ? ?; unfold R'; apply Rd).
srefine (finite_equiv' _ (equiv_quotient_functor R' R e^-1 _) _).
1: by try (intros; split).
generalize dependent (fcard X);
intros n; induction n as [|n IH]; intros R' ? ? ? ? ?.
refine (finite_equiv Empty _^-1 _).
refine (Quotient_rec R' _ Empty_rec (fun x _ _ => match x with end)).
pose (R'' x y := R' (inl x) (inl y)).
assert (is_mere_relation _ R'') by exact _.
assert (Reflexive R'') by (intros ?; unfold R''; apply reflexivity).
assert (Symmetric R'') by (intros ? ?; unfold R''; apply symmetry).
assert (Transitive R'') by (intros ? ? ?; unfold R''; apply transitivity).
assert (forall x y, Decidable (R'' x y)) by (intros ? ?; unfold R''; apply R'd).
assert (inlresp := (fun x y => idmap)
: forall x y, R'' x y -> R' (inl x) (inl y)).
destruct (dec (merely {x:Fin n & R' (inl x) (inr tt)})) as [p|np].
refine (finite_equiv' (Quotient R'') _ _).
refine (Build_Equiv _ _ (Quotient_functor R'' R' inl inlresp) _).
refine (Quotient_ind_hprop R' _ _).
exists (class_of R'' y); reflexivity.
exists (class_of R'' x); simpl.
apply isembedding_isinj_hset; intros u.
refine (Quotient_ind_hprop R'' _ _); intros v.
revert u; refine (Quotient_ind_hprop R'' _ _); intros u.
exact (related_quotient_paths R' (inl u) (inl v) q).
refine (finite_equiv' (Quotient R'' + Unit) _ _).
refine (Build_Equiv _ _ (sum_ind (fun _ => Quotient R')
(Quotient_functor R'' R' inl inlresp)
(fun _ => class_of R' (inr tt))) _).
refine (Quotient_ind_hprop R' _ _).
exists (inl (class_of R'' y)); reflexivity.
exists (inr tt); reflexivity.
apply isembedding_isinj_hset; intros u.
refine (Quotient_ind_hprop R'' _ _); intros v.
revert u; refine (sum_ind _ _ _).
refine (Quotient_ind_hprop R'' _ _); intros u.
apply ap, qglue; unfold R''.
exact (related_quotient_paths R' (inl u) (inl v) q).
apply related_quotient_paths in q; try exact _.
destruct u as [u|[]]; simpl.
revert u; refine (Quotient_ind_hprop R'' _ _); intros u; simpl.
apply related_quotient_paths in q; try exact _.
(** Therefore, the cardinality of [X] is the sum of the cardinalities of its equivalence classes. *)
Definition fcard_quotient
: fcard X = finadd (fun z:Quotient R => fcard {x:X & in_class R z x}).
refine (fcard_domain (class_of R) @ _).
apply ap, path_arrow; intros z; revert z.
refine (Quotient_ind_hprop _ _ _); intros x; simpl.
apply fcard_equiv'; unfold hfiber.
refine (equiv_functor_sigma_id _); intros y; simpl.
refine (path_quotient R y x oE _).
apply equiv_iff_hprop; apply symmetry.
(** ** Injections *)
(** An injection between finite sets induces an inequality between their cardinalities. *)
Definition leq_inj_finite {X Y} {fX : Finite X} {fY : Finite Y}
(f : X -> Y) (i : IsEmbedding f)
: fcard X <= fcard Y.
assert (MapIn (Tr (-1)) f) by exact _.
destruct fX as [n e]; simpl.
destruct fY as [m e']; simpl.
pose (g := e' o f o e^-1).
assert (MapIn (Tr (-1)) g) by (unfold g; exact _).
assert (i : isinj g) by (apply isinj_embedding; exact _).
pose (h := (fin_transpose_last_with m (g (inr tt)))^-1 o g).
assert (MapIn (Tr (-1)) h) by (unfold h; exact _).
assert (Ha : forall a:Fin n, is_inl (h (inl a))).
remember (g (inl a)) as b eqn:p.
assert (q : g (inl a) <> (g (inr tt))).
exact (inl_ne_inr _ _ (i _ _ r)).
rewrite p in q; apply symmetric_neq in q.
assert (r : h (inl a) = inl b).
unfold h; apply moveR_equiv_V; symmetry.
refine (fin_transpose_last_with_rest m (g (inr tt)) b q @ p^).
assert (q : h (inl a) = g (inr tt)).
unfold h; apply moveR_equiv_V; symmetry.
refine (_ @ p^); apply fin_transpose_last_with_with.
destruct (is_inl_or_is_inr (g (inr tt))) as [l|r]; try assumption.
assert (s := inr_un_inr _ r).
revert s; generalize (un_inr (g (inr tt)) r); intros [] s.
elim (inl_ne_inr _ _ (i _ _ (p @ s))).
assert (Hb : forall b:Unit, is_inr (h (inr b))).
assert (q : h (inr tt) = inr tt).
unfold h; apply moveR_equiv_V; symmetry.
apply fin_transpose_last_with_last.
exact (IHn m (unfunctor_sum_l h Ha)
(mapinO_unfunctor_sum_l (Tr (-1)) h Ha Hb)).
(** ** Surjections *)
(** A surjection between finite sets induces an inequality between their cardinalities. *)
Definition geq_surj_finite {X Y} {fX : Finite X} {fY : Finite Y}
(f : X -> Y) (i : IsSurjection f)
: fcard X >= fcard Y.
destruct fX as [n e], fY as [m e']; simpl.
assert (k := isprojective_fin_n m).
pose (g := e' o f o e^-1).
assert (k' : IsSurjection g) by exact _ .
assert (j := k (Fin n) _ (Fin m) _ idmap g k').
simpl; destruct j as [s is_section].
change n with (fcard (Fin n)).
change m with (fcard (Fin m)).
apply (leq_inj_finite s).
apply isembedding_isinj_hset, (isinj_section is_section).
(** ** Enumerations *)
(** A function from [nat] to a finite set must repeat itself eventually. *)
Context `{Funext} {X} `{Finite@{_ Set _} X} (e : nat -> X).
Let er (n : nat) : Fin n -> X
:= fun k => e (nat_fin n k).
Lemma finite_enumeration_stage (n : nat)
: IsEmbedding (er n)
+ { n : nat & { k : nat & e n = e (n + k).+1 }}.
induction n as [|n [IH|IH]].
apply hprop_inhabited_contr; intros [[] _].
destruct (detachable_image_finite (er n) (er n.+1 (inr tt)))
as [[k p]|ne].
exists (nat_fin_compl n k).
rewrite nat_fin_compl_compl.
destruct k as [[k|[]] p], l as [[l|[]] q]; simpl.
apply isinj_embedding in IH.
refine (Empty_rec (ne _)).
refine (Empty_rec (ne _)).
Definition finite_enumeration_repeats
: { n : nat & { k : nat & e n = e (n + k).+1 }}.
destruct (finite_enumeration_stage (fcard X).+1) as [p|?].
assert (q := leq_inj_finite (er (fcard X).+1) p); simpl in q.