{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreigwx36p3anj7mk4qhcfmor2hu2eueofhmw2zrfks6lglamsyinsmu",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mjqjnph6dpi2"
  },
  "path": "/t/lawvere-theories/13944#post_7",
  "publishedAt": "2026-04-18T02:46:34.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "No, especially because\n\n\n    type Stuck :: Peano\n    type family Stuck where\n\n\nThis is an irreducible type family, but it’s still technically valid. It also is not an instance of Prop.",
  "title": "Lawvere theories"
}