{A} `{HasEquivs A} {a b c : A} (g : b $<~> c) (f : a $<~> b) : g $o f $== cate_fun (g $oE f). Proof. apply gpd_rev. apply cate_buildequiv_fun. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.