a b : CatIsEquiv (braid a b) := catie_adjointify (braid a b) (braid b a) (braid_braid a b) (braid_braid b a).
Require Import Basics.Overture Basics.Tactics Types.Forall. Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv. Require Import WildCat.NatTrans WildCat.Opposite.