copumpkin/categories

Doesn't build with 2.4.2.3-rc

Closed this issue · 2 comments

/tmp/nix-build-categories-33409120d071656f5198c658145889ae2e86249c.drv-0/categories-3340912/Categories/Morphism/Indexed.agda:54,15-57
Xs IxOb.! .i != (B IxOb.! Xs) .i of type S
when checking that the expression
≣-cong (P.uncurry _⇒_ ⋆′ F) (cong₀ Xs i≈j) has type
my-Carrier .i ≣ my-Carrier .j
builder for ‘/nix/store/wgp5ilsf16y3c0ng70p0mcdbr575qfv4-categories-33409120d071656f5198c658145889ae2e86249c.drv’ failed with exit code 1
error: build of ‘/nix/store/wgp5ilsf16y3c0ng70p0mcdbr575qfv4-categories-33409120d071656f5198c658145889ae2e86249c.drv’ failed

The current master (da069c8) doesn't build with the current git checkout of Agda (8a8b831f33358) either. The error message is the same.

This is now fixed - the changes for 2.5.1.1 (merged pull request #15) took care of this too. I would close this issue, but I don't have the rights to do so.