#categorytheory — Public Fediverse posts

This is getting complicated! #haskell #categorytheory

Propositions As Types Analogy • 1
• https://inquiryintoinquiry.com/2013/01/29/propositions-as-types-analogy-1/

One of my favorite mathematical tricks — it almost seems too tricky to be true — is the Propositions As Types Analogy. And I see hints the 2‑part analogy can be extended to a 3‑part analogy, as follows.

Proof Hint ∶ Proof ∶ Proposition
∷
Untyped Term ∶ Typed Term ∶ Type

or

Proof Hint ∶ Untyped Term
∷
Proof ∶ Typed Term
∷
Proposition ∶ Type

See my working notes on the Propositions As Types Analogy —
• https://oeis.org/wiki/Propositions_As_Types_Analogy

#Mathematics #CategoryTheory #ProofTheory #TypeTheory
#Logic #Analogy #Isomorphism #PropositionalCalculus
#CombinatorCalculus #CombinatoryLogic #LambdaCalculus
#Peirce #LogicalGraphs #GraphTheory #RelationTheory

Survey of Precursors Of Category Theory • 6
• https://inquiryintoinquiry.com/2025/05/05/survey-of-precursors-of-category-theory-6/

A few years ago I began a sketch on the “Precursors of Category Theory”, tracing the continuities of the category concept from Aristotle, to Kant and Peirce, through Hilbert and Ackermann, to contemporary mathematical practice. A Survey of resources on the topic is given below, still very rough and incomplete, but perhaps a few will find it of use.

Background —

Precursors Of Category Theory
• https://oeis.org/wiki/Precursors_Of_Category_Theory

Propositions As Types Analogy
• https://oeis.org/wiki/Propositions_As_Types_Analogy

Blog Series —

Notes On Categories
• https://inquiryintoinquiry.com/2013/02/22/notes-on-categories-1/

Precursors Of Category Theory
1. https://inquiryintoinquiry.com/2024/05/25/precursors-of-category-theory-1-a/
2. https://inquiryintoinquiry.com/2024/05/26/precursors-of-category-theory-2-a/
3. https://inquiryintoinquiry.com/2024/05/27/precursors-of-category-theory-3-a/
4. https://inquiryintoinquiry.com/2024/05/28/precursors-of-category-theory-4-a/
5. https://inquiryintoinquiry.com/2024/05/29/precursors-of-category-theory-5-a/
6. https://inquiryintoinquiry.com/2024/05/30/precursors-of-category-theory-6-a/

Precursors Of Category Theory • Discussion
1. https://inquiryintoinquiry.com/2020/09/13/precursors-of-category-theory-discussion-1/
2. https://inquiryintoinquiry.com/2020/09/21/precursors-of-category-theory-discussion-2/
3. https://inquiryintoinquiry.com/2020/09/25/precursors-of-category-theory-discussion-3/

Categories à la Peirce —

C.S. Peirce • A Guess at the Riddle
• https://inquiryintoinquiry.com/2012/03/21/c-s-peirce-a-guess-at-the-riddle/

Peirce's Categories
1. https://inquiryintoinquiry.com/2015/10/30/peirces-categories-1/
2. https://inquiryintoinquiry.com/2015/10/31/peirces-categories-2/
3. https://inquiryintoinquiry.com/2015/11/04/peirces-categories-3/
•••
19. https://inquiryintoinquiry.com/2020/05/13/peirces-categories-19/
20. https://inquiryintoinquiry.com/2020/05/14/peirces-categories-20/
21. https://inquiryintoinquiry.com/2020/06/25/peirces-categories-21/

C.S. Peirce and Category Theory
1. https://inquiryintoinquiry.com/2021/06/23/c-s-peirce-and-category-theory-1/
2. https://inquiryintoinquiry.com/2021/06/24/c-s-peirce-and-category-theory-2/
3. https://inquiryintoinquiry.com/2021/06/27/c-s-peirce-and-category-theory-3/
4. https://inquiryintoinquiry.com/2021/06/28/c-s-peirce-and-category-theory-4/
5. https://inquiryintoinquiry.com/2021/06/29/c-s-peirce-and-category-theory-5/
6. https://inquiryintoinquiry.com/2021/06/30/c-s-peirce-and-category-theory-6/
7. https://inquiryintoinquiry.com/2021/07/01/c-s-peirce-and-category-theory-7/
8. https://inquiryintoinquiry.com/2021/07/02/c-s-peirce-and-category-theory-8/

#Aristotle #Peirce #Kant #Carnap #Hilbert #Ackermann #SaundersMacLane
#Abstraction #Analogy #CategoryTheory #FunctionalLogic #RelationTheory
#PrecursorsOfCategoryTheory #PropositionsAsTypes #Semiotics #TypeTheory

ChatGPT on categorical logic again.

🧱 Level 1: Morphisms = Proofs, Typed with Validity

You 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, Transformations

Now 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.

#categorytheory #logic #RelevanceLogic

ChatGPT 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.

#RelevanceLogic #categorytheory #enrichedcategory #rm3

#introduction

Part of the Migration. Moved from @[email protected]

Interested in #topology (for fun and #TDA )
#GraphicalLinearAlgebra and similar notations like string diagrams and #ExistentialGraphs
#CurryHowardIsomorphism
#Semantics for humans and computers
#topoi
#CategoryTheory
#WordEmbeddings (in #NLP )
#language
#logic
#SFF
#History of science, math, societies
etc.

Trans rights are human rights; blm; workers solidarity; native rights; and all the various other ways of not being vile to people