Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Colocal types #1089

Merged
merged 18 commits into from
Sep 6, 2024
Merged

Colocal types #1089

merged 18 commits into from
Sep 6, 2024

Conversation

fredrik-bakke
Copy link
Collaborator

Defines what it means for a type to be colocal at a map, and shows a few basic properties of these.

Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good 👍

@EgbertRijke
Copy link
Collaborator

Hi! I think we had this discussion with Tom before, when we should speak of the diagonal and when we should speak of the constant map. Eg: it is misleading to say that "the constant map is an equivalence" if it is merely meant that A -> (B -> A) is an equivalence. It is much clearer to say that the diagonal map is an equivalence in this case. We were fairly careful about when to use the word "diagonal" and when to use the word "constant map".

In this pull request I see some changes from "diagonal" back to "constant map". Is the above consideration taken into account here?

@EgbertRijke EgbertRijke enabled auto-merge (squash) September 6, 2024 16:57
@EgbertRijke EgbertRijke merged commit 838916f into UniMath:master Sep 6, 2024
4 checks passed
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.

None yet

3 participants