Square@{u v w} {A : Type@{u}} `{Is1Cat@{u w v} A} {x00 x20 x02 x22 : A} (f01 : x00 $-> x02) (f21 : x20 $-> x22) (f10 : x00 $-> x20) (f12 : x02 $-> x22) : Type@{w} := f21 $o f10 $== f12 $o f01.
Require Import Basics.Overture. Require Import WildCat.Core. Require Import WildCat.Equiv.