Skip to content

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented May 1, 2023

cf. #1954 / #1962 and @JacquesCarette 's request for comparison. See also issue #1957 for blocking dependencies.

Besides library design issues, the only real difference is that of the arity (0, rather than 2) of the pt constructor, and hence also of the cong/homo properties of the associated Is*Homomorphism records. Otherwise, it was pure cut-and-paste, modulo the additional infrastructure for Identity and Composition for IsPointedHomomorphism.

@JacquesCarette
Copy link
Contributor

The reason for the exercise was to show just how deeply the cut-and-paste goes.

@jamesmckinna
Copy link
Contributor Author

I'll close this for now, but potentially re-open it once:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants