# 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)

114 questions
Filter by
Sorted by
Tagged with
24 views

• 194
97 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
27 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
643 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 ...
• 327
322 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 ...
• 201
524 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 ...
• 352
228 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
42 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
55 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?
• 593
118 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 ...
• 121
203 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 ...
• 276
1 vote
32 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 ...
• 155
532 views

### Functor laws and natural transformations in Haskell

As I've been struggling to get a deeper understanding of monads in Haskell, I started reading about functors and their counterparts in category theory. Keep in mind that I have no background in the ...
• 141
1 vote
58 views

### Can the most general unifier be defined categorically?

I remember from my reading of Category Theory for Computing Science that classical concepts like weakest preconditions can be seen as the categorical notion of pullback. I was wondering if the same ...
• 2,230
117 views

### Applying FP/Categorical terminology to non-FP languages

In my continuing effort to finally wrap my brain around advanced FP/categorical concepts, I've been reading dozens of articles and tutorials; what I have concluded is that: 1) Category Theory and ...
• 141
146 views

### Why does the category of language types have morphisms, not functors?

I am probably not phrasing this question well, so please bear with me as I try to explain what I mean. I am working on learning category theory, as applied to programming. So far, I understand that: ...
• 141
87 views

### Proof of the limit-colimit coincidince

Note: I figured this out, but haven't had the time to write an answer for it: see the comment. For reference: the discussed material appears in http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro....
1 vote
87 views

### Datatypes as initial algebras

I'm refining my understanding of the connection between initial algebras and datatypes. This paper suggests that one could even represent the categories corresponding to datatypes definitions: as ...
• 2,230
48 views

### Understanding Isabelle's implementation of coinduction

I'm studying how coinduction was encoded in Isabelle. At page 7 of the attached document, the author describes how some datatypes can be encoded as initial algebras. Here is one example: Finite lists ...
• 2,230
58 views

### How is substitution in type theory the composition of classifying morphisms in category theory?

In the article at nlab about relation between category theory and type theory, it is said that substitution in type theory is the same as composition of classifying morphisms in category theory. ...
• 593
1 vote
32 views

### Is, beta reduction in type theory being considered as counit for hom-tensor adjunction in category theory, a denotational or operational semantic?

In the article at nlab about the relation between type theory and category theory, it is said that "beta reduction" in type theory corresponds to "counit for hom-tensor adjunction" in category theory ...
• 593
56 views

### $\beta$ reduction equational equality

In Categories, Types and Structures, authors talk about exponential objects in section 2.3.1. Let $C$ be a Cartesian category, and $a,b \in Ob_C$. The exponent of $a$ and $b$ is an object $b^a$ ...
• 593
1 vote
57 views

### A notion dual to a product type having a given type

Consider this class: class Has record part where extract :: record -> part update :: (part -> part) -> record -> record It captures the notion of ...
• 165
78 views

### What is the adjunct of the evaluation morphism in a closed monodical category?

According to the nlab article about evaluation map if $X, Y \in C$, a closed monodical category then the adjunct to evaluation morphism $[X, Y]\otimes X \rightarrow Y$ is the identity morphism \$[X, Y] ...
• 593
71 views

### Mapping a free variable of type A to a cartesian closed category

In From Lambda Calculus to Cartesian Closed Categories, the author explains the interpretation of lambda calculus in cartesian closed category and at one point he explains how a term representing a ...
• 593
1 vote