fact: Definition trans_comp {A B : Type} `{Is01Cat B} {F G K : A -> B} (gamma : G $=> K) (alpha : F $=> G) : F $=> K := fun a => gamma a $o alpha a.
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.Equiv WildCat.Square