Definition flipsec_weq {A B : UU} {C : A -> B -> UU} : (∏ a b, C a b) ≃ (∏ b a, C a b) := make_weq flipsec isweq_flipsec.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.