Relicense derivative work from TypeTopology

[fredrik-bakke]

Certain parts of the library are improperly licensed since they contain or depend on derivative work from the TypeTopology library, which is licensed under the copyleft license GPL 3.0. This license stipulates that such work must be licensed under the same GPL 3.0 license itself, which is not done currently.

This issue can be broken into three action items:

• Identify which parts of the library contain derivative work from the TypeTopology library.
• Determine the proper way to license individual pages #1636
• Relicense these and dependent pages, meaning any file that imports a file with the GPL 3.0 license must itself be licensed under GPL 3.0.

Thanks to @VojtechStep for initially raising the question to me about this licensing issue.

Derivative works from TypeTopology

• Cantor-Schröder-Bernstein #182 Editing CSB and split-surjective files & Adding set theory folder #183 contributed the Cantor–Schröder–Bernstein theorem as a translation from the TypeTopology library.

work in-progress

[VojtechStep]

See also how a similar situation was handled in cubical agda/cubical#1021 and the discussion linked there. IIUC the final resolution was for the 1lab (where the code was adapted from, and which is GPL) to relicense the files under BSD (after getting consent from contributors to those files) so that they can be copied to cubical, and then cubical could keep most of the code under MIT with exception for the individual files. I'm not sure if we can actually distribute agda-unimath under MIT with some files under GPL