Does not build on 2.4.2
Fuuzetsu opened this issue · 1 comments
Fuuzetsu commented
Finished Categories.Discrete.
Checking Categories.End (/tmp/nix-build-categories.drv-0/git-export/Categories/End.agda).
Checking Categories.DinaturalTransformation (/tmp/nix-build-categories.drv-0/git-export/Categories/DinaturalTransformation.agda).
/tmp/nix-build-categories.drv-0/git-export/Categories/DinaturalTransformation.agda:39,24-25
No variable of type
ClimbBuilder (_Y_287 eta alpha f) (_Z_288 eta alpha f)
(_S_290 eta alpha f)
was found in scope.
when checking that (H.F₁ (f , C.id))
((η (c′ , c′) ∙ α c′) ∙ F.F₁ (C.id , f)) are valid arguments to a
function of type
({X Y Z : Obj} {s : Level} {S : Set s}
{{Sb : ClimbBuilder Y Z S}} →
S →
{t : Level} {T = T₁ : Set t} {{Tb : ClimbBuilder X Y T₁}} →
T₁ → Climb X Z)
builder for `/nix/store/80v6hmj6ng5gr4dl99zwgrsrz5g1996s-categories.drv' failed with exit code 1
error: build of `/nix/store/80v6hmj6ng5gr4dl99zwgrsrz5g1996s-categories.drv' failed