Definition weqdnicoprod (n : nat) (j : ⟦S n⟧ ) : ⟦n⟧ ⨿ unit ≃ ⟦S n⟧. Proof. intros. apply (make_weq (weqdnicoprod_map j)). apply (isweqhomot _ _ (weqdnicoprod_compute _)). apply weqproperty. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.