# Questions tagged [category-theory]

Category theory is used to formalize mathematics and its concepts as a collection of objects and arrows (also called morphisms). Category theory can be used to formalize concepts of other high-level abstractions such as set theory, ring theory, and group theory. (By Steve Awodey)

127 questions
Filter by
Sorted by
Tagged with
46 views

### Is there a category theory equivalent of pure type systems?

I have seen the correspondence between the simply-typed lambda calculus and Cartesian closed categories, and am curious about how this generalizes to other lambda calculi. I have seen some related ...
• 101
19 views

### A specification of all possible languages for representing graphs?

There are a few commonly used markup languages for specifying graph structures. I am interested in discovering alternative graph notations that may be counterintuitive yet more compact or useful in ...
52 views

### "union" or "disjunction" in pure untyped lambda calculus

In the untyped lambda calculus (with variables, abstraction and application as the only constructors), we have a "pair" construct, given by $(a, b) = \lambda x, x a b$. The projections are ...
1 vote
40 views

### The isomorphism in "Scott's representation theorem"

In the essay Relating Theories of the lambda-calculus, Scott constructs (from page 418) a category that exhibits a chosen lambda calculus $L$ with $\beta$-equality as the collection(s) of ...
69 views

Haskell's monads are usually considered to mean strong monads in category theory, but it seems like the former is a bit stronger than the latter. With strong monads, you have a Kleisli extension ...
• 123
25 views

• 194
98 views

### (Co)-monads and terminating implementations

The bounty above should read 'I would like to know whether the example I discuss is a com-monad and why (why not).' Suppose we set $\mathbb{M} \alpha := r \to \alpha$, where $r$ is some fixed type, ...
• 194
1 vote
28 views

### Constructing a monad via type synonyms of a particular kind

We can define a reader/environment monad on the simply-typed lambda calculus, using the following three equations, where $r$ is some fixed type, $\alpha$ is any type (I subscript some terms with their ...
• 194
2k views

### A monad is just a monoid in the category of endofunctors, what's the enlightenment?

Pardon the word play. I'm a little confused about the implication of the claim and hence the question. Background: I ventured into Category Theory to understand the theoretical underpinnings of ...
• 347
776 views

### Functional Programming and Category Theory

I'm a math Ph.D. having done research in Algebraic Geometry and Algebraic Topology in grad school for my thesis and I've studied a fair amount of category theory in the process (e.g. having worked ...
• 221
525 views

### Given A to C, and B to C with known complexities, what can be said about A to B?

Say I have two sets of values $A$ and $B$ and for each set I have a computable function from that set to a third set $C$. Now suppose that I want to construct a function from $A$ to $B$, such that if ...
• 364
407 views

### Describing the Bool-And monoid in terms of categories

Normally I put the question before the context, but in this case I want to admit the possibility that the context and my understanding nullify the question. Plus it helps me think through my question. ...
1 vote
46 views

### Is the identity functor a kind of free object?

My understanding of free objects is: Free functors, free applicatives, free monads, free monoids, &c, give you more structure "for free", i.e. in general, or for all some thing with less structure,...
• 253
98 views

### Is there any correspondence between SUM type in type theory and arithmetical summation?

Is there any correspondence between the coproduct(sum) type in type theory and arithmetical summation? For example what does 3+4 or x+6 mean in type theory?
• 621
169 views

### Is this possible: In OOP, private methods in a class form a F-coalgebra and public methods in a class form an F-algebra?

I recently found out that OOP classes turn out to be F-coalgebras: https://www.semanticscholar.org/paper/Objects-and-Classes%2C-Co-Algebraically-Jacobs/c7c45abf7d99e0aef627fd5223023bf82e70dc71 The ...
• 131
400 views

### Why are all polymorphic functions between functors natural transformations?

Bartosz Milewski's Category Theory for Programmers says the following: A parametrically polymorphic function between two functors (including the edge case of the Const functor) is always a natural ...
• 348
1 vote
33 views

### What is the maths name for a set which contains the Domain and Codomain of a function? [closed]

Im interested in this so that I can name a type parameter in a program I'm writing. There is function that that has three parameters. D, Domain C, Codomain X, where D is a subset of X and C is a ...
• 173