`{Funext} (A B : Type) (p : A = B) : equiv_path B A (p^) = (equiv_path A B p)^-1%equiv. Proof. apply path_equiv. reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.