{X Y} {fX : Finite X} {fY : Finite Y} (f : X -> Y) (i : IsEmbedding f) : fcard X <= fcard Y. Proof. assert (MapIn (Tr (-1)) f) by exact _. clear i. destruct fX as [n e]; simpl. destruct fY as [m e']; simpl. strip_truncations. pose (g := e' o f o e^-1). assert (MapIn (Tr (-1)) g) by (unfold g; exact _). clearbody g. clear e e'. generalize dependent m. induction n as [|n IHn]. 1: exact _. intros m g ?. assert (i : IsInjective g) by (apply isinj_embedding; exact _). destruct m as [|m]. { elim (g (inr tt)). } 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))). { intros a. remember (g (inl a)) as b eqn:p. destruct b as [b|[]]. - assert (q : g (inl a) <> (g (inr tt))). { intros r. 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^). } rewrite r; exact tt. - assert (q : h (inl a) = g (inr tt)). { unfold h; apply moveR_equiv_V; symmetry. refine (_ @ p^); apply fin_transpose_last_with_with. } rewrite q. 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))). { intros []. assert (q : h (inr tt) = inr tt). { unfold h; apply moveR_equiv_V; symmetry. apply fin_transpose_last_with_last. } rewrite q; exact tt. } apply leq_succ. exact (IHn m (unfunctor_sum_l h Ha) (mapinO_unfunctor_sum_l (Tr (-1)) h Ha Hb)). Qed.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core Spaces.Nat.Factorial. Require Import HFiber. Require Import Factorization. Require Import Truncations. Require Import Colimits.Quotient. Require Import Projective. Require Import Fin.