Theorem iscontriscontr {X : UU} (is : iscontr X) : iscontr (iscontr X). Proof. assert (is0 : ∏ (x x' : X), x = x') by (apply proofirrelevancecontr; assumption). assert (is1 : ∏ cntr : X, iscontr (∏ x, x = cntr)). { intro. assert (is2 : ∏ x, iscontr (x = cntr)). { assert (is2 : isaprop X) by (apply isapropifcontr; assumption). unfold isaprop in is2. unfold isofhlevel in is2. intro x. apply (is2 x cntr). } apply funcontr. assumption. } set (f := @pr1 X (λ cntr : X, ∏ x, x = cntr)). assert (X1 : isweq f) by (apply isweqpr1; assumption). change (∑ (cntr : X), ∏ x, x = cntr) with (iscontr X) in X1. apply (iscontrweqb (make_weq f X1)). assumption. Defined.