a b c f (g : _ $-> c) : f $o braid a b $== g -> f $== g $o braid b a. Proof. intros p. apply (cate_epic_equiv (braide a b)). refine (_ $@ (cat_assoc _ _ _)^$). refine (_ $@ (_ $@L ((_ $@L cate_buildequiv_fun _) $@ _)^$)). 2: apply braid_braid. refine ((_ $@L _) $@ _ $@ (cat_idr _)^$). 1: apply cate_buildequiv_fun. exact p. Defined.
Require Import Basics.Overture Basics.Tactics Types.Forall. Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv. Require Import WildCat.NatTrans WildCat.Opposite.