{A} `{HasEquivs A} (a : A) : cate_fun (id_cate a) $== Id a. Proof. apply cate_buildequiv_fun. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.