nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 (nprofile…6kk0) in oktt you write
The most well-adapted way to add a universe is in the Tarskian style; universes à la Russell should be understood as a matter of elaboration, definitely not as a matter of semantics.
and in Algebraic Type Theory and Universe Hierarchies you write
It is commonly believed that algebraic notions of type theory support only universes à la Tarski, and that universes à la Russell must be removed by elaboration. We clarify the state of affairs […]
What's the story here? Did you change your mind, or am I missing the point and this is not actually a contradiction? I'm not sure what the chronological relation is between the two papers.
Also, in the latter paper you write
concrete computerized implementations of type theory tend to be much closer to the abstract syntax of the initial cwf than to the “raw” syntax which some have insisted is a primary object of study.
Did you have anything specific in mind? Is this about NbE?
Naïm Camille Favier
npub1av…z5z7z
2025-04-13 13:58:30 UTC
Author Public Key
npub1avwd5p4zn7ndkvjf9qtrsddacax0cvmujryu2qnlxcm6nmlnquwqxz5z7zPublished at
2025-04-13 13:58:30 UTCEvent JSON
{
"id": "cbabf20ee4c3c1c6b46eacfe305cda22b434dc3a57addbafed3b09e1c763a786",
"pubkey": "eb1cda06a29fa6db324928163835bdc74cfc337c90c9c5027f3637a9eff3071c",
"created_at": 1744552710,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.mostr.pub"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.mostr.pub"
],
[
"proxy",
"https://types.pl/users/ncf/statuses/114331006461890746",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.mostr.pub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 in oktt you write\n\nThe most well-adapted way to add a universe is in the Tarskian style; universes à la Russell should be understood as a matter of elaboration, definitely not as a matter of semantics.\n\nand in Algebraic Type Theory and Universe Hierarchies you write\n\nIt is commonly believed that algebraic notions of type theory support only universes à la Tarski, and that universes à la Russell must be removed by elaboration. We clarify the state of affairs […]\n\nWhat's the story here? Did you change your mind, or am I missing the point and this is not actually a contradiction? I'm not sure what the chronological relation is between the two papers.\n\nAlso, in the latter paper you write\n\nconcrete computerized implementations of type theory tend to be much closer to the abstract syntax of the initial cwf than to the “raw” syntax which some have insisted is a primary object of study.\n\nDid you have anything specific in mind? Is this about NbE?",
"sig": "52c5f249b937349e434715d06e79e27fae972b9a9916ae1eb9ea17ebd73ea5f511b95ecddc840f2b3ebb3af9e5a7a3e921627d27c3f9916622750f8a2731f169"
}