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

Refactor funext #878

Merged
merged 1 commit into from
Oct 22, 2023
Merged

Refactor funext #878

merged 1 commit into from
Oct 22, 2023

Conversation

fredrik-bakke
Copy link
Collaborator

@fredrik-bakke fredrik-bakke commented Oct 22, 2023

Minor refactor of funext to follow the new naming scheme.
There are still some things that could be improved:

  • The file on homotopy induction
  • Refine the connection between weak funext and funext
  • A more detailed treatment of the connection between univalence and funext. Currently, it is not clear where exactly univalence is even needed in the argument, and that A and B are assumed to live in the same universe is not commented on.

@EgbertRijke
Copy link
Collaborator

LGTM

@EgbertRijke EgbertRijke enabled auto-merge (squash) October 22, 2023 13:21
@EgbertRijke
Copy link
Collaborator

And I will be in a little bit of trouble because that synthetic homotopy theory refactor refactored funext too:P

@fredrik-bakke
Copy link
Collaborator Author

See! Would've been nice to have!

@EgbertRijke EgbertRijke merged commit d842de8 into UniMath:master Oct 22, 2023
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.

2 participants