Theorem weqtotal2asstor {X : UU} (P : X -> UU) (Q : total2 P -> UU) : total2 Q ≃ ∑ x : X, ∑ p : P x, Q (tpair P x p). Proof. intros. set (f := total2asstor P Q). set (g:= total2asstol P Q). split with f. assert (egf : ∏ xpq : _ , (g (f xpq)) = xpq). intro. apply idpath. assert (efg : ∏ xpq : _ , (f (g xpq)) = xpq). intro. apply idpath. apply (isweq_iso _ _ egf efg). Defined.