The latest cubical Agda repository has this definition:
record Iso {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ')
...
sec : section fun inv
ret : retract fun inv
but the paper I'm reading uses
leftInv
rightInv
instead. Chat GPT insists that the "modern" library uses the latter, but I can't seem to find it. I'm using
https://github.com/agda/cubical
Bartosz Milewski
npub15c…wczp5
2025-12-25 14:10:25 UTC
Author Public Key
npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5Published at
2025-12-25 14:10:25 UTCEvent JSON
{
"id": "11323489fb8d65eb556c7e0bf59939deee85a890520c4af25e1c255be86b3ebe",
"pubkey": "a60a88374d8e1cf092c7ea93662aa784fb33b3e75be7725017032e6929ebc5d5",
"created_at": 1766671825,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/users/BartoszMilewski/statuses/115780604735669596",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "The latest cubical Agda repository has this definition:\nrecord Iso {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') \n ... \n sec : section fun inv\n ret : retract fun inv\nbut the paper I'm reading uses \n leftInv\n rightInv \ninstead. Chat GPT insists that the \"modern\" library uses the latter, but I can't seem to find it. I'm using\nhttps://github.com/agda/cubical",
"sig": "06ade497026ba32586dfb98b79cb2a7e5ed93c00d32d9dd6fe8efeb5935f05772f112c7ab34802e9e2a7662d445e2529e5fd182ae7dac8b5719f8ee43e69a3d5"
}