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