Lemma isinclfromstn1 { X : UU } ( f : ⟦1⟧ -> X ) ( is : isaset X ) : isincl f. Proof. intros. apply ( isinclbetweensets f ( isasetstn 1 ) is ). intros x x' e. apply ( invmaponpathsweq weqstn1tounit x x' ( idpath tt ) ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.