Henry
@bblfish
died suddenly on 5th September 2023.
His family can be contacted via tini_story@yahoo.com and ghalavanja@gmail.com
Born 29th July 1967, died 5th September, 2023
his family can be contacted via tini_story@yahoo.com and ghalavanja@gmail.com
Henry Story has been working on Decentralised social Networks since 2004 when he took up foaf, contributing to the Atom Syntax syndication format, WebID Authentication, Linked Data Protocol, Social Linked Data Platform (Solid), and more... He read philosophy and earns a living programming in #Scala
Henry
@bblfish
died suddenly on 5th September 2023.
His family can be contacted via tini_story@yahoo.com and ghalavanja@gmail.com
The Cyber Resilience Act is being finalised in the next two weeks, despite the parts that could deeply harm #OpenSource. Rather than suggesting changes to the #CRA (plenty of others doing so), here's an article explaining why changes are still necessary despite the 11th hour.
@ivan_herman @scotth I have been using omnigraffle for 20 years nearly. There were not that many alternatives at the time.
@scotth @ivan_herman Omnigraffle see graffle file in https://github.com/co-operating-systems/PhD/tree/main/Logic/VC/model2
Economics starts with #barter
https://twitter.com/TansuYegen/status/1698228580482695370
🗓️ 11-15 Sept.: the @w3c community is going to #Seville 🇪🇸 for #w3cTPAC! This week is dedicated to discussions in and between groups to gather new ideas, raise questions and better coordinate the #WebStandards work.
https://www.w3.org/2023/09/TPAC/
Today attending The Future of Decentralization, AI, and Computing Summit at UC Berkeley
NQueens Combinational Puzzle Meets Cats by Philip Schwarz #scala https://youtu.be/1g5bzeGbKiI?si=d0q7AHZcayZLqsan :scala:
Latest edition of #scalanews is out all! Enjoy! #scala :scala: 🎉📰https://www.scalanews.net 🗞️🚀 :scala:
cc @ross @typelevel @majkp @adamwarski @softwaremill @scala_lang @alexelcu
I've tried to determine the best U.S. president by purely scientific means. After tossing over a thousand coins, I can report that the best president is Washington, Lincoln, or Jefferson.
Yet another great #Veritasium video! ❤️💕
How The Most Useless Branch of #Math Could Save Your Life https://www.youtube.com/watch?v=8DBhTXM_Br4 #knottheory #topology #watching📺
@ivan_herman I drew some graphics last week to explain a deep logical problem with Verifiable Claims that work in dark and light modes. #Accessibility
https://github.com/w3c/vc-data-model/issues/1248#issuecomment-1697508577
@ivan_herman I drew some graphics last week to explain a deep logical problem with Verifiable Claims that work in dark and light modes. #Accessibility
https://github.com/w3c/vc-data-model/issues/1248#issuecomment-1697508577
@dbdc4dc6031900bb2cbce65958f468fb2af3c4251e5a2c84f4e93836522686fb
#Yakihonne's web site is https://yakihonne.com
and supports #Math mode markdown apparently - I need to try it out.
Designing for dark mode === dark art 😞
I know there is a way with CSS. But if one generates SVG from a tool (google draw, draw.io, whatever) and wants the result to be used in its original form (e.g., light mode) as well as when the browser forces dark mode: it becomes a royal pain. The result depends on browser, plugin, OS...
Are there "standards" on how browsers should do that? Should there be? How can one prepare for this?
Just a Ghent appreciation post.
My city. Incredibly happy I was able to design my life entirely within her.
Definition. A type D is injective if for every embedding j : X → X' and any function f : X → D, we can find a function f' : X' → D that extends f along j, in the sense that f' ∘ j = f.
Discussion. In HoTT/UF we have two choices. We may merely require that f' exists, or that it be explicitly given. Depending on the choice, we arrive at the notions of "injective" and "algebraically injective" type respectively.
I have studied both. Here I will restrict myself to "algebraically injective" types, for simplicity, which I will refer to as "injective" for the sake of brevity. I hope this will cause no confusion.
I developed a lot of results for (algebraically) injective types in my github repository TypeTopology [1] and then published them in the article [2]
[1] https://www.cs.bham.ac.uk/~mhe/TypeTopology/InjectiveTypes.index.html
[2] https://doi.org/10.1017/S0960129520000225
What I want to do in this thread is to quickly review what I did in that paper and then list some new results about injectivity that I have developed in TypeTopology that haven't been published yet.
(This was a longer introduction than I intended!)
11/
Having motivated the extension problem and constructivity in HoTT/UF, we move to the subject matter of this thread.
The general situation is that we have a function X → Y, and we want to extend it to a function X' → Y, where X' enlarges X.
If we did have excluded middle available, in general, the extension problem would always be solvable for non-empty Y. Given f : X → Y, we can define f' : X' → Y by f'(x) = f (x) if x in in X, and f'(x) = some arbitrarily chosen point of Y otherwise.
(You may need some additional amount of choice for this, if the assumption is simply that Y is non-empty, but I don't want to discuss this now.)
10/
Why do we care about constructive mathematics? There are zillions of reasons, depending on the constructive mathematician we speak to. The purpose of this thread is not to discuss that.
But here I want to mention two reasons that matter to me and to lots of people working on HoTT/UF.
(9.1) HoTT/UF can be interpreted in any ∞-topos, so that any statement in HoTT/UF means something in that topos.
A definition, or construction or proof in HoTT/UF makes sense in any ∞-topos.
Except if we go non-constructive and assume excluded middle and choice.
Proofs and constructions that use excluded middle, in HoTT/UF, apply only to so-called *boolean* ∞-toposes. Very few ∞-toposes are boolean.
So a main reason to be "constructive" (that is, avoid excluded middle and choice) is to be more general, in the sense of accounting for all ∞-toposes, not just the boolean ones.
(9.2) HoTT/UF can be used to compute. For example, we can compute in HoTT/UF using cubical Agda.
Not everybody, in the mathematical community, is interested in ∞-toposes (but for example Peter Scholze is, among many other people).
Not everybody is interested in computing (but a lot of us here are).
If you are not interested in (9.1) or (9.2), you will probably wish to stop reading this thread, unless you are curious to see what is going on.
9/