Hackers' Pub

Syntax	Description	Examples
`"` keyword `"`	Finds the string within quotes, including spaces. Case-insensitive. (Escape quotes inside with `\"`)	`"Hackers' Pub"`
`from:` handle	Finds content written by the specified user.	`from:hongminhee` `from:hongminhee@hollo.social`
`lang:` ISO 639-1	Finds content written in the specified language.	`lang:en`
`#` tag	Finds content with the specified tag. Case-insensitive.	`#HackersPub`
condition condition	Finds content that satisfies both conditions on either side of the space (logical AND).	`"Hackers' Pub" lang:en`
condition `OR` condition	Finds content that satisfies at least one of the conditions on either side of the OR operator (logical OR).	`#HackersPub OR "Hackers' Pub" lang:en`
`(` condition `)`	Combines the operators within the parentheses first.	`(#HackersPub OR "Hackers' Pub" OR "Hackers Pub") lang:en`

VojtechStep @VojtechStep@mathstodon.xyz

3/22/2025, 9:07:37 PM

Public

After a couple months of development, one submitted master's thesis and one burnout, I'm pleased to say that I now have a formal proof of correctness of @dwarnDavid Wärn's zigzag construction of identity paths of pushouts, using the type-theoretical definition from his first note.
https://github.com/UniMath/agda-unimath/pull/1370

AFAIK this is the first completed formalized proof that it satisfies the universal property of identity systems, in any proof assistant. I'm pretty proud of myself, ngl.

If you have a fediverse account, you can quote this note from your own instance. Search https://mathstodon.xyz/users/VojtechStep/statuses/114208122937257163 on your instance and quote it. (Note that quoting is not supported in Mastodon.)