equiv_N_segment@{} (n : N) : { m : N & m <= n } <~> (sum@{p p} {m : N & m < n} Unit). Proof. srefine (equiv_adjointify _ _ _ _). - intros mH. destruct (N_le_eq_or_lt mH.1 n mH.2) as [H0|Hs]. + exact (inr tt). + exact (inl (mH.1;Hs)). - intros [mH|?]. + exact (mH.1; N_lt_le mH.1 n mH.2). + exists n; reflexivity. - abstract (intros [[m H]|[]]; cbn; [ generalize (N_le_eq_or_lt m n (N_lt_le m n H)); intros [H0|Hs]; cbn; [ apply Empty_rec; rewrite H0 in H; exact (N_lt_irref n H) | apply ap, ap, path_ishprop ] | generalize (N_le_eq_or_lt n n (reflexive_N_le n)); intros [H0|Hs]; [ reflexivity | apply Empty_rec; exact (N_lt_irref n Hs) ]]). - abstract (intros [m H]; cbn; generalize (N_le_eq_or_lt m n H); intros [H0|Hs]; cbn; [ apply path_sigma_hprop; symmetry; assumption | apply ap, path_ishprop ]). Defined.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.