# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorTobyBartels
• CommentTimeSep 5th 2011

This finally exists: axiom of separation.

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeSep 6th 2011

Hooray, thanks! I edited the comment about autology to accord with my answer in the other thread.

• CommentRowNumber3.
• CommentAuthorFinnLawler
• CommentTimeJan 20th 2014

New page at comprehension, describing Lawvere’s version of the comprehension schema in a hyperdoctrine, and also Jacobs’s variant.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeJan 21st 2014

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?)

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeJan 21st 2014

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.

• CommentRowNumber6.
• CommentAuthorFinnLawler
• CommentTimeJan 21st 2014

Looks fine. I’ve done some minor tidying-up, and added the example of the category of elements of a presheaf.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeJan 21st 2014

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?

• CommentRowNumber8.
• CommentAuthorFinnLawler
• CommentTimeJan 21st 2014

Yes, good point. I have rephrased things slightly.

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeJan 21st 2014
• (edited Jan 21st 2014)

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.

• CommentRowNumber10.
• CommentAuthorTobyBartels
• CommentTimeJan 26th 2014

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.)

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeJan 26th 2014

That sounds very reasonable to me. I am in favor of merging the entries. (But I won’t do it myself, now.)

• CommentRowNumber12.
• CommentAuthorTodd_Trimble
• CommentTimeJan 26th 2014

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?

• CommentRowNumber13.
• CommentAuthorUrs
• CommentTimeJan 26th 2014

But is “comprehensive” here really related to “comprehension”?

• CommentRowNumber14.
• CommentAuthorTodd_Trimble
• CommentTimeJan 26th 2014

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).

• CommentRowNumber15.
• CommentAuthorTodd_Trimble
• CommentTimeJan 26th 2014
• (edited Jan 26th 2014)

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.)

• CommentRowNumber16.
• CommentAuthorUrs
• CommentTimeJan 26th 2014

Ah, thanks. I’ll try to read this when I have a minute.

• CommentRowNumber17.
• CommentAuthorFinnLawler
• CommentTimeJan 26th 2014

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.

• CommentRowNumber18.
• CommentAuthorUrs
• CommentTimeJan 26th 2014

When you do these edits, I suppose you could cross-link with reflective factorization system and stable factorization system.

• CommentRowNumber19.
• CommentAuthorFinnLawler
• CommentTimeJan 26th 2014

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.

• CommentRowNumber20.
• CommentAuthorUrs
• CommentTimeJan 26th 2014
• (edited Jan 26th 2014)

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)

• CommentRowNumber21.
• CommentAuthorMike Shulman
• CommentTimeJan 27th 2014

Could also cross-link factorization system in a 2-category?

• CommentRowNumber22.
• CommentAuthorFinnLawler
• CommentTimeJan 27th 2014

I’ve given it a mention, beside the link to your page comprehensive factorization (michaelshulman). (Note to self: read and understand that page!)

• CommentRowNumber23.
• CommentAuthorUrs
• CommentTimeJan 29th 2014
• (edited Jan 29th 2014)

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?

• CommentRowNumber24.
• CommentAuthorMike Shulman
• CommentTimeJan 29th 2014

Yes, exactly. That’s what I was trying to say “elsewhere”.

• CommentRowNumber25.
• CommentAuthorUrs
• CommentTimeJan 29th 2014

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.

1. 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.

• CommentRowNumber27.
• CommentAuthortonyjones
• CommentTimeFeb 27th 2016

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.”

• CommentRowNumber28.
• CommentAuthorMike Shulman
• CommentTimeDec 3rd 2018

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).

• CommentRowNumber29.
• CommentAuthorMike Shulman
• CommentTimeDec 3rd 2018

BTW, this new thread could be merged with this one and (more obviously, but less interestingly) this one.

2. 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.