4 ms·

Thanks. It just felt like being unable to spell out the empty bunch should be as interesting as the nonexistence of bunches o' bunches. I've heard from the st

Thanks. It just felt like being unable to spell out the empty bunch should be as interesting as the nonexistence of bunches o' bunches. I've heard from the students of RLC that quotient types are potentially useful** so should I wait to find out from you when those subtleties turn out to be less annoying or schlep on my current path till I bump up against bumpkin-type*-related annoyances not entirely of my own making ? *Sum & product types,I'm either always told not to worry about them, or be asked to pay attention in a way that I think I probably shouldn't ** itswise.. for bits-schlepping often end up needing more marketing than it's worth, imex

082349872349872 2y ago
Re: quotient types, I believe so, even bitswise... but it's exactly the projection forgetting all that stuff that's in the same class as zero that's easier mathematically than computationally. (guess I should see what Lean does here) incidentally, rummaging by way of Hagino and Charity leads to Burstall87: http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-25/ECS-LFCS-87-25.pdf http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-25/ECS-L... (what Burstall has written as ind case is what we'd currently call fold) in particular, 5. Equational data types (cut down by eq's <== quotients) which has the interesting observation: > Notice that the initial algebra gives rise to an induction principle and to use this we have to invent a suitable predicate to prove by induction. This comes from the 'no junk' property of the initial algebra. The 'no confusion' property gives rise to inequations, and here to do proofs we have to invent a suitable discriminant function. There is some pleasant feeling of duality here.
- gsf_emergency 2y ago
  So there's already pleasance?? Sorry, can't add anything substantive, but the following might save some time? https://proofassistants.stackexchange.com/questions/908/what-exactly-is-setoid-hell/927#927 https://proofassistants.stackexchange.com/questions/908/what... https://eprints.illc.uva.nl/id/document/12673 https://eprints.illc.uva.nl/id/document/12673
  - 082349872349872 2y ago
    many thanks! "Observational Equality: Now for Good" led me to "Observational Equality, Now!" which is a little easier for the layman to read without developing a headache: "Observational Equality: Ow!"
    - gsf_emergency 2y ago
      Heh I'm surprised (as in your fencing related dicta) that you got back on the trail.. what was the link chain?? Edit: if I told you this was the most layman paper I could find on my secondary (mostly killer-mode) ikigai, could you maybe deduce what the problem statement (aka MVP, to use some old country lingo) is, and even find a more appropriate paper for a layman? https://ems.press/content/serial-article-files/48098 https://ems.press/content/serial-article-files/48098
      - 082349872349872 2y ago
        hmm. I'd remembered it was short (3 hops?) from 42470111 but now I'm not seeing how I first got to TT^Obs from either of those starting points... cubic diracs are well out of my ken — even normal square ones are. are casimir elements and spins somewhere in the correct general direction? (otherwise the cubic doesn't make sense to me, as I don't think jerk normally enters physically motivated diffy-qs?)
        gsf_emergency 2y ago
        If by spins you mean Cliff(Lie) then you got the 2 swords* I'm quite intrigued that enwiki hasn't vibed about that, but it has produced a lagniappe: P81 The shaggy steed of physics: mathematical beauty in the physical world Casimir elements, heh, it's why my Erdos number is lower than expected.. * or is it a pitchfork? also vibing currently that the hypernormal distrust models that appear simpler than their own, while the weird have the opposite inclination. Holding in mind that dynamic between YeGoblyneQueene & g***n as a fine example of the ur academic conflict which I believe Taleb was trying to direct attention to

082349872349872 2y ago

Re: quotient types, I believe so, even bitswise... but it's exactly the projection forgetting all that stuff that's in the same class as zero that's easier mathematically than computationally. (guess I should see what Lean does here) incidentally, rummaging by way of Hagino and Charity leads to Burstall87: http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-25/ECS-LFCS-87-25.pdf http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-25/ECS-L... (what Burstall has written as ind case is what we'd currently call fold) in particular, 5. Equational data types (cut down by eq's <== quotients) which has the interesting observation: > Notice that the initial algebra gives rise to an induction principle and to use this we have to invent a suitable predicate to prove by induction. This comes from the 'no junk' property of the initial algebra. The 'no confusion' property gives rise to inequations, and here to do proofs we have to invent a suitable discriminant function. There is some pleasant feeling of duality here.

gsf_emergency 2y ago
So there's already pleasance?? Sorry, can't add anything substantive, but the following might save some time? https://proofassistants.stackexchange.com/questions/908/what-exactly-is-setoid-hell/927#927 https://proofassistants.stackexchange.com/questions/908/what... https://eprints.illc.uva.nl/id/document/12673 https://eprints.illc.uva.nl/id/document/12673
- 082349872349872 2y ago
  many thanks! "Observational Equality: Now for Good" led me to "Observational Equality, Now!" which is a little easier for the layman to read without developing a headache: "Observational Equality: Ow!"
  - gsf_emergency 2y ago
    Heh I'm surprised (as in your fencing related dicta) that you got back on the trail.. what was the link chain?? Edit: if I told you this was the most layman paper I could find on my secondary (mostly killer-mode) ikigai, could you maybe deduce what the problem statement (aka MVP, to use some old country lingo) is, and even find a more appropriate paper for a layman? https://ems.press/content/serial-article-files/48098 https://ems.press/content/serial-article-files/48098
    - 082349872349872 2y ago
      hmm. I'd remembered it was short (3 hops?) from 42470111 but now I'm not seeing how I first got to TT^Obs from either of those starting points... cubic diracs are well out of my ken — even normal square ones are. are casimir elements and spins somewhere in the correct general direction? (otherwise the cubic doesn't make sense to me, as I don't think jerk normally enters physically motivated diffy-qs?)
      - gsf_emergency 2y ago
        If by spins you mean Cliff(Lie) then you got the 2 swords* I'm quite intrigued that enwiki hasn't vibed about that, but it has produced a lagniappe: P81 The shaggy steed of physics: mathematical beauty in the physical world Casimir elements, heh, it's why my Erdos number is lower than expected.. * or is it a pitchfork? also vibing currently that the hypernormal distrust models that appear simpler than their own, while the weird have the opposite inclination. Holding in mind that dynamic between YeGoblyneQueene & g***n as a fine example of the ur academic conflict which I believe Taleb was trying to direct attention to