# Tagged Questions

162 views

### internal language for the 2-category of small categories

What is the internal language of the category Cat of small categories? I found an article by Glynn Winskel and his student Mario Jose CĂˇccamo about such calculus! However it is limited to a fragment ...
301 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, ...
418 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$. ...
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 ...
246 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?
313 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 ...
640 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 ...
235 views

456 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 ...
788 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 ...