(n : nat) : IsEmbedding (er n) + { n : nat & { k : nat & e n = e (n + k).+1 }}. Proof. induction n as [|n [IH|IH]]. - left. intros x. apply hprop_inhabited_contr; intros [[] _]. - destruct (detachable_image_finite (er n) (er n.+1 (inr tt))) as [[k p]|ne]. + right. exists (nat_fin n k). exists (nat_fin_compl n k). rewrite nat_fin_compl_compl. exact p. + left. intros x. apply hprop_allpath. intros k l. apply path_sigma_hprop. destruct k as [[k|[]] p], l as [[l|[]] q]; simpl. * apply isinj_embedding in IH. apply ap. apply IH. unfold er in p, q. simpl in p, q. exact (p @ q^). * refine (Empty_rec (ne _)). exists k. exact (p @ q^). * refine (Empty_rec (ne _)). exists l. exact (q @ p^). * reflexivity. - right; exact IH. Defined.
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.