Corollary isconnectedstn1 : ∏ i1 i2 : ⟦1⟧, i1 = i2. Proof. intros i1 i2. apply (invmaponpathsweq weqstn1tounit). apply isProofIrrelevantUnit. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.