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

use Quotient in ua library #1810

Merged
merged 1 commit into from
Jan 13, 2024

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Jan 12, 2024

The use of quotient here was easy to replace. In a few places, cbn is replaced with simpl as Quotient interacts poorly with cbn, probably because of simpl never.

Signed-off-by: Ali Caglayan <[email protected]>
Copy link
Collaborator

@jdchristensen jdchristensen left a comment

Choose a reason for hiding this comment

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

LGTM. IIRC, the goal is to remove HIT.quotient, right?

@Alizter
Copy link
Collaborator Author

Alizter commented Jan 13, 2024

@jdchristensen yes. There are some universe issues with the newer quotient in the Classes library, whcih is why I started inspecting the universe levels closely.

@Alizter Alizter merged commit ab9faec into HoTT:master Jan 13, 2024
23 checks passed
@Alizter Alizter deleted the ps/branch/use_quotient_in_ua_library branch January 13, 2024 00:52
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