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

Only recur for comparing in Glue if φ breaks down #6013

Merged
merged 2 commits into from
Aug 14, 2022
Merged

Only recur for comparing in Glue if φ breaks down #6013

merged 2 commits into from
Aug 14, 2022

Conversation

plt-amy
Copy link
Member

@plt-amy plt-amy commented Aug 9, 2022

Fixes #5955. I added some comments to the code explaining the change. The problem was that, when comparing terms at type Glue φ T, the conversion checker would try to decompose φ into faces, and recursively compare each face under the resulting substitutions (this is compareTermOnFace/forallFaceMaps).

But some expressions are indecomposable, e.g. φ i, and in that case, compareTermOnFace would try comparing m, n at type (Glue φ T)[idS].. i.e., exactly the situation we started in. Not good for termination!

@andreasabel
Copy link
Member

@plt-amy : This is off-topic, but I couldn't find your email-address (and I do not twitter). I see that you have genuine interest in Cubical Agda. We are currently lacking an active maintainer, since the original author Andrea @Saizan is occupied by his new job and can only occasionally give some direction. If you are happy with that, you can get commit-rights and thus extra responsibility and look after Cubical Agda a bit.
What further development concerns, Christian @csattler has ideas about making cofibrations a proper sort (they are currently represented as interval expressions); he has convinced me that this is a good way forward. Otherwise, I haven't heard about directions Cubical Agda should go.

@plt-amy
Copy link
Member Author

plt-amy commented Aug 14, 2022

I was actually thinking of asking whether I could take over stewardship of the cubical bits 😅 I've been discussing possible improvements with Anders @mortberg and trading implementation ideas with the cooltt folks (@jonsterling et al).

(edit: my email is me [at] amelia.how)

@plt-amy plt-amy merged commit 8fab59d into agda:master Aug 14, 2022
@andreasabel
Copy link
Member

I was actually thinking of asking whether I could take over stewardship of the cubical bits

This is excellent news! Welcome to the team!

@andreasabel andreasabel added the cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp label Aug 15, 2022
@andreasabel andreasabel added this to the 2.6.3 milestone Aug 15, 2022
@mortberg
Copy link
Collaborator

mortberg commented Aug 15, 2022

I was actually thinking of asking whether I could take over stewardship of the cubical bits sweat_smile I've been discussing possible improvements with Anders @mortberg and trading implementation ideas with the cooltt folks (@jonsterling et al).

(edit: my email is me [at] amelia.how)

This is great news! @plt-amy Don't hesitate to @ me here or request a review from me. I'm not actively following the Agda Github as I haven't figured out a way to filter out the cubical parts that I'm mainly interested in... So unless I'm explicitly notified it's very likely that I miss something

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Composition of Glue Type Causes Infinite Loop
3 participants