Added a reference to Clemens Berger and Ralph M. Kaufmann’s *Comprehensive Factorization Systems*.

Add a temporary reference to Shulman’s paper (https://arxiv.org/abs/1004.3802) for the definition of autological category. An “autological category” page should be made eventually (or created as a subsection of the “axiom of separation” page).

]]>Adding disambiguation message to top of page

Anonymous

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

]]>there is *comprehensive factorization (michaelshulman)*.

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

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

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

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

]]>