Definition weqstn0toempty : ⟦0⟧ ≃ empty. Proof. apply weqtoempty. apply negstn0. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.