Convert to Idris 2

[marcosh]

We will have to consider this at some point, so I thought it would be good to put this out here.

coming from statebox/idris-stbx-core#34

[clayrat]

Blodwen is now deprecated so I removed it from the title

[clayrat]

Issues encountered:

• Basic.Functor.functorEq doesn’t typecheck (solved by explicitly using heterogenous equality)
• Idris.TypesAsCategory.typesAsCategory insists on compose being (partially) eta-expanded, i.e. only \a => compose a and more verbose variants typecheck
• Product.ProductFunctor.productFunctor doesn't infer a and b for MkProductMorphism in preserveId
• Preorder.PreorderAsCategory doesn't typecheck unless all type-level references to transitive/reflexive are fed with po explicitly, the error is:

Can't solve constraint between:
	?__con
and
	Constraint ((Preorder t) po) conArg

[clayrat]

Pushed https://github.com/statebox/idris-ct/tree/idris2

[clayrat]

• Implicit name clashes (for j) in Free.FreeFunctor.foldPath
• MonoidalCategory.StrictMonoidalCategory.tensorIsAssociativeMor doesn't typecheck with

Can't solve constraint between:
	mapObj tensor (a, c)
and
	a

• Pattern-matching lambdas in MonoidalCategory.SymmetricMonoidalCategoryHelpers.swapFunctor don't change the goal, need to explicitly case-split to finish local proofs.

[clayrat]

• Adding unitCoherence to MonoidalCategory.SymmetricMonoidalCategory causes the compiler to crash with Segmentation fault (core dumped).

[cxandru]

TypesAsCategory doesn't compile w/ Idris2 and since I'm quite new to Idris, and can't conclude this from the error messages, I wanted to ask if this might be only a superficial (syntactic, e.g.) incompatibility (and if so how to fix it), or whether it's a more fundamental problem.

[cxandru]

TypesAsCategory doesn't compile w/ Idris2 and since I'm quite new to Idris, and can't conclude this from the error messages, I wanted to ask if this might be only a superficial (syntactic, e.g.) incompatibility (and if so how to fix it), or whether it's a more fundamental problem.

Ok I fixed some errors by addding qualifcations to the arguments to MkCategory. But the proof for rightIdentity is failing, not for leftIdentity though, curiously enough. What could be the reason?

[cxandru]

It turned out to be a bug in Idris2: idris-lang/Idris2#1370

[clayrat]

Looks like the upstream bug is fixed, is the proof going through now?