equiv_N_segment_succ@{} (n : N) : { m : N & m <= succ n } <~> @sum@{p p} {m : N & m <= n} Unit. Proof. refine (_ oE equiv_N_segment (succ n)). apply equiv_functor_sum_r. apply equiv_functor_sigma_id. intros m; apply equiv_iff_hprop_uncurried, N_lt_succ_iff_le. Defined.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.