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