{A} `{HasEquivs A} {a b : A} (e : a $<~> b) : Monic e. Proof. intros c f g p. refine ((compose_V_hh e _)^$ $@ _ $@ compose_V_hh e _). exact (_ $@L p). Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.