{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreibz24ituwouel4ovuwymkdin4wana5e67ovnlscgsrswnd6lo3w5a",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mjq4a3hcwp72"
  },
  "path": "/t/lawvere-theories/13944#post_4",
  "publishedAt": "2026-04-17T22:14:15.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "n-Category Cafe",
    "congruence relations"
  ],
  "textContent": "L0neGamer:\n\n> With the above, it is described as a functor; could we make it into a proper haskell function by just swapping `n` and `a`?\n\nNotice that `F a` has kind `Arity -> Type` so it definitely can not be a `Functor` in the strict Haskell Prelude sense. When swapping the arguments, it is nothing but a vector functor of statically known dimension, e.g.\n\n\n    newtype V2 a = V2 (F a Two)\n\n\nFor the functoriality of `F a`, I did write that objects of `Arity` are to be thought of as natural numbers, but did not say what the morphisms are. The n-Category Cafe describes it as “the opposite of a skeleton of the category of finite sets”. Hence my use of `Pair` for what at first glance appears to be a coproduct. (2 is not equal to 1 * 1 but to 1 + 1)\n\nL0neGamer:\n\n> Or is this construction not powerful enough for that kind of “proof”, and it’s merely just setting up for quickchecking\n\nI did not intend this to be accessible to proof-checking, just wanted to convey the original idea of Lawvere theory as direct as possible. In any case, what would a “proof” of the laws be? It would, for any particular model of the theory, require knowledge of the particular implementation of `model`, which would have to be encoded somehow in a form so that a proof checker can analyze it.\n\nThere is another technique for algebraic categories, called “generators and relations”. It says that every object of the category is a quotient of a free object over some generators, by relations that honour the algebraic structure, so-called congruence relations. I can imagine that is is easy to prove that a free construction is lawful, thereby shifting the proof burden towards proving that the relations form a congruence. Sadly, relations are hard to work with in computing, due to the existential quantification in the relational composition.",
  "title": "Lawvere theories"
}