Henry

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

2023-09-10

Henry
@bblfish
died suddenly on 5th September 2023.
His family can be contacted via tini_story@yahoo.com and ghalavanja@gmail.com

Henry boosted:
2023-09-05

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.

blog.opensource.org/diverse-op

#SoftwareFreedom #FOSS #FLOSS #Policy @EU_Commission

2023-09-05

@ivan_herman @scotth I have been using omnigraffle for 20 years nearly. There were not that many alternatives at the time.

Henry boosted:
W3C Developersw3cdevs@w3c.social
2023-09-04

🗓️ 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.
w3.org/2023/09/TPAC/

W3C TPAC 2023 - hybrid meetings from 11 to 15 September 2023 - Seville, Spain
Henry boosted:
SalarRahmanian :scala: :nixos:softinio@fosstodon.org
2023-09-04

Today attending The Future of Decentralization, AI, and Computing Summit at UC Berkeley

Henry boosted:
SalarRahmanian :scala: :nixos:softinio@fosstodon.org
2023-09-04

NQueens Combinational Puzzle Meets Cats by Philip Schwarz #scala youtu.be/1g5bzeGbKiI?si=d0q7AH :scala:

Henry boosted:
SalarRahmanian :scala: :nixos:softinio@fosstodon.org
2023-09-04

Latest edition of #scalanews is out all! Enjoy! #scala :scala: 🎉📰scalanews.net 🗞️🚀 :scala:

cc @ross @typelevel @majkp @adamwarski @softwaremill @scala_lang @alexelcu

Henry boosted:
EdisonMaxwell ☑️EdisonMaxwell@mathstodon.xyz
2023-09-03

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.

Henry boosted:
Vladimir Savićfirusvg
2023-09-03

Yet another great video! ❤️💕

How The Most Useless Branch of Could Save Your Life youtube.com/watch?v=8DBhTXM_Br4 📺

Henry boosted:
2023-09-03

@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

github.com/w3c/vc-data-model/i

2023-09-03

@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

github.com/w3c/vc-data-model/i

2023-09-03

@dbdc4dc6031900bb2cbce65958f468fb2af3c4251e5a2c84f4e93836522686fb
#Yakihonne's web site is yakihonne.com
and supports #Math mode markdown apparently - I need to try it out.

Henry boosted:
EOIN ꙮ GAIRLEGomega9@quietplace.xyz
2023-09-02
Henry boosted:
2023-09-02

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?

Henry boosted:
Pieter Colpaertpietercolpaert
2023-09-02

Just a Ghent appreciation post.

My city. Incredibly happy I was able to design my life entirely within her.

Street with lights acrossBirds art installation near the water at Ajuinlei in GhentEarly morning view from the St. Michael bridge on the 3 towers of Ghent.De Krook, my workplace and public library
Henry boosted:
2023-09-02

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] cs.bham.ac.uk/~mhe/TypeTopolog

[2] doi.org/10.1017/S0960129520000

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/

Henry boosted:
2023-09-02

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/

Henry boosted:
2023-09-02

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/

Client Info

Server: https://mastodon.social
Version: 2025.04
Repository: https://github.com/cyevgeniy/lmst