a b c d f (g : d $-> _) : fmap01 F a (braid b c) $o f $== g -> f $== fmap01 F a (braid c b) $o g. Proof. intros p. apply (cate_monic_equiv (emap01 F a (braide b c))). refine (_ $@ cat_assoc _ _ _). refine (_ $@ (_ $@R _)). 2: { refine (_ $@ (_^$ $@R _)). 2: apply cate_buildequiv_fun. refine ((fmap_id _ _)^$ $@ fmap2 _ _ $@ fmap_comp _ _ _). refine ((_ $@R _) $@ _)^$. 1: apply cate_buildequiv_fun. apply braid_braid. } refine ((_ $@R _) $@ p $@ (cat_idl _)^$). refine (_ $@ fmap2 _ _); apply cate_buildequiv_fun. 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.