Definition weqstn2tobool : ⟦2⟧ ≃ bool. Proof. set ( f := λ j : ⟦2⟧, match ( isdeceqnat j 0 ) with ii1 _ => false | ii2 _ => true end ). set ( g := λ b : bool, match b with false => make_stn 2 0 ( idpath true ) | true => make_stn 2 1 ( idpath true ) end ). split with f. assert ( egf : ∏ j : _ , paths ( g ( f j ) ) j ). { intro j. unfold f. destruct ( isdeceqnat j 0 ) as [ e | ne ]. - apply ( invmaponpathsincl _ ( isinclstntonat 2 ) ). rewrite e. apply idpath. - apply ( invmaponpathsincl _ ( isinclstntonat 2 ) ). destruct j as [ j l ]. simpl. set ( l' := natlthtolehsn _ _ l ). destruct ( natlehchoice _ _ l' ) as [ l'' | e ]. + simpl in ne. destruct ( ne ( natlth1tois0 _ l'' ) ). + apply ( pathsinv0 ( invmaponpathsS _ _ e ) ). } assert ( efg : ∏ b : _ , paths ( f ( g b ) ) b ). { intro b. unfold g. destruct b. - apply idpath. - apply idpath. } apply ( isweq_iso _ _ egf efg ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.