Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
This finally exists: axiom of separation.
Hooray, thanks! I edited the comment about autology to accord with my answer in the other thread.
New page at comprehension, describing Lawvere’s version of the comprehension schema in a hyperdoctrine, and also Jacobs’s variant.
Thanks, nice, I had not been aware of this.
I have added the tautological example (the hyperdoctrine over $Set$ of posets of subsets) to offer the reader help to see what the abstract definition is trying to achieve.
Apart from this I made two trivial formatting edits, please feel free to disagree:
gave Lawvere’s and Jacobs’ definition separate subsection
changed the notation $E X$ for the fibers to $E_X$ (okay?)
I have also made “comprehension scheme” a redirect and added links to old entries mentioning comprehension, such as second-order arithmetic and Trimble on ETCS III.
I notice that looking at axiom of separation that the relation between the two entries remains a bit vague at the moment.
Looks fine. I’ve done some minor tidying-up, and added the example of the category of elements of a presheaf.
Since you use the word “extension” now, should we add a remark that if the right adjoint exists, then it is called “extension”. So that “comprehension means that we have extension.” Is that the right way of speaking?
Yes, good point. I have rephrased things slightly.
We have an old stub entry extension (semantics) which used to just point to Wikipedia and otherwise receive a link from extensional type theory.
I have added a bare minimum to extension (semantics) and cross-linked it with comprehension.
I’m inclined to say that the contents of comprehension belong in axiom of separation, in the (so far quite brief) section on structural versions. It is the same axiom. (Note that a few axioms called ‘comprehension’ are defined at axiom of separation; also, axiom of comprehension and several variants already redirect there, although the particular phrases that currently redirect to comprehension.)
That sounds very reasonable to me. I am in favor of merging the entries. (But I won’t do it myself, now.)
There’s something else called the “comprehensive factorization”, but I can’t remember now how it goes. Maybe someone can add something to this effect, if it can be made to fit?
there is comprehensive factorization (michaelshulman).
But is “comprehensive” here really related to “comprehension”?
Thanks, Urs. I’m going to have to study what Mike wrote to remind myself how this is supposed to go, but if I remember correctly there is supposed to be a connection (it was originally called the comprehensive factorization because of some connection with comprehension).
It has something to do with generalizing the fact that an external predicate or relation on a set $A$, given by a monomorphism $S \hookrightarrow A$, is ’reified’ by a function $A \to \Omega$ or an element $1 \to P(A)$, only that in Mike’s context we are replacing relations by discrete op-fibrations over $A$ and functions $A \to \Omega$ by functors $A \to Set$, or at least so in the motivating examples. So comprehension is supposed to be abstracted: in a hyperdoctrine $S: E^{op} \to Pos$ (with motivating example $Sub: E^{op} \to Pos$, with $E$ a topos), comprehension allows us to ’reflect’ a predicate $p \in S(E)$ down into a morphism in the base category $E$. In the generalization we consider instead the pseudofunctor $S: E^{op} \to Cat$ corresponding to a fibration, and then factor through a discrete fibration…
Sorry, I realize that I’m making a mess here and am speaking something close to gibberish – I’ll have to think harder, or maybe someone can help out. I thought there was supposed to be a connection (due originally to Lawvere).
Well, instead of watching me babble here, maybe try this link where Claudio Hermida explains it. At least my memory wasn’t completely fabricated. (Maybe to babble a bit further, though, the factorization of a fibration $F \to A$ through a discrete op-fibration is supposed to remind one of a classifier $A \to \Omega$, where $\Omega$ is now standing for $Set$ and $A \to Set$ classifies the discrete op-fibration.)
Ah, thanks. I’ll try to read this when I have a minute.
I was planning to add something on the comprehensive factorization to comprehension when I got the chance, so I’ll do that this evening, and move the whole lot to axiom of separation at the same time.
There’s nothing complicated about the factorization system, really: a fibration with full comprehension gives a subfibration of the codomain fibration, and if the resulting ’subtype inclusions’ are closed under composition, then that gives you a factorization system on the base category (this is in Carboni et. al., On localization and stabilization for factorization systems). The factorization of a morphism is the commuting triangle given by the unit of the reflection. For the subobject fibration of a regular category this is the usual epi-mono factorization, whereas for the presheaf fibration over Cat it gives the factorization of an arbitrary functor into a final functor followed by a discrete fibration.
When you do these edits, I suppose you could cross-link with reflective factorization system and stable factorization system.
Right, I’ve moved everything to axiom of separation and added a section on the comprehensive factorization, as well as a redirect from the page comprehension. I’ve blanked the latter, but now I’m not sure whether that’s the right thing to do in this situation.
Thanks!
I have also renamed the now blank page to something (to “comprehension $\gt$ history” as it were, but it does not matter much) (and made sure to kill the automatically created redirect in the process)
Could also cross-link factorization system in a 2-category?
I’ve given it a mention, beside the link to your page comprehensive factorization (michaelshulman). (Note to self: read and understand that page!)
Mike just indirectly reminded me elsewhere of my going off into the blue in the thread on Finn’s thesis about dependent linear type theory and comprehension. Thinking about it, let me have another go:
Isn’t it right that: a linear hyperdoctrine having Lawvere-ian comprehension means equivalently that it has a dependent !-modality
?
Here I am assuming that in the definition of Lawvere-ian comprehension we say we are pushing the tensor unit instead of pushing the terminal object, which anyway seems to be a more robust way of going about it, I’d think.
Then following Ponto-Shulman 12, (4.3) (and using that by linear Frobenius reciprocity context extension/pullback preserves tensor units) the linearization functor $\Sigma$ is
$\Sigma \;\colon\; \mathbf{H}_{/X} \longrightarrow Mod(X)$given by sending any $(p : Y \to X) \in \mathbf{H}_X$ to $p_! 1_Y \in Mod(X)$ and this having a right adjoint $R$ that induces the dependent linear type theory $!_X$-comonad is precisely Lawvere’s comprehension in this case.
Right?
Yes, exactly. That’s what I was trying to say “elsewhere”.
Okay, thanks.
I have now briefly recorded this at comprehension – Examples – In linear dependent type theory. Also cross-linked with dependent linear type theory.
Created a stub for !-modality in the process.
This is a minor comment, but I did some digging up of references and noticed that what is described in the article as “Jacobs’ reformulation” is actually from Thomas Ehrhard’s thesis. That is stated clearly in Jacobs’ older article, “Comprehension categories and the semantics of type dependency”, and see also Ehrhard’s A Categorical Semantics of Constructions. I don’t have time to edit the article now, but will try to do it next week if no one gets around to it earlier.
Any thoughts on Bart Jacobs recent work on Quotient-Comprehension Chains? http://arxiv.org/abs/1511.01570 ”This paper reveals that quotients and comprehension are related to measurement, not only in quantum logic, but also in probabilistic and classical logic”
Also his work on the notion of effectus? http://arxiv.org/abs/1512.05813 “Effectus theory is a new branch of categorical logic that aims to capture the essentials of quantum logic, with probabilistic and Boolean logic as special cases. Predicates in effectus theory are not subobjects having a Heyting algebra structure, like in topos theory, but ‘characteristic’ functions, forming effect algebras. Such effect algebras are algebraic models of quantitative logic, in which double negation holds. Effects in quantum theory and fuzzy predicates in probability theory form examples of effect algebras.”
As far as I can tell, Ehrhard’s definition of comprehension requires not just that the fibers have terminal objects but that these are preserved by the reindexing functors. This is automatic if the fibration is a bifibration, as in Lawvere’s version; it’s fairly explicit in Ehrhard’s formulation, and somewhat implicit in Jacobs’ but I believe still present (his “terminal object functor” must, I think, be a fibered terminal object).
Re #29: Done. Comments #1 and #2 are from a Latest Changes thread entitled ’The axiom of separation’, the second of the two threads that Mike mentioned. Comments #3- #27 are from a Latest Changes thread entitled ’comprehension’, the first of the two threads that Mike mentioned.
Added a reference to Clemens Berger and Ralph M. Kaufmann’s Comprehensive Factorization Systems.
1 to 33 of 33