Unit + nat = nat. Proof. apply path_universe_uncurried. srapply equiv_adjointify. - exact (fun x => match x with inl _ => O | inr n => S n end). - exact (fun n => match n with O => inl tt | S n => inr n end). - by intros []. - by intros [[]|n]. Qed.
From HoTT Require Import TruncType ExcludedMiddle abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card. From HoTT Require Import Equiv.BiInv. From HoTT Require Import HIT.unique_choice. From HoTT.Sets Require Import Ordinals Hartogs Powers GCH AC.