copumpkin/categories

Does not build on 2.4.2

Fuuzetsu opened this issue · 1 comments

 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

@Saizan , you fixed this on a branch and @xplat said he was OK with 2.4.2, could you merge into master?