nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) Consider the following geometric theory (if you will permit a made-up LF-style syntax for geometric theories which makes it slightly more convenient to talk about axiom schemas which involve base types)
X : Set
R : X -> X -> Nat -> Prop
_ : (x x' : X) -> ∃(n : Nat). (R x x' n)
_ : (n n' : Nat) -> (x x' : X) -> (n != n') -> (R x x' n) -> (R x x' n') -> ⊥
This is the theory of a binary function to the naturals.
Now, consider two models M1 and M2 and assume that M is the coproduct, with i1 : M1 -> M, i2 : M2 -> M the injections. Then (M.R (i1 x1) (i2 x2) n) must be true for precisely one n, for every (x2 : M1.X), (x2 : M2.X). However, for any n, there is a models N with injections j1 : M1 -> N, j2 : M2 -> N where (N.R (j1 x1) (j2 x2) n) is true, and thus there cannot exist a morphism M -> N. QED
Owen Lynch
npub1cj…fxs07
2025-11-25 14:19:00 UTC
in reply to nevent1q…f6ys
Author Public Key
npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07Seen on
wss://relay.ditto.pubPublished at
2025-11-25 14:19:00 UTCEvent JSON
{
"id": "8b18d8ef5627239cb13b220c9d7adfa5737da629132433292e49859ca1307655",
"pubkey": "c4884ff89ad14becbadc2a822632f6267158dbd86e6b51dd1d219ae77f51e99a",
"created_at": 1764080340,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.ditto.pub/"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.ditto.pub/"
],
[
"e",
"1f4dbb7e1d9d611a9047c3ac0f7546db18c1b428a4122d0a6473c38fbb531fc0",
"wss://relay.ditto.pub/",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/olynch/statuses/115610769218455087",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe Consider the following geometric theory (if you will permit a made-up LF-style syntax for geometric theories which makes it slightly more convenient to talk about axiom schemas which involve base types)\n\nX : Set\nR : X -\u003e X -\u003e Nat -\u003e Prop\n_ : (x x' : X) -\u003e ∃(n : Nat). (R x x' n)\n_ : (n n' : Nat) -\u003e (x x' : X) -\u003e (n != n') -\u003e (R x x' n) -\u003e (R x x' n') -\u003e ⊥\n\nThis is the theory of a binary function to the naturals.\n\nNow, consider two models M1 and M2 and assume that M is the coproduct, with i1 : M1 -\u003e M, i2 : M2 -\u003e M the injections. Then (M.R (i1 x1) (i2 x2) n) must be true for precisely one n, for every (x2 : M1.X), (x2 : M2.X). However, for any n, there is a models N with injections j1 : M1 -\u003e N, j2 : M2 -\u003e N where (N.R (j1 x1) (j2 x2) n) is true, and thus there cannot exist a morphism M -\u003e N. QED",
"sig": "0f4873cee147f3d00dcea23d0cadb7575dc8b41bab82bd6e99f565c721c2d36fe9fbad634c267f5c45417de7ac4df8de4742b23981e66c6efc3d01756b00229d"
}