{A} `{HasEquivs A} {a b : A} (e : a $<~> b) : Epic e := cate_monic_equiv (A:=A^op) (a:=b) (b:=a) e.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.