m_j_g
Joined 8 years ago
Karma
61
Submissions
54
Member since
Mar 7
marcinjangrzybowski (at) gmail.com
View on Hacker NewsRecent submissions
Comment · 12 days ago
we are moving forward steadily :)
https://github.com/marcinjangrzybowski/cubical-bis/blob/inte...
(see table in the middle of doc)
mind, that it is fully constructive implementation, you can get arbitrary precision aproximation to every real expression.
for now WIP, but soon will be aviable in cubical-library :)
also our related TYPES2026 presentation: https://types2026.cse.chalmers.se/slides/51.pdf
Comment · 8 months ago
to the point, that it is reasonable to commit altogether to the choice.
Comment · 8 months ago
This made me think of the secretary problem.
Early in life it makes sense to move on more easily, not because we value people or partners less, but because we’re still figuring out ourselves and how the world works. There’s just more uncertainty.
Later, when we know more about who we are and what fits, it’s natural to switch less.
Comment · 1 year ago
In Poland you can get one without doctors referal (for CT you need one because of ionizing radiation exposure), it cost between 100-200$ in normal, reputable hospital (not one like from the street view).
Comment · 1 year ago
vaguely related : synthetic homotopies visualisation tool - https://github.com/marcinjangrzybowski/cubeViz2
Comment · 1 year ago
Did you played with cubical flavor of Agda?
here is fun project of mine related to it : https://github.com/marcinjangrzybowski/cubeViz2
:)
Comment · 4 years ago
secound, espeicaly together with elm street for generating code from Haskell
Comment · 4 years ago
From my experience ability to turn equivalences to equlities and vice versa is very usefull. Without this you are ending in setoid hell - intracable mess of isomorphism. I suspect that also Higher Inductive Types have lots of potential to simplify practical verification effords (apart from obvious usecases of quotients and truncations)
Comment · 5 years ago
It is nice to see practical application of dependently typed language!
Comment · 5 years ago
Contrary, formal methods could (in theory!!) give as way to assess correctness of software regardless of programmer qualifications.
Comment · 5 years ago
previous video that led to wager : https://news.ycombinator.com/item?id=27330412
Comment · 5 years ago
cubical Agda : https://github.com/agda/cubical
is also worth mentioning int this context