# Questions tagged [categorical-logic]

Categorical logic is a study of semantics constructed by categories.

55 questions
Filter by
Sorted by
Tagged with
35 views

### Is there a decent notion of "double Lawvere theory?"

I've been playing with the idea of a "double Lawvere theory" for mechanizing first order logical theories. I've been able to find only a tiny amount of detail online though and want feedback ...
121 views

### Linear logic and linearly distributive categories

1. Context On page two of the introduction to their paper Weakly distributive categories on linearly distributive categories Cockett and Seely write: It turns out that these weak distributivity maps, ...
148 views

143 views

### Strong induction for natural number object

From Lawvere's paper about ETCS we know that we can do induction for natural number object. My aim is to prove the strong induction principle for an NNO in a topos by translating this argument https://...
1 vote
67 views

### Proving the following is a equalizer by proving factorization for $1$ implies factorization for every object

I am reading the following document about Lawvere's ETCS: http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf My question is about Theorem 6 in this document. The aim is to prove an equivalence ...
1 vote
93 views

### Existence of subobject classifier in Lawvere's ETCS

I am reading this document: http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf Compared with the ordinary definition of a topos, the axioms of ETCS do not assume the existence of a subobject ...
1 vote
218 views

### Why is intuitionistic type theory without dependent types more powerful than Martin-Löf type theory?

In the preface of Introduction to higher order categorical logic, Lambek and Scott write (emphasis mine): [L]ogicians have made three attempts to formulate higher order logic, in increasing power: ...
64 views

1 vote
25 views

### Basic Constructive Modal Logic and Monoidal Endofunctors

I'm reading this paper by Kakutani : http://nicosia.is.s.u-tokyo.ac.jp/~kakutani/files/aplas07.pdf but I can't see how to use naturality of $m$ (given by the monoidal endofunctor modelling $\Box$) ...
149 views

### If a Grothendieck topos has a geometric morphism to $Sets$, then it is unique

In Caramello, Theories, Sites, Toposes, I read that Every Grothendieck topos $\mathcal E$ admits a unique (up to isomorphism) geoemtric morphism $\gamma_{\mathcal E}:\mathcal E\to \bf Set$. The ...
281 views

### Universal quantifiers in category theory

I’ve recently learned about the curry howard isomorphism for dependent type theory, and I’m now interested in learning about how to capture this in category theory. I believe that I understand how to ...
122 views

### Introduction to categorical logic and CHL-correspondence?

My motivation for this question is that I’m interested in using categorical logic/category theory to intuitively visualize and think about proofs in advanced type-theory based proof-assistants like ...
247 views

40 views

### Is "points lift along surjections" equivalent to choice in the internal logic?

I'm wondering about the following proposition in the internal logic of a topos: Given an epimorphism $e : E \to B$, then for every points $p : 1 \to B$, there is a point $\tilde{p} : 1 \to E$ for ...
This is a very basic question: given a theory $\mathbb{T}$, I have seen definitions of models of $\mathbb{T}$ as functions from signature $\Sigma$ to a fixed background category such that it satisfies ...
Most presentations of (dependent) constructive type theory present introduction and elimination rules for $0,1,+,\times$, which via Curry-Howard-Lambek corresponds to the initial object, terminal ...