{A} {D : A -> Type} `{DHasEquivs A D} {a b : A} {f : a $-> b} `{!CatIsEquiv f} {g : a $-> b} {p : f $== g} {a' : D a} {b' : D b} (f' : DHom f a' b') `{fe' : !DCatIsEquiv f'} {g' : DHom g a' b'} (p' : DGpdHom p f' g') : DCatIsEquiv (fe:=catie_homotopic f p) g'. Proof. snrapply dcatie_adjointify. - exact (Build_DCatEquiv (fe':=fe') f')^-1$'. - refine (p'^$' $@R' _ $@' _). 1: exact isd0gpd_hom. refine ((dcate_buildequiv_fun f')^$' $@R' _ $@' _). 1: exact isd0gpd_hom. apply dcate_isretr. - refine (_ $@L' p'^$' $@' _). 1: exact isd0gpd_hom. refine (_ $@L' (dcate_buildequiv_fun f')^$' $@' _). 1: exact isd0gpd_hom. apply dcate_issect. 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.