daniel gratzer on Nostr: Chapter 3 deals with this stuff a bit! C-f for injectivity there (and see Theorem ...
Chapter 3 deals with this stuff a bit! C-f for injectivity there (and see Theorem 3.5.19 for a proof that ETT lacks injective pi types)
daniel gratzer
npub1zw…3df7y
2026-09-23 17:55:06 UTC
in reply to nevent1q…yy6g
Author Public Key
npub1zwlhl84xnlyyzkpqrk6yg782jz9e3v37kznxpjpe0jexjq8kq7vqq3df7ySeen on
wss://relay.momostr.pinkPublished at
2026-09-23 17:55:06 UTCEvent JSON
{
"id": "794e1cf4480d9629f65eda11b03cabd218f06bd41e7698c2af8db40ee646f66f",
"pubkey": "13bf7f9ea69fc84158201db44478ea908b98b23eb0a660c8397cb26900f60798",
"created_at": 1790186106,
"kind": 1,
"tags": [
[
"e",
"9df808bf9eb52e612c76ca51678406f8708db5b372e2bb287af049712abaff1c",
"",
"reply",
"8a8316532b57248ac82db7d866a32a07d9f14900eafa3f7c3b4f4662c09f79a9"
],
[
"proxy",
"https://mathstodon.xyz/@danielgratzer/117321636694386970",
"web"
],
[
"p",
"8a8316532b57248ac82db7d866a32a07d9f14900eafa3f7c3b4f4662c09f79a9"
],
[
"e",
"cb389b3399d0435b639c6f31ae91ccf6599a53b99887cde7c1e868048e5d3d68",
"",
"root",
"052692b03bfd5ad998de06638938bd239d9ee776cdb49e1ddd41edc727270803"
],
[
"p",
"13bf7f9ea69fc84158201db44478ea908b98b23eb0a660c8397cb26900f60798"
],
[
"p",
"052692b03bfd5ad998de06638938bd239d9ee776cdb49e1ddd41edc727270803"
],
[
"proxy",
"https://mathstodon.xyz/users/danielgratzer/statuses/117321636694386970",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://mathstodon.xyz/users/danielgratzer/statuses/117321636694386970",
"pink.momostr"
],
[
"-"
]
],
"content": "Chapter 3 deals with this stuff a bit! C-f for injectivity there (and see Theorem 3.5.19 for a proof that ETT lacks injective pi types)",
"sig": "fb0a3dfa79cb41a798200c209d34a3fb305009ff479358f0eb0d49987a61484d66de42588c6ad4cd87eec61c47eb529d979f67c198b5101cc84f51d2dac6c28a"
}