{A} {D : A -> Type} `{DHasEquivs A D} {a b : A} {e : a $<~> b} {a' : D a} {b' : D b} (e' : DCatEquiv e a' b') : DMonic (mon:=cate_monic_equiv e) (dcate_fun e'). Proof. intros c f g p c' f' g' p'. refine ((dcompose_V_hh e' _)^$' $@' _ $@' dcompose_V_hh e' _). 1: exact isd0gpd_hom. exact (_ $@L' p'). Defined.
Require Import Basics.Overture. Require Import Basics.Tactics. Require Import Basics.Equivalences. Require Import Types.Sigma. Require Import WildCat.Core. Require Import WildCat.Displayed. Require Import WildCat.Equiv.