101010.pl is one of the many independent Mastodon servers you can use to participate in the fediverse.
101010.pl czyli najstarszy polski serwer Mastodon. Posiadamy wpisy do 2048 znaków.

Server stats:

488
active users

#categorytheory

0 posts0 participants0 posts today
José A. Alonso<p>Readings shared July 12, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/13-readings_shared_07-12-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/07/13-readings_shared_07-12-25</span></a> <a href="https://mathstodon.xyz/tags/ASP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ASP</span></a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ATP</span></a> <a href="https://mathstodon.xyz/tags/CLP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CLP</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CoqProver</span></a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Emacs</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LogicProgramming</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Prolog</span></a> <a href="https://mathstodon.xyz/tags/ProofTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ProofTheory</span></a> <a href="https://mathstodon.xyz/tags/Prover9" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Prover9</span></a></p>
José A. Alonso<p>Categorical semantics in Haskell. ~ Mohamed Amine Ayari. <a href="https://kondylidou.github.io/assets/pdf/BA-mohamed.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">kondylidou.github.io/assets/pd</span><span class="invisible">f/BA-mohamed.pdf</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a></p>
Teixi<p><span class="h-card" translate="no"><a href="https://mathstodon.xyz/@FrohlichMarcel" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>FrohlichMarcel</span></a></span> </p><p>Oh là là just dropped:<br>2.5 hour "Introduction To Category Theory"<br>by Richard Southwell<br><a href="https://youtu.be/H32kyA4BMz4" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/H32kyA4BMz4</span><span class="invisible"></span></a></p><p><a href="https://mastodon.social/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>categorytheory</span></a> <a href="https://mastodon.social/tags/haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>haskell</span></a> <a href="https://mastodon.social/tags/ZuriHac" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ZuriHac</span></a> <a href="https://mastodon.social/tags/ZuriHac2025" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ZuriHac2025</span></a> <a href="https://mastodon.social/tags/functionalprogramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>functionalprogramming</span></a></p><p>HT <span class="h-card" translate="no"><a href="https://fosstodon.org/@zurihac" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>zurihac</span></a></span></p>
José A. Alonso<p>Readings shared July 4, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/05-readings_shared_07-04-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/07/05-readings_shared_07-04-25</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Rust" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rust</span></a> <a href="https://mathstodon.xyz/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TypeTheory</span></a></p>
José A. Alonso<p>Category theory: Introducing the perfect language. ~ Richard Southwell <a href="https://youtu.be/H32kyA4BMz4" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/H32kyA4BMz4</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a></p>
Leon P Smith<p>Slice categories and continuations are very similar concepts, with a lot of overlap between the two. Yet I'm somewhat confident that there are differences as well. Anybody have insight?</p><p><a href="https://ioc.exchange/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a> <a href="https://ioc.exchange/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://ioc.exchange/tags/plt" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>plt</span></a></p>
Programming Languages Delft<p>"2-Functoriality of Initial Semantics, and Applications" by Benedikt Ahrens, Ambroise Lafont, and Thomas Lamiaux was accepted at <a href="https://akademienl.social/tags/icfp" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>icfp</span></a> </p><p>"We provide tools to compare and relate the models obtained from a signature for different choices of monoidal category [..] we use our results to relate the models of the different implementation [..] and to provide a generalized recursion principle for simply-typed syntax."</p><p>Read it on <a href="https://akademienl.social/tags/arXiv" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>arXiv</span></a>: <a href="https://arxiv.org/abs/2503.10863" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2503.10863</span><span class="invisible"></span></a></p><p><a href="https://akademienl.social/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TypeTheory</span></a> <a href="https://akademienl.social/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a></p>
José A. Alonso<p>Readings shared June 27, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/28-readings_shared_06-27-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/06/28-readings_shared_06-27-25</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/AI4Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AI4Math</span></a> <a href="https://mathstodon.xyz/tags/Autoformalization" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Autoformalization</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CompSci</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Mizar</span></a></p>
José A. Alonso<p>Readings shared June 9, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/09-readings_shared_06-09-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/06/09-readings_shared_06-09-25</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LogicProgramming</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Prolog</span></a> <a href="https://mathstodon.xyz/tags/Rust" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rust</span></a></p>
José A. Alonso<p>Formalizing invisible mathematics: case studies from higher category theory. ~ Emily Riehl. <a href="https://emilyriehl.github.io/files/invisible.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">emilyriehl.github.io/files/inv</span><span class="invisible">isible.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a></p>
Marcel Fröhlich<p>Hey mathstodon ...</p><p>Thinking about architecture and design of commercial data environments and software applications in more formal ways than the average set thinking dominating IT.</p><p>What is your experience with using category theory outside of a research scope?</p><p><a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>categorytheory</span></a></p>
Counting Is Hard<p>As promised. Here is the sequel to my Weihrauch reductions are Containers post, this time relating strong reductions to dependent adaptors. Enjoy!</p><p><a href="https://www.countingishard.org/blog/strong-reducibility-as-an-adaptor" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">countingishard.org/blog/strong</span><span class="invisible">-reducibility-as-an-adaptor</span></a></p><p><a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>categorytheory</span></a> <a href="https://mathstodon.xyz/tags/computability" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>computability</span></a></p>
José A. Alonso<p>Readings 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"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/05/23-readings_shared_05-23-25</span></a> <a href="https://mathstodon.xyz/tags/AIforCode" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforCode</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/RocqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>RocqProver</span></a></p>
José A. Alonso<p>Solving 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"><span class="invisible">https://</span><span class="ellipsis">tildeweb.au.dk/au571806/public</span><span class="invisible">ations/files/2025-fscd-guarded-dom.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/RocqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>RocqProver</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a></p>
Ramin Honary<p><span class="h-card"><a class="u-url mention" href="https://chaos.social/@das_g" rel="nofollow noopener" target="_blank">@<span>das_g</span></a></span> 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 <strong>entire Real World</strong> 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.</p><p><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></p>
José A. Alonso<p>Readings 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"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/05/14-readings_shared_05-14-25</span></a> <a href="https://mathstodon.xyz/tags/Arend" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Arend</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/OCaml" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>OCaml</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a></p>
José A. Alonso<p>Formal 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"><span class="invisible">https://</span><span class="">arxiv.org/abs/2505.07780</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a></p>
José A. Alonso<p>Readings 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"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/05/09-readings_shared_05-09-25</span></a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ATP</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Education" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Education</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/Teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Teaching</span></a></p>
José A. Alonso<p>A 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"><span class="invisible">https://</span><span class="ellipsis">cgi.cse.unsw.edu.au/~eptcs/pap</span><span class="invisible">er.cgi?ThEdu24.2.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a></p>
CubeRootOfTrue<p>🧭 Contravariant Peter Principle (a.k.a. The Lizard Scenario)</p><p>Now imagine instead that your competence remains fixed, but the job requirements mutate. That’s a contravariant scenario:<br>Contravariant Responsibility Functor:</p><p> Let’s say there's a functor \( G:R^{op}\rightarrow C\)</p><p> This maps the changing role structure back into what competence would be needed to perform it.</p><p>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.</p><p>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.</p><p><a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>categorytheory</span></a> <a href="https://mathstodon.xyz/tags/ethics" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ethics</span></a></p>