Various STLC fixes

[rokopt]

I'm making this pull request a draft because we want to either break it up into several new PRs or integrate bits of it with existing PRs or something. But I am creating the PR because I can't figure out how to test the code without CI; asdf doesn't seem to run newly-written tests no matter what I do (including deleting a bunch of files), at least for some unpredictable period of time; it eventually happens for reasons that I don't understand any more than I understand the reasons that it doesn't happen right away.

The contents of the PR:

• Convert some type parameters in the Idris-2 code for lambda from implicit to explicit, to make comparing the Lisp code to it easier
• Add a test for #58
• Try to fix #58 by fixing a couple of parameters to morphism constructors in the so0 and so1 cases of curry that were using the wrong arguments
• Add the codomain type to the spec for the absurd STLC term (see comment https://github.com/anoma/geb/issues/53#issuecomment-1421093312 to #53)
• Add the left and right components of the codomain to the spec for the left and right STLC terms for #53
• Add an external API for computing hom-objects for #60

[rokopt]

(The latest CI failures are due to less-than not being hooked in to end-to-end tests yet.)

[rokopt]

I've added explicit type information to lamda:left and lambda:right for #53 .

Unfortunately, the type-checking is commented out at the moment, because it fails as follows:

Types should match for left s-1 s-1 BOOL

Those types should match, so the object-equality test must still be insufficient, at least for BOOL. Maybe #71 would fix this?

[mariari]

I've added explicit type information to lamda:left and lambda:right for #53 .

Unfortunately, the type-checking is commented out at the moment, because it fails as follows:

Types should match for left s-1 s-1 BOOL

Those types should match, so the object-equality test must still be insufficient, at least for BOOL. Maybe #71 would fix this?

probably not, for now you can check past aliases, with the meta data patch being in, we can deprecate any pattern where we match on aliases, and instead have them be implicit in the code we call

[rokopt]

All of the commits from this PR have now been merged to main in other PRs, so I'm closing this one.