Questions tagged [categorical-logic]
Categorical logic is a study of semantics constructed by categories.
96 questions
4
votes
1
answer
174
views
The necessity of introducing CwF for the categorical semantics of Martin-Löf theories?
This question involves two simple subquestions regarding the intuition of necessity of introducing CwF (Category with families) as categorical semantics of Martin-Löf theories. (Note that I'm not ...
- 706
0
votes
1
answer
201
views
Is there induction in (the internal logic of) an arbitrary elementary topos $\mathcal{E}$?
The Question:
Is there induction${}^\dagger$ in (the internal logic of) an arbitrary elementary topos $\mathcal{E}$?
$\dagger$: By which I mean: "Is there an induction principle . . .". ...
- 48.5k
3
votes
1
answer
115
views
Prove $A \otimes 1 \cong A$ in a type theory for SMC.
I was reading Categorical logic from a categorical point of view by Michael Shulman.
While I appreciated the insight into how type theory can make certain proofs in category theory simpler, I struggle ...
- 65
1
vote
0
answers
131
views
Motivation to study Eilenberg-Moore category
A pair of adjoint functors $F:\mathscr{C\leftrightarrows D:}G$ is said to be monadic if the comparision functor $K:\mathscr D\to \mathscr C^T$ is an equivalence, where $T=GF$ and $\mathscr C^T$ the ...
- 706
0
votes
0
answers
103
views
The Free Algebra Construction on a Lawvere Theory and Failure to Recover Classical Free Algebra
Given a Lawvere theory $A$ and a functor $P: A \to \mathsf{Set}$, we have a free algebra on $P$ ensured by the adjoint functor theorem and I attempted to construct it as a quotient of the free algebra ...
- 505
1
vote
0
answers
73
views
Equivalence among $\tau$-theory, elementary topos and Mitchell-Bénabou language [closed]
In Johnstone's book "Sketches of an Elephant: A topos theory compendium, volume 2" (referred as Elephant), he defined a higher-order typed (intuitionistic) signature (simplified as $\tau$-...
- 61
5
votes
1
answer
97
views
Clarification of the General Definition of Categorical Semantics
I'm interested in the general definition for a categorical interpretation of a type theory. I currently understand the following:
For each context $\Gamma$ of the theory, we provide an interpretation ...
- 135
1
vote
0
answers
82
views
Split fibrations and indexed categories
In the book Categories for Types by Crole, in the second chapter, there's a guided exercise to prove that the category of split fibrations $\mathcal{SFib}$ and that of (strict) indexed categories $\...
- 1,768
1
vote
0
answers
73
views
Does colimits preserve quasi compactness in a Grothendieck topos?
In one of Luries papers on the conceptual completeness theorm proof
at the proof of the theorem itself(2.3), He uses the fact that the elements in a topos Shv(C) (Over a pretopos C, which in this ...
- 11
1
vote
1
answer
100
views
Example of first order Hyperdoctrine without Beck-Chevalley
Let $C$ be a (monoidal) cartesian category, $HA$ the category of Heyting algebras and $P : C \to HA$ a functor with left and right adjoints $∃_π$ and $∀_π$ to $P(\pi)$ for every projection $\pi$ in $C$...
- 1,768
3
votes
1
answer
168
views
Validity of ZFC Axioms in a General Topos
Apologies for the clueless question. I'm new to categorical logic and have no background in model theory, and I'm struggling to pin down the exact way in which the internal language of a topos allows ...
- 135
-3
votes
1
answer
130
views
Clarifying a question: If $f:a\to b$ is any arrow, show that $\operatorname{true}_b\circ f=\operatorname{true}_a.$
This is about Exercise 4.2.3 of Goldblatt's, "Topoi".
NOT The Question:
Paraphrasing the exercise:
If $f:a\to b$ is any arrow, show that $\operatorname{true}_b\circ f=\operatorname{true}_a.$...
- 48.5k
1
vote
1
answer
77
views
Equivalence between equality as a left adjoint and as a right adjoint
Given a hyperdoctrine $P : C^{op} → HA$ it is common to define equality as a left adjoint to contraction
$$ \dfrac{weak(φ) ∧ =_σ ⊢ ψ : P\ (σ × σ)}{φ ⊢ contr(ψ) : P\ σ} $$
Here $$weak := P\ π : P\ \...
- 1,768
2
votes
1
answer
138
views
Explicit definition of cartesian multicategories
In the definition of cartesian multicategories of the nlab it says "symmetric multicategory [equiped with contraction and deletion operations ...] which satisfy certain evident axioms".
In ...
- 1,768
1
vote
0
answers
42
views
Symmetry of cartesian multicategories in first order logic syntax
Cartesian multicategories are symmetric multicategories with a weakening and contraction operations.
When thinking of multicategories as some kind of "algebra" (?) of terms of first order ...
- 1,768