Naïm Camille Favier on Nostr: What do you get if you interpret "f : A → B is surjective" (∀ b : B. ∃ a : A. ...
What do you get if you interpret "f : A → B is surjective" (∀ b : B. ∃ a : A. f(a) = b) in the internal language of a [whatever adjectives you need to make sense of that statement] category? I think the existential should be interpreted as the inclusion im f → B in a regular category, so the ∀ should give you a section of that? What flavour of epimorphism is this?
Published at
2025-05-21 16:55:25 UTCEvent JSON
{
"id": "710ee789766bef1901ba80bc1bbc4bd6953f6d5c9fbbc2f84022b2c9b9107651",
"pubkey": "eb1cda06a29fa6db324928163835bdc74cfc337c90c9c5027f3637a9eff3071c",
"created_at": 1747846525,
"kind": 1,
"tags": [
[
"proxy",
"https://types.pl/users/ncf/statuses/114546869898552906",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.mostr.pub"
]
],
"content": "What do you get if you interpret \"f : A → B is surjective\" (∀ b : B. ∃ a : A. f(a) = b) in the internal language of a [whatever adjectives you need to make sense of that statement] category? I think the existential should be interpreted as the inclusion im f → B in a regular category, so the ∀ should give you a section of that? What flavour of epimorphism is this?",
"sig": "2a2e1b46bbe8121e8fb1588234859b282607e880d68b2187a66e9dcae2eeeb40def40af83e705323c1e08b5eb015b5765d6111146ab69780ba7601afd5e07926"
}
