{A} {D : A -> Type} `{DHasEquivs A D} {a : A} (a' : D a) : DCatEquiv (id_cate a) a' a' := Build_DCatEquiv (DId a').
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.