101010.pl

Counting Is HardAs promised. Here is the sequel to my Weihrauch reductions are Containers post, this time relating strong reductions to dependent adaptors. Enjoy!<a href="https://www.countingishard.org/blog/strong-reducibility-as-an-adaptor" rel="nofollow noopener" translate="no" target="_blank">https://www.countingishard.org/blog/strong-reducibility-as-an-adaptor</a><a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#categorytheory</a> <a href="https://mathstodon.xyz/tags/computability" class="mention hashtag" rel="nofollow noopener" target="_blank">#computability</a>

José A. AlonsoReadings shared May 23, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/23-readings_shared_05-23-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/05/23-readings_shared_05-23-25</a> <a href="https://mathstodon.xyz/tags/AIforCode" class="mention hashtag" rel="nofollow noopener" target="_blank">#AIforCode</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/RocqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#RocqProver</a>

José A. AlonsoSolving guarded domain equations in presheaves over ordinals and mechanizing it. ~ Sergei Stepanenko, Amin Timany. <a href="https://tildeweb.au.dk/au571806/publications/files/2025-fscd-guarded-dom.pdf" rel="nofollow noopener" translate="no" target="_blank">https://tildeweb.au.dk/au571806/publications/files/2025-fscd-guarded-dom.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/RocqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#RocqProver</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a>

Ramin Honary<a class="u-url mention" href="https://chaos.social/@das_g" rel="nofollow noopener" target="_blank">@das_g</a> True. It is certainly magical that there is a programming language which defines a state monad called “IO” (or sometimes “Effect”) which carries around with it a symbol of the entire Real World in order to model the idea that any evaluation of a function of that type of monad may (or may not) create a change somewhere out in the real world, as opposed to “pure” functions which can only ever manipulate the stack.<a class="hashtag" href="https://fe.disroot.org/tag/tech" rel="nofollow noopener" target="_blank">#tech</a> <a class="hashtag" href="https://fe.disroot.org/tag/software" rel="nofollow noopener" target="_blank">#software</a> <a class="hashtag" href="https://fe.disroot.org/tag/haskell" rel="nofollow noopener" target="_blank">#Haskell</a> <a class="hashtag" href="https://fe.disroot.org/tag/programminglanguage" rel="nofollow noopener" target="_blank">#ProgrammingLanguage</a> <a class="hashtag" href="https://fe.disroot.org/tag/typetheory" rel="nofollow noopener" target="_blank">#TypeTheory</a> <a class="hashtag" href="https://fe.disroot.org/tag/categorytheory" rel="nofollow noopener" target="_blank">#CategoryTheory</a>

José A. AlonsoReadings shared May 14, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/14-readings_shared_05-14-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/05/14-readings_shared_05-14-25</a> <a href="https://mathstodon.xyz/tags/Arend" class="mention hashtag" rel="nofollow noopener" target="_blank">#Arend</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/OCaml" class="mention hashtag" rel="nofollow noopener" target="_blank">#OCaml</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a>

José A. AlonsoFormal P-category theory and normalization by evaluation in Rocq. ~ David G. Berry, Marcelo P. Fiore. <a href="https://arxiv.org/abs/2505.07780" rel="nofollow noopener" translate="no" target="_blank">https://arxiv.org/abs/2505.07780</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a>

José A. AlonsoReadings shared May 9, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/09-readings_shared_05-09-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/05/09-readings_shared_05-09-25</a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ATP</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/Education" class="mention hashtag" rel="nofollow noopener" target="_blank">#Education</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a> <a href="https://mathstodon.xyz/tags/Teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#Teaching</a>

José A. AlonsoA graphical interface for category theory proofs in Coq. ~ Luc Chabassier. <a href="https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ThEdu24.2.pdf" rel="nofollow noopener" translate="no" target="_blank">https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ThEdu24.2.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a>

CubeRootOfTrue🧭 Contravariant Peter Principle (a.k.a. The Lizard Scenario)Now imagine instead that your competence remains fixed, but the job requirements mutate. That’s a contravariant scenario: Contravariant Responsibility Functor: Let’s say there's a functor $ G:R^{op}\rightarrow C$ This maps the changing role structure back into what competence would be needed to perform it.But if the functor is no longer representable, then the job has moved beyond what your (static) domain supports. You didn't move—the codomain did.In a sense, the organization pulls back a mutated version of the role, and you’re now the wrong preimage. That’s not your fault—but the target object has changed.<a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#categorytheory</a> <a href="https://mathstodon.xyz/tags/ethics" class="mention hashtag" rel="nofollow noopener" target="_blank">#ethics</a>

CubeRootOfTrue🧠 Categorical Peter PrincipleLet’s model the Peter Principle as a (somewhat playful) functor:Covariant Peter Functor: Let C be the category of competence levels. Let R be the category of responsibility levels. Then a functor F:C→R maps increasing competence to increasing responsibility.But (here’s the punchline): This functor preserves structure only up to the breaking point.At each step, you’re promoted to a position requiring slightly more competence than you currently have. The mapping continues until the functor fails to be faithful—you get promoted past the limits of your competence, and the correspondence breaks.(by now you know who wrote this)<a href="https://mathstodon.xyz/tags/peterprinciple" class="mention hashtag" rel="nofollow noopener" target="_blank">#peterprinciple</a> <a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#categorytheory</a>

CubeRootOfTrue🧩 Example: Law as a Natural TransformationImagine a 2-functor from: Category of individual acts and desires (personal logic, rights) To category of socially accepted actions (legal logic, responsibilities)Then a natural transformation encodes: How a society translates individual reasoning into enforceable action. How law binds or restricts certain inferences while preserving structure (naturality condition).That is, this commutes if η is natural — that is, doing something and then applying law is the same as applying law first and doing the translated thing.--- oops, ChatGPT doesn't know about asking for permission vs forgiveness; I mean, it *should* commute, except for that pesky time asymmetry where you can't take back what you did. --- more context is needed ---This models ethics, cultural norms, or constitutional constraints as natural transformations that preserve reasoning across systems.This is why we need Judges. It's not an easy job, respect them<a href="https://mathstodon.xyz/tags/rights" class="mention hashtag" rel="nofollow noopener" target="_blank">#rights</a> <a href="https://mathstodon.xyz/tags/responsibilities" class="mention hashtag" rel="nofollow noopener" target="_blank">#responsibilities</a> <a href="https://mathstodon.xyz/tags/legal" class="mention hashtag" rel="nofollow noopener" target="_blank">#legal</a> <a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#categorytheory</a>

CubeRootOfTrue<a href="https://mathstodon.xyz/@skewray" class="u-url mention" rel="nofollow noopener" target="_blank">@skewray</a> I will also add, this is all axiom based. You can derive 3 and 4 valued logic from the Peano axioms and Category Theory, no more than that is necessary.<a href="https://mathstodon.xyz/tags/peano" class="mention hashtag" rel="nofollow noopener" target="_blank">#peano</a> <a href="https://mathstodon.xyz/tags/caturday" class="mention hashtag" rel="nofollow noopener" target="_blank">#caturday</a> <a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#categorytheory</a> <a href="https://mathstodon.xyz/tags/twist" class="mention hashtag" rel="nofollow noopener" target="_blank">#twist</a>

CubeRootOfTrueChatGPT on categorical logic again.🧱 Level 1: Morphisms = Proofs, Typed with ValidityYou can think of these arrows as typed by a truth value — i.e., each morphism has a color: valid, invalid, plausible, context-sensitive, contradictory-but-derivable, etc.In this sense, truth is not binary, but becomes a fiber over each morphism: a coloring or modality.So your category becomes a fibration over a poset of truth values, or a category enriched in truth values — maybe in a Heyting algebra or relevance lattice.🧱 Level 2: 2-Cells = Laws, Derivations, TransformationsNow we raise it to a 2-category: 0-cells: Propositions (types) 1-cells: Deductions / proof structures f:A→B 2-cells: Proofs of equivalence between proofs (e.g., natural transformations, rewrite rules, context substitution, modality shifts)This is where natural transformations live: between two different "routes" from A to B. They express meta-logical structure: laws, policies, meanings.Let’s say you have: One arrow f:A→B defined in deontic logic (permission-based) Another arrow g:A→B in alethic logic (necessity-based)A natural transformation η:f⇒g might be a social contract or legal interpretation that maps from a space of permitted inferences to necessary ones — or vice versa.<a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#categorytheory</a> <a href="https://mathstodon.xyz/tags/logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#logic</a> <a href="https://mathstodon.xyz/tags/RelevanceLogic" class="mention hashtag" rel="nofollow noopener" target="_blank">#RelevanceLogic</a>

CubeRootOfTrue🔹 “Natural” Rights and NaturalityThe Founders talked about “natural rights” in the Lockean sense (self-evident, god-given, not granted by governments), but modern naturality—in the categorical sense—is about structure-preserving transformations, functors and natural transformations that respect the relationships between objects.So here's the kicker: The “natural” rights the Founders described were not truly natural transformations — They didn’t define the morphisms between citizens, societies, and responsibilities.They intuited that something was preserved under moral "structure", but without the machinery to make this precise.💡 Maybe what the Constitution lacks is a natural transformation from Rights to Responsibilities.I couldn't have put it better myself, which is why I posted ChatGPT's version. I know it still sounds a little like nonsense, butRights and Responsibilities are really two sides of the same coin, you can't have one without the other (you can drive a car, buy a gun, etc., but you have to learn how to use it first, and get a license, etc.)<a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#categorytheory</a> <a href="https://mathstodon.xyz/tags/rights" class="mention hashtag" rel="nofollow noopener" target="_blank">#rights</a> <a href="https://mathstodon.xyz/tags/deontic_logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#deontic_logic</a>

José A. AlonsoReadings shared April 27, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/27-readings_shared_04-27-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/04/27-readings_shared_04-27-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#CommonLisp</a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="nofollow noopener" target="_blank">#Emacs</a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#LogicProgramming</a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener" target="_blank">#Prolog</a>

José A. AlonsoIntroducing category theory (Version 26 Apr 2025). ~ Peter Smith. <a href="https://www.logicmatters.net/resources/pdfs/SmithCat.pdf" rel="nofollow noopener" translate="no" target="_blank">https://www.logicmatters.net/resources/pdfs/SmithCat.pdf</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a>

CubeRootOfTrueChatGPT has a new sister called Monday. I will let you find out about that. Meanwhile here is what ChatGPT says about using enriched categories to model relevance logic:An Example Sketch Let V=Pos be a poset-enriched monoidal category where each hom-object is a set of “proofs” or “derivations,” ordered by resource usage. Then C(A,B) is itself an object in Pos, i.e., a poset of ways to prove B from A. The product ⊗ inside C does not come with free projections, so there is no arrow from (A⊗B) to B in general. If someone claims “Surely, we can discard A and prove B anyway,” the poset of proofs for C(A⊗B,B) is _empty_, or has no minimal element if your ordering demands using all resources.Thus, the absence of a projection morphism is encoded in the structure of the hom-object: it simply does not contain a suitable proof.-- here 'resource usage' is 'relevant stuff'You can write (A⊗B) -> B, in a diagram. But that arrow is "False", so it doesn't really "exist". Enriched categories capture this concept.<a href="https://mathstodon.xyz/tags/RelevanceLogic" class="mention hashtag" rel="nofollow noopener" target="_blank">#RelevanceLogic</a> <a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#categorytheory</a> <a href="https://mathstodon.xyz/tags/enrichedcategory" class="mention hashtag" rel="nofollow noopener" target="_blank">#enrichedcategory</a> <a href="https://mathstodon.xyz/tags/rm3" class="mention hashtag" rel="nofollow noopener" target="_blank">#rm3</a>

Jencel PanicA <a href="https://mathstodon.xyz/tags/monad" class="mention hashtag" rel="nofollow noopener" target="_blank">#monad</a> is when you know how to convert $M (M a)$ to $M a$, but not $M a$ to $a$.<a href="https://mathstodon.xyz/tags/haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#haskell</a> <a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#categorytheory</a> <a href="https://mathstodon.xyz/tags/functionalprogramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#functionalprogramming</a>

José A. AlonsoReadings shared April 3, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/03-readings_shared_04-03-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/04/03-readings_shared_04-03-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="nofollow noopener" target="_blank">#AlphaProof</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoCategory theory using Haskell (An introduction with Moggi and Yoneda). ~ Shuichi Yukita. <a href="https://books.google.com/books?id=4Xc2EQAAQBAJ" rel="nofollow noopener" translate="no" target="_blank">https://books.google.com/books?id=4Xc2EQAAQBAJ</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a>

Recent searches

Search options

Administered by:

Server stats:

#categorytheory