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

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

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

Process completed with exit code 1.

Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.

Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.

Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.

Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.

Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.

Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.

Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: geekyeggo/delete-artifact@v1. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.

The following actions uses node12 which is deprecated and will be forced to run on node16: geekyeggo/delete-artifact@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/

Unable to delete artifact "alectryon-html"; the artifact was not found.

Unable to delete artifact "workspace-8.18"; the artifact was not found.

Unable to delete artifact "file-dep-graphs"; the artifact was not found.

Unable to delete artifact "timing-html"; the artifact was not found.

Unable to delete artifact "workspace-dev"; the artifact was not found.

Unable to delete artifact "coqdoc-html"; the artifact was not found.

Unable to delete artifact "dep-graphs"; the artifact was not found.

Unable to delete artifact "workspace-latest"; the artifact was not found.

Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.

Unexpected input(s) 'name', 'authToken', 'extraPullNames', valid inputs are ['extra_nix_config', 'github_access_token', 'install_url', 'install_options', 'nix_path']

Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.

Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.

Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.