(s : Square f01 f21 f10 f12) (t : Square f03 f23 f12 f14) : Square (f03 $o f01) (f23 $o f21) f10 f14 := cat_assoc _ _ _ $@ (f23 $@L s) $@ (cat_assoc _ _ _)^$ $@ (t $@R f01) $@ cat_assoc _ _ _.
Require Import Basics.Overture. Require Import WildCat.Core. Require Import WildCat.Equiv.