proposition: Lemma path_unit_nat : Unit + nat = nat.
proof: 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). - now intros []. - now intros [[]|n]. Qed.
imports: HoTT(TruncType ExcludedMiddle abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card) HoTT(Equiv.BiInv) HoTT(HIT.unique_choice) HoTT.Sets(Ordinals Hartogs Powers GCH AC)