Lemma isweq_flipsec {A B : UU} {C : A -> B -> UU} : isweq (@flipsec A B C). Proof. apply (isweq_iso _ flipsec); reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.