8
votes
1answer
276 views

Categorical Semantics for Second-Order Logics

I am currently doing some work using a categorical semantics of first-order logic. The specific semantics I am using is due to Andrew Pitts, as described in: Categorical Logic, Andrew M. Pitts, ...
2
votes
2answers
359 views

What structure has been found for functions with this relationship.

Given $f$ and $g$ $\forall x y. f(x) = f(y) \Longrightarrow f(g(x)) = f(g(y))$ Or equivalently $ker\ f \subseteq ker\ (f \circ g)$. Note: if $f$ is injective then this holds for any $g$. ...
7
votes
6answers
1k views

Giving $Top(X,Y)$ an appropriate topology

I am not sure if its OK to ask this question here. Let $Top$ be the category of topological spaces. Let $X,Y$ be objects in $Top$. Let $F:\mathbb{I}\rightarrow Top(X,Y)$ be a function (I will ...
3
votes
2answers
224 views

What categories correspond to the typed lambda calculus with parametric types?

the unadorned typed lambda calculus correspond to the closed cartesian categories, but if we add in dependent or parametric types how are they then characterised?
2
votes
0answers
295 views

Groupoid interpretation of type theory

Hello, I read the paper on groupoid interpretation of type theory by Hofmann and Streicher and I have a question. According to the authors $Tm([[\text{Set}\:[\Gamma]\: ]])$ is the same as ...
24
votes
0answers
612 views

Computer calculations in A_infinity categories?

Is there a good computer program for doing calculations in A-infinity categories? Explicit calculations in A-infinity categories are an important, useful, yet very tedious task. One has to keep ...
4
votes
1answer
226 views

Inverse of Kleisli star, or “extension operator”

While thinking about monads in the theory of denotational semantics, I have made an observation about the Kleisli category that I would like to check Suppose $F : \mathcal D \to \mathcal C$, $G : ...
5
votes
0answers
325 views

Chain/Hierarchy of Monoids

Let's assume that we have the following collection of structures: Some space $P$. Monoids $(M_{i+1},\circ_{i+1})$, and Actions $\bullet_{i+1}:M_{i+1}\times M_i\to M_i$, for $i\ge 0$ And ...
11
votes
2answers
443 views

What do you use categorical glueing/sconing/Freyd covers for?

In the theory of programming languages and structural proof theory, one of the handiest techniques we have available is a method called "logical relations", in which you can prove properties of ...
7
votes
2answers
727 views

The difference between the Recursive and the Effective topos.

I would like to know which is the real difference between the Recursive topos (in the sense of Mulry) and the Effective topos (in the sense of Hyland). Especially what is related to recursive ...
37
votes
9answers
9k views

Relating Category Theory to Programming Language Theory

I'm wondering what the relation of category theory to programming language theory is. I've been reading some books on category theory and topos theory, but if someone happens to know what the ...
16
votes
11answers
5k views

Programming Languages based on Category Theory

Since some computer scientists use category theory, I was wondering if there are any programming languages that use it extensively.