Theorem weqfromweqstntostn ( n : nat ) : ( (⟦n⟧) ≃ (⟦n⟧) ) ≃ ⟦factorial n⟧. Proof. induction n as [ | n IHn ]. - simpl. apply ( weqcontrcontr ). + apply ( iscontraprop1 ). * apply ( isapropweqtoempty2 _ ( negstn0 ) ). * apply idweq. + apply iscontrstn1. - change ( factorial ( S n ) ) with ( ( S n ) * ( factorial n ) ). set ( w1 := weqweqstnsn n ). apply ( weqcomp w1 ( weqcomp ( weqdirprodf ( idweq _ ) IHn ) ( weqfromprodofstn _ _ ) ) ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.