Definition weqstn1tounit : ⟦1⟧ ≃ unit. Proof. set ( f := λ x : ⟦1⟧, tt ). apply weqcontrcontr. - split with lastelement. intro t. destruct t as [ t l ]. set ( e := natlth1tois0 _ l ). apply ( invmaponpathsincl _ ( isinclstntonat 1 ) ( make_stn _ t l ) lastelement e ). - apply iscontrunit. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.