fact: Definition whiskerBL {f : x $<~> x02} (s : Square f01 f21 f10 f12) : Square (f^-1$ $o f01) f21 f10 (f12 $o f) := s $@ ((compose_hh_V _ _)^$ $@R f01) $@ cat_assoc _ _ _.
imports: Basics.Overture WildCat.Core WildCat.Equiv