{A} `{HasEquivs A} {a b : A} (e : a $<~> b) : cate_fun (e^-1$)^-1$ $== cate_fun e. Proof. apply cate_moveR_V1. symmetry; apply cate_issect. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.