[johncolanduoni]

> Proofs = Types = Categories; all related, all translatable in terms of one another, yet all different.

Proofs = Some Types and Type Theories = Some Categories, so I think even taken as an attempt to paint the situation in broad strokes what you wrote is at best misleading. Many (commonly studied) categories and classes thereof are not interpretable as type theories, and type theories contain plenty of terms that would not be typically interpreted as proofs.

Also, even in category theory, papers and books take quite a bit of care to be clear when they introduce a new term. Urbit's documentation looks like it took every conceivable opportunity to invent new words for things where we already have words. The complaint is not about made-up words per se, but scores of unnecessary made-up words. It's like they expect to trademark the name of every little internal concept inside Urbit.

[bordercases]

Although that's a benefit I didn't think of, my charitable interpretation is that it allows for the use of terms that plug in to a social setting. Of course this all derives from Moldbug's political philosophy. It's technology that's engineered for a certain set of behaviors based on his framework.

The terms put the technology in the context of the philosophy, giving hints as to how it solves the problems within it. I can see why that would turn some people off, but for its purpose I believe it's effective. It grounds previously ephermal concepts in metaphors that are tight, like land = server + addressing space or code = law. A lack of good metaphors (rather than an abundance of poor ones, as is the state of things) may be a part of the reason we've become so disoriented with how we handle privacy. When you think of privacy issues as, "my identifying documents are on someone else's land", suddenly it becomes more clear as to what the problem is. By contrast "The Cloud" is a shit metaphor: the cloud is just someone else's computer. It isn't public, universal, or neutral, like real clouds are. And where in the cloud is there a network?

If one were to derive Unix in terms of, say, the operations of an anarchist society, as opposed to problems that are mostly mundane or technical, I would be saying the same thing. Arguably the last time this happened was during the Mother of All Demos with Doug Engelbart's models of the knowledge economy. Since then we've either been footnotes to Xerox PARC's visions, or have been otherwise haphazard.

As for the Proof/Type/Category equivalences, you're right, they're only equivalent for some structures in all three theories. So they're only equivalent up to locally closed cartesian categories, or wherever. But moving between those three perspectives even under this constraint still leaves you with distinctions, like syntax vs semantics. So in that sense they maintain the notion that different views lead to different nuances even if they cluster around the same space.