a b c d f (g : d $-> _) : twist a b c $o f $== g -> f $== twist b a c $o g. Proof. intros p. apply (cate_monic_equiv (twiste a b c)). nrefine ((cate_buildequiv_fun _ $@R _) $@ p $@ _ $@ cat_assoc _ _ _). refine ((cat_idl _)^$ $@ (_^$ $@R _)). refine ((cate_buildequiv_fun _ $@R _) $@ _). apply twist_twist. 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.