{A} {D : A -> Type} `{DHasEquivs A D} {a b : A} {e f : a $<~> b} {p : cate_fun e $== cate_fun f} {a' : D a} {b' : D b} {e' : DCatEquiv e a' b'} {f' : DCatEquiv f a' b'} (p' : DGpdHom p (dcate_fun e') (dcate_fun f')) : DGpdHom (cate_inv2 p) (dcate_fun e'^-1$') (dcate_fun f'^-1$'). Proof. apply dcate_moveL_V1. rapply ((p'^$' $@R' _) $@' dcate_isretr _). exact isd0gpd_hom. 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.