{A} {D : A -> Type} `{DHasEquivs A D} {a b : A} {f : a $-> b} `{!CatIsEquiv f} {a' : D a} {b' : D b} (f' : DHom f a' b') {fe' : DCatIsEquiv f'} : DCatEquiv (Build_CatEquiv f) a' b' := dcate_buildequiv f' (fe':=fe').
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.