nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 (nprofile…6kk0) nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq9q3q6p8cfsc52e8thrsdhmy8hyqmnwxja4f5zq7s7elj3e75fk4qq8fcvf (nprofile…fcvf)
yea looks like a simpler version of cubical to me: sacrifice definitional proof irrelevance and transport refl is identity to get extensionality principles
Max S. New ⚜️
npub1dm…g9dey
2025-06-26 15:51:54 UTC
in reply to nevent1q…66e2
Author Public Key
npub1dmn630rgl55pt7vgee6l930wfqjq6jry973hqf90fs6kgxztzd8qrg9deySeen on
wss://relay.mostr.pubPublished at
2025-06-26 15:51:54 UTCEvent JSON
{
"id": "4c8d05334374970a63362ce857cb5a31036a66acd443fb0bb6fbfa457b4d2f25",
"pubkey": "6ee7a8bc68fd2815f988ce75f2c5ee48240d48642fa37024af4c3564184b134e",
"created_at": 1750953114,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.mostr.pub"
],
[
"p",
"28220d04f84c314564ebb8e0dbec87b901b9b8d2ed534103d0f67f28e7d44daa",
"wss://relay.mostr.pub"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.mostr.pub"
],
[
"p",
"94d514e6ef5c91f63b660e44fcc0cbfda85ebaf99e6f8ceed3b1c4746cc76a85",
"wss://relay.mostr.pub"
],
[
"e",
"e0632ad561f070fc3531f108d3ff4bda505ff710ceca6b22285a00164b0ca187",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://types.pl/users/maxsnew/statuses/114750463328724164",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.mostr.pub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq9q3q6p8cfsc52e8thrsdhmy8hyqmnwxja4f5zq7s7elj3e75fk4qq8fcvf \n\nyea looks like a simpler version of cubical to me: sacrifice definitional proof irrelevance and transport refl is identity to get extensionality principles",
"sig": "d90df9da56dc3bf4315b28d49fc65a6e5d9d844fc9e202f55e3ebef2acb01f95c6917503b939219225e4ae81375be0a09afb136339830ec527ec89a7d37aa677"
}