`{P : A -> B -> Type} : (forall a b, P a b) -> (forall b a, P a b) := fun f b a => f a b. Arguments {A B P} f b a /. Global Instance isequiv_flip `{P : A -> B -> Type} : IsEquiv (@ _ _ P) | 0. Proof. set (flip_P := @ _ _ P). set (flip_P_inv := @ _ _ ( P)). set (flip_P_is_sect := (fun f => 1) : flip_P_inv o flip_P == idmap). set (flip_P_is_retr := (fun g => 1) : flip_P o flip_P_inv == idmap). exists flip_P_inv flip_P_is_retr flip_P_is_sect. intro g. exact 1. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids