{HE : HasEquivs A} (f10 : x00 $<~> x20) (f12 : x02 $<~> x22) (s : Square f01 f21 f10 f12) : Square f21 f01 f10^-1$ f12^-1$ := (cat_idl _)^$ $@ ((cate_issect f12)^$ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L ((cat_assoc _ _ _)^$ $@ (s^$ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L cate_isretr f10) $@ cat_idr _)).
Require Import Basics.Overture. Require Import WildCat.Core. Require Import WildCat.Equiv.