Try to make entire library Cumulative #1710
Draft
Annotations
1 error and 1 warning
|
Run coq-community/docker-coq-action@v1:
theories/DProp.v#L122
In environment
H : Univalence
P : DHProp
Q : DHProp
eq_type_hprop := equiv_path_trunctype' P Q : P = Q <~> P = Q
The term "equiv_path_dhprop' P Q" has type
"Equiv@{HoTT.DProp.1550 HoTT.DProp.1550}
(@paths@{HoTT.DProp.1550} (TruncType@{HoTT.DProp.1508} (-1))
(dhprop_hprop@{HoTT.DProp.1508} P) (dhprop_hprop@{HoTT.DProp.1508} Q))
(@paths@{HoTT.DProp.1550} DHProp@{HoTT.DProp.1508} P Q)"
while it is expected to have type
"Equiv@{HoTT.DProp.1550 HoTT.DProp.1550}
(@paths@{HoTT.DProp.1512} (TruncType@{HoTT.DProp.1513} (-1))
(dhprop_hprop@{HoTT.DProp.1508} P) (dhprop_hprop@{HoTT.DProp.1508} Q))
(@paths@{HoTT.DProp.1518} DHProp@{HoTT.DProp.1508} P Q)".
Command exited with non-zero status 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/.
|
The logs for this run have expired and are no longer available.
Loading