Theorem weqstnprod { n : nat } ( P : ⟦n⟧ -> UU ) ( f : ⟦n⟧ -> nat ) ( ww : ∏ i : ⟦n⟧ , ( stn ( f i ) ) ≃ ( P i ) ) : ( ∏ x : ⟦n⟧ , P x ) ≃ stn ( stnprod f ). Proof. revert P f ww. induction n as [ | n IHn ]. - intros. simpl. apply ( weqcontrcontr ). + apply ( iscontrsecoverempty2 _ ( negstn0 ) ). + apply iscontrstn1. - intros. set ( w1 := weqdnicoprod n lastelement ). assert ( w2 := weqonsecbase P w1 ). assert ( w3 := weqsecovercoprodtoprod ( λ x : _, P ( w1 x ) ) ). assert ( w4 := weqcomp w2 w3 ) ; clear w2 w3. assert ( w5 := IHn ( λ x : ⟦n⟧, P ( w1 ( ii1 x ) ) ) ( λ x : ⟦n⟧, f ( w1 ( ii1 x ) ) ) ( λ i : ⟦n⟧, ww ( w1 ( ii1 i ) ) ) ). assert ( w6 := weqcomp w4 ( weqdirprodf w5 ( weqsecoverunit _ ) ) ) ; clear w4 w5. simpl in w6. assert ( w7 := weqcomp w6 ( weqdirprodf ( idweq _ ) ( invweq ( ww lastelement ) ) ) ). refine ( _ ∘ w7 )%weq. unfold w1. exact (weqfromprodofstn _ _ ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.