fact: Definition fmap_square {B : Type} `{Is1Cat B} (f : A -> B) `{!Is0Functor f} `{!Is1Functor f} (s : Square f01 f21 f10 f12) : Square (fmap f f01) (fmap f f21) (fmap f f10) (fmap f f12) := (fmap_comp f _ _)^$ $@ fmap2 f s $@ fmap_comp f _ _.
imports: Basics.Overture WildCat.Core WildCat.Equiv