Skip to content

Split Yoneda embedding into separate module and rename helper functions#1299

Open
dancewithheart wants to merge 3 commits intoagda:masterfrom
dancewithheart:yoneda-embedding-split
Open

Split Yoneda embedding into separate module and rename helper functions#1299
dancewithheart wants to merge 3 commits intoagda:masterfrom
dancewithheart:yoneda-embedding-split

Conversation

@dancewithheart
Copy link

@dancewithheart dancewithheart commented Mar 13, 2026

Split the Yoneda embedding definitions out of
Cubical.Categories.Yoneda into a separate module
Cubical.Categories.Yoneda.Embedding.

The main names are re-exported from Cubical.Categories.Yoneda
to preserve the existing interface.

Also rename helper functions:

  • yo-yo-yoyonedaToElement
  • no-no-noelementToYoneda

Partially address #1285.

@maxsnew
Copy link
Collaborator

maxsnew commented Mar 13, 2026

What's the impetus for splitting it into two files?

@dancewithheart
Copy link
Author

I treated the split as part of the cleanup: the file mixes the core Yoneda lemma
(yoneda, yonedaᴾ, yoneda*, yonedaᴾ*) with the embedding/application
definitions (yo, YO, isFullYO, isFaithfulYO, isFullyFaithfulYO).

The idea was simply to separate those. I re-exported from Yoneda to preserve
the current interface.

If the extra file is not desirable, I'm happy to keep everything in one file
and limit the PR to the renames.

I also thought it might be useful to import the lemma without the embedding
machinery, though that alone may not justify a separate file.

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants