Add some type relations and isomorphisms #2419
Conversation
| -- primed variants are more level polymorphic | ||
|
|
||
| ×-distribˡ-⊎′ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C) | ||
| ×-distribˡ-⊎′ = Σ-distribˡ-⊎ |
There was a problem hiding this comment.
Following the convention of Function.Base then the primes should be on the less polymorphic lemmas rather than the more polymorphic lemmas?
There was a problem hiding this comment.
Yes, I wasn't sure about backwards compatibility. If you think it's fine I'll swap the two. Do you think ×-distrib-⊎ should also be primed for consistency, even though it probably doesn't make sense to add a non-primed version?
There was a problem hiding this comment.
I think ×-distrib-⊎ should stay as is because it is already non-dependent because it uses _×_ rather than ∃. The additional advantage is that this doesn't have backward compatibility problems!
There was a problem hiding this comment.
Apologies for the recent flurry of (now deleted) suggestions here. I realise that I wasn't quite understanding how this PR adds more polymorphic versions, and reimplements the prior functionality in these terms, but I'd be tempted to suggest that we 'just' take the more polymorphic versions... would this be a breaking change? Or potentially give rise to unsolved metas?
|
Ah, and a CHANGELOG entry would be great! |
|
I'll add the CHANGELOG once 2.1 is out. |
|
@WhatisRT any progress on the suggested changes? This should be easy to merge once you've done that... |
WhatisRT
force-pushed
the
add-type-relations
branch
from
f664387
to
e6f51de
Compare
|
I've added the changes to the CHANGELOG. I don't really understand what's the final verdict on the naming, should I change some of the names or not? |
|
Yes, some of the names do need changing from what's in your PR. But some of the name changes you did do were not necessary! |
|
I think that it would be good to try to merge this sooner rather than later, and AFAICT, it's down to agreeing names for the new additions... can we converge on mutually agreeable suchl!? |
|
Looks like the master merge broke the build? |
Nope... (I think) it's a CI thing... the rebuild of |
|
Reading the comments, it looks like we have got consensus on the names? |
Yes, I'd been waiting on @WhatisRT to update this PR, but if you're keen to merge now (and for sure, this PR prompted me to think harder about some other type isos which might usefully be added downsream, esp. as regards refactoring |
|
Sorry, I think I missed some of the naming suggestions. But it seems you all have way stronger opinions about that than I do so I'd rather let you do the final adjustments. |
Name change inherited from source update
Remove redundant parentheses
|
I think if @JacquesCarette or @MatthewDaggitt can resolve the questions about level polymorphism and its impact on names (I managed to confuse myself too much over this to do so :-() then following @WhatisRT 's most recent comment, then you should make those changes yourselves and merge! |
|
Looking again at all this: the less/insufficiently polymorphic versions of the distributive laws are also present in Also (but separate from this PR): in each module, |
|
How should we proceed with this? Merge as is, and refactor later? |
Upstreaming some functions that I've used to prove things about sets (not the Agda kind).