Theorem saying that any general scheme to "transport" a structure along a weak equivalence which does not change the structure in the case of the identity equivalence is equivalent to the transport along the path which corresponds to a weak equivalence by the univalenceAxiom.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement