4 ms·

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 math

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

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