Skip to main content
18 events
when toggle format what by license comment
Apr 5, 2013 at 17:23 vote accept David Spivak
Apr 5, 2013 at 17:21 history edited David Spivak CC BY-SA 3.0
typo
Apr 5, 2013 at 6:15 comment added Andrej Bauer Oh, I am actually grateful to you for drilling into this. I thought it was obvious we wanted to do things internally, so we needed some internal axioms to start from. It's sometimes very hard to guess what the audience is really thinking :-)
Apr 4, 2013 at 22:51 comment added François G. Dorais OK. I see, and you want to prove these in the internal logic. There are many ways to look at this and I now see I was blindsided. Thanks for your patience, Andrej.
Apr 4, 2013 at 21:27 comment added Andrej Bauer If I just have some type $V$ and know nothing about it, that is not very useful. I need to know some properties, so I can start proving things.
Apr 4, 2013 at 19:41 comment added François G. Dorais Ah, I see. You're distinguishing the fact that $G$ is not a variable in the internal logic. I think I'm on the same page now. Still, that doesn't explain why you want $V$ to be definable.
Apr 4, 2013 at 19:32 comment added François G. Dorais But $V$ is a specific graph here. Why is it important that $V$ is definable in the internal logic? Isn't it sufficient that $V$ exists?
Apr 4, 2013 at 19:29 comment added François G. Dorais So, the discrete graphs (as identified by peeking into the objects) are precisely the graphs such that $G \times V \to G$ is epi. There is a simple formula in the internal logic, which evaluates to $\top \in \Omega$ precisely for such $G$.
Apr 4, 2013 at 19:11 comment added François G. Dorais OK. I'm lost now. Are we talking about the same thing? At what point do you need quantification over all types? Let's back up... What is "the projection $G\times V \to G$ is onto"? (I interpret it as the usual way of saying that the projection $G \times V \to G$ is epi in the internal logic.)
Apr 4, 2013 at 18:18 comment added Andrej Bauer I do not understand this parameter business. The internal language of the topos of graphs is a type theory. Every object of the topos is a type, i.e., the internal language is a real mix of semantics and syntax. Also, there is no such thing as a "parameter type". We might do some things schematically by using metavariables in place of types. So perhaps this is different from set theory, where sets are individuals that can be parametrized over in the language. In the topos language, anything of the form "for all types, ..." is not part of the language.
Apr 4, 2013 at 17:23 comment added François G. Dorais OK, I understand. Since it's conservative to add such a constant there is no harm done, but why is it advantageous to add $V$ as a constant rather than use it as a parameter? (Sorry for bugging you with all these questions, I'm just very curious to understand your point of view.)
Apr 4, 2013 at 17:04 comment added Andrej Bauer I do not think of $V$ as a parameter. It is a primitive type in the internal language of the topos of graphs, i.e., it is a constant. It is no more a parameter than the type $N$ of the natural numbers. It is good that we can characterise $V$ up to isomorphism wiht an internal statement, because then its interpretation is fixed.
Apr 4, 2013 at 16:11 comment added François G. Dorais "A graph $G$ is discrete when the projection $G\times V \to G$ is onto" defines discreteness using $V$ as a parameter. Later, you show that there is a parameter-free definition since $V$ is definable (up to isomorphism). Am I missing the point of the last few paragraphs where you argue that $V$ is definable?
Apr 4, 2013 at 15:54 comment added Andrej Bauer I am not sure I understand you. What would be a parameter-non-free definition of an object?
Apr 4, 2013 at 15:15 comment added François G. Dorais That was too brief a question... I didn't read the parameter-free requirement in the op's question. I do find it interesting when something is parameter-free definable and I'm happy you are addressing that issue, but I wonder why you find it such a sticking point.
Apr 4, 2013 at 12:23 comment added François G. Dorais Why is it important for $V$ to be parameter-free definable?
Apr 4, 2013 at 9:00 history edited Andrej Bauer CC BY-SA 3.0
added 144 characters in body
Apr 4, 2013 at 8:47 history answered Andrej Bauer CC BY-SA 3.0