Theorem weqfromdecsubsetofstn { n : nat } ( f : ⟦n⟧ -> bool ) : total2 ( λ x : nat, hfiber f true ≃ (⟦x⟧) ). Proof. revert f. induction n as [ | n IHn ]. - intros. split with 0. assert ( g : hfiber f true -> (⟦0⟧) ). { intro hf. destruct hf as [ i e ]. destruct ( weqstn0toempty i ). } apply ( weqtoempty2 g weqstn0toempty ). - intro. set ( g := weqfromcoprodofstn 1 n ). change ( 1 + n ) with ( S n ) in g. set ( fl := λ i : ⟦1⟧, f ( g ( ii1 i ) ) ). set ( fh := λ i : ⟦n⟧, f ( g ( ii2 i ) ) ). assert ( w : ( hfiber f true ) ≃ ( hfiber ( sumofmaps fl fh ) true ) ). { set ( int := invweq ( weqhfibersgwtog g f true ) ). assert ( h : ∏ x : _ , paths ( f ( g x ) ) ( sumofmaps fl fh x ) ). { intro. destruct x as [ x1 | xn ]. + apply idpath. + apply idpath. } apply ( weqcomp int ( weqhfibershomot _ _ h true ) ). } set ( w' := weqcomp w ( invweq ( weqhfibersofsumofmaps fl fh true ) ) ). set ( x0 := pr1 ( IHn fh ) ). set ( w0 := pr2 ( IHn fh ) ). simpl in w0. destruct ( boolchoice ( fl lastelement ) ) as [ i | ni ]. + split with ( S x0 ). assert ( wi : hfiber fl true ≃ ⟦1⟧ ). { assert ( is : iscontr ( hfiber fl true ) ). { apply iscontraprop1. * apply ( isinclfromstn1 fl isasetbool true ). * apply ( make_hfiber _ lastelement i ). } apply ( weqcontrcontr is iscontrstn1 ). } apply ( weqcomp ( weqcomp w' ( weqcoprodf wi w0 ) ) ( weqfromcoprodofstn 1 _ ) ). + split with x0. assert ( g' : ¬ ( hfiber fl true ) ). { intro hf. destruct hf as [ j e ]. assert ( ee : j = lastelement ). { apply proofirrelevancecontr, iscontrstn1. } destruct ( nopathstruetofalse ( pathscomp0 ( pathscomp0 ( pathsinv0 e ) ( maponpaths fl ee ) ) ni ) ). } apply ( weqcomp w' ( weqcomp ( invweq ( weqii2withneg _ g' ) ) w0 ) ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.