In environment DHasEquivs : forall (A : Type) (IsGraph0 : IsGraph A) (Is2Graph0 : Is2Graph A) (Is01Cat0 : Is01Cat A) (H : Is1Cat A), HasEquivs A -> forall (D : A -> Type) (IsDGraph0 : IsDGraph D) (IsD2Graph0 : IsD2Graph D) (IsD01Cat0 : IsD01Cat D), IsD1Cat D -> Type A : Type IsGraph0 : IsGraph A Is2Graph0 : Is2Graph A Is01Cat0 : Is01Cat A H : Is1Cat A H0 : HasEquivs A D : A -> Type IsDGraph0 : IsDGraph D IsD2Graph0 : IsD2Graph D IsD01Cat0 : IsD01Cat D IsD1Cat0 : IsD1Cat D DCatEquiv : forall a b : A, a $<~> b -> D a -> D b -> Type DCatIsEquiv : forall (a b : A) (f : a $-> b), CatIsEquiv f -> forall (a' : D a) (b' : D b), DHom f a' b' -> Type dcate_fun : forall (a b : A) (f : a $<~> b) (a' : D a) (b' : D b), DCatEquiv a b f a' b' -> DHom f a' b' dcate_isequiv : forall (a b : A) (f : a $<~> b) (a' : D a) (b' : D b) (f' : DCatEquiv a b f a' b'), DCatIsEquiv a b f (cate_isequiv a b f) a' b' (dcate_fun a b f a' b' f') dcate_buildequiv : forall (a b : A) (f : a $-> b) (CatIsEquiv0 : CatIsEquiv f) (a' : D a) (b' : D b) (f' : DHom f a' b') (fe' : DCatIsEquiv a b f ?fe a' b' f'), DCatEquiv a b (Build_CatEquiv f) a' b' dcate_buildequiv_fun : forall (a b : A) (f : a $-> b) (CatIsEquiv0 : CatIsEquiv f) (a' : D a) (b' : D b) (f' : DHom f a' b') (fe' : DCatIsEquiv a b f ?fe1 a' b' f'), DGpdHom (cate_buildequiv_fun f) (dcate_fun a b (Build_CatEquiv f) a' b' (dcate_buildequiv a b f ?CatIsEquiv0 a' b' f' fe')) f' dcate_inv' : forall (a b : A) (f : a $<~> b) (a' : D a) (b' : D b), DCatEquiv a b f a' b' -> DHom (cate_inv' a b f) b' a' a : A b : A f : a $<~> b a' : D a b' : D b f' : DCatEquiv a b f a' b' The term "DId a'" has type "DHom (Id ?a) a' a'" while it is expected to have type "?D0 (Id a)". Command exited with non-zero status 1