Equivalence of conatural types #330
Conversation
|
Thanks, @Seiryn21 . Yes, this is what I wanted! Let me review it in the next few days. Thanks for your contribution. |
There was a problem hiding this comment.
Thanks! And sorry for the late review - the pull request came at end of term with too many things to deal at work. Yes, this is what I wanted in the TODO. Would you mind explaining a bit more for the benefit of our readers? Short sentences will be enough.
If you prefer, I can accept the pull request as it is, and add comments myself after that, but it is probably better if you do it.
source/Unsafe/CoNat-Equiv.lagda
Outdated
|
|
||
| \end{code} | ||
|
|
||
| This implementation of CoNat comes from Cubical, the bisimilarity relation can |
There was a problem hiding this comment.
Maybe say from the "Cubical Agda Library".
source/Unsafe/CoNat-Equiv.lagda
Outdated
| \end{code} | ||
|
|
||
| This implementation of CoNat comes from Cubical, the bisimilarity relation can | ||
| be proven to be equivalent to equality, but not in classical Agda |
There was a problem hiding this comment.
Add full stop to the sentence.
source/Unsafe/CoNat-Equiv.lagda
Outdated
|
|
||
| \begin{code} | ||
|
|
||
| CoNat' : Set |
There was a problem hiding this comment.
Could we use the TypeTopology conventions, for universes, rather than Set?
| data _＝C'_ x y where | ||
| con : x ＝C'' y → x ＝C' y | ||
|
|
||
| record _＝C_ x y where |
There was a problem hiding this comment.
Maybe a few more comments would be in order, in the spirit of TypeTopology, which tried (often, but not always) to explain what's going on. I suppose this is the bisimilarity relation aluded to above.
|
Because your pull request is officially "work in progress", I can't merge it. |
|
That should be good, and Happy Holidays to you too ! |
@martinescardo Is this what you wanted in #309 ?