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.
1 to 59 of 59
There’s a classic debate which has run for the past century as to how to deal with a following situation presented by Russell in On Denoting. Consider the statements:
Famously (iii) is false since King George had to ask for this information, and yet it appears to result from substituting one term for the other in (ii) into (i).
The ’X knows’ operator is often taken as modal. Two kinds of solution then developed:
Given our analysis of the, it seems that we don’t want (ii).
Looking to the larger picture, has it all been worked out about how path induction works in the situation of modal types?
An even easier case looks at two names for what turns out to be the same person, traditionally Cicero and Tully. Then
is not valid. Have I got this right that we don’t have a construction
to produce a term in ?
But with the corresponding possibility modality ’as far as X knows’, we do have
because
does allow me to form a term in ?
That seems to suggest that does not operate on dependent types, i.e. the rule
is not sound. If it were then we could use path induction (= indiscernibility of identicals) as usual.
It makes sense in the ’locally everywhere’ interpretation of , such as in Awodey-Kishida sheaf semantics. A contingent identity in one world (one fiber) might not hold everywhere locally.
Dependent types meets sheaf interpretation of modal logic would seem to need fibrations within a fibration.
Is there something about acting somehow on each fiber of a fibration not yielding a fibration?
I don’t see how that’s relevant. The assumption has empty context, so it holds everywhere.
Have you seen Awodey and Kishida’s paper? If sheaf semantics can be used for first-order modal logic, it’s not too much of stretch to think that something similar would work for modal dependent type theory. In their system, holds at a world (point in the base space), if holds for all the worlds in a neighbourhood.
My thought was that two terms that might designate the same individual in one world could differ in another. This is like the classic case:
Metaphysicians illustrate this in terms of a close possible world to ours in which Nixon became a lawyer and didn’t enter politics.
Let’s not bring natural language into this and stick with formal systems. You said,
and I say, if we admit the rule
then we can conclude, using the standard rules for dependent type theory with equality, that .
Sure, I agree with that.
I was thinking about reasons we might be motivated not to admit the rule
What happens with Urs’s comonad flat modality? Do we have
Is this something to do with the point in Urs and Mike’s paper where they write
One maybe tempted to define the coreflection as we did the reflections and , but this would amount to asking for a pullback-stable system of coreflective subcategories of each , and at present we do not know any way to obtain this in models.
The issue is basically the same, yes. In isolation, the rule
only forces us to define for non-dependent types; but in the presence of the weakening rule, we also get
for every type , forcing us to define for all dependent types, and the substitution rule (for judgemental equality) forces this to be pullback-stable.
It seems to me that what this argument shows is that the argument of “X knows” is not a type but a piece of syntax, i.e. it is “quoted”.
Re Mike #10, I don’t quite see what you’re saying. As you know, there’s been a long tradition of taking certain constructions of the form “it is ??? that” as modalities attached to propositions, e.g, “it is necessarily the case that”, “it is known that”. You can at least see a family resemblance between them.
Now, it could all be misguided trying to develop a modal logic to capture such constructions, but then you may find philosophers unhappy that you’ve taken the term to talk about truncations, flat, sharp, etc., with no bearing on the historical use of modality.
Is there nothing to tell people pouring over puzzles such as:
On reflection, I think that what I was (very poorly) attempting to say is roughly equivalent to what Zhen is trying to say. Of course a modal operator like “X knows that …” is, like any other connective or quantifier, an operation on syntax. My point was that the meaning of this syntax is not “truth-functional”, i.e. it is not internalizable as a map , since there can be statements and that are equivalent (i.e. equal as elements of ), but such that “X knows that ” is true while “X knows that ” is false. This is more or less equivalent to saying that we can’t apply it in a nonempty context, since on the one hand if we had a function then we could just apply that function in any context, while on the other hand if we could apply in any context then we could apply it to the variable in context and then -abstract to get .
This is indeed very much the same as the issue that Urs and I had with , which we also weren’t able to internalize or apply in a nonempty context. In that case, we were able to sort of get around the issue by using the “externalized universe” ; I wonder if something similar would be possible here?
One issue is that I don’t know what it means to apply modalities like “X knows that” or “it is necessarily the case that” to a non-hprop type.
Traditionally, necessity reflects a stability under minor variation, where inessential features of an entity may alter, but essential features remain the same. So for an emerald, the property of being owned by me is inessential, but its being green is essential. This is often illustrated by ’possible’ world’ talk. The local neighbourhood approach of sheaf semantics for modal logic picks up on this idea. Close possible worlds to the ’actual world’ may have someone else own the gem, but it’s still green.
Someone, Robert Brandom I think, once claimed that many kinds of entity named in our language already contain some modal aspect. Perhaps then we could say ’emerald’ is already modal with respect to necessity, ’necessarily an emerald’ and ’emerald’ being equivalent. Then some types would not be modal. So ’necessarily an ingredient of beef stew’ is not equivalent to ’ingredient of beef stew’, the choice to add some ale being contingent, where the choice of beef is not.
But can’t we just ’guess’ how things might go by extending sheaf semantics to modal type theory? Awodey and Kishida look at untyped first-order modal logic, so have a set of individuals forming the domain of discourse, fibred over the possible worlds. Then a unary predicate picks out a subset of the total space. If an intensional type is modelled by an -groupoid, is there a natural way to see this as a single fibre over a point in a base space of possible worlds?
I was musing here that possible worlds could be taken themselves as forming a type, so that other types could depend on it.
That’s a very different kettle of fish. We know how to work with well-behaved modalities (say, a Lawvere-Tierney topology), and we know how to extend the modal operator to non-propositional types in that case (namely, sheafification). The so-called “sheaf semantics” of Awodey and Kishida is not of this form. To put it in type-theoretic language, what they are doing involves two types, and , and their modal operator acts on and . You could do the obvious thing and replace with , but then I completely lose sight of what this is supposed to mean: why should we be considering types fibred over the “domain of discourse” ?
Awodey-Kishida isn’t really what I would call “extending sheaf semantics to modal type theory”. I would say rather that they extend a classical semantics by a particular modality which happens to describe sheafification. In other words, they aren’t giving a sheaf-theoretic interpretation of modality; they’re giving a modal-logic interpretation of sheaves.
Awodey-Kishida isn’t really what I would call “extending sheaf semantics to modal type theory”.
I didn’t say it was. I meant, given what they did to classical logic, couldn’t we imagine doing something similar for dependent type theory?
they aren’t giving a sheaf-theoretic interpretation of modality; they’re giving a modal-logic interpretation of sheaves.
Hmm. Well, they’re not doing it for the benefit of helping mathematicians think about sheaves, rather to provide a complete semantics for a logic:
In this paper the topological interpretation is extended in a natural way to arbitrary theories of full first-order logic. The resulting system of S4 first-order modal logic is complete with respect to such topological semantics.
It’s an extension of the topological semantics for modal logic, as they say, in parallel with how Kripke sheaves are an extension of Kripke frames. And there’s a way of understanding the Kripke approach in terms of the topological approach.
I believe his group have a generalisation, see Topos Semantics for Higher-Order Modal Logic:
The usual Kripke, neighborhood, and sheaf semantics for propositional and first-order modal logic are subsumed by this notion.
Why not homotopify?
I meant, given what they did to classical logic, couldn’t we imagine doing something similar for dependent type theory?
Ah, right. Sorry, I misunderstood what you were saying.
I just went back to look at their paper again, and it looks like what they do depends fairly deeply on the traditional separation of “carrier sets” and “propositions” in first-order logic. In particular, they require the domains of variables to be sheaves and the basic function symbols to be continuous (i.e. maps of sheaves), but they allow relation symbols to be interpreted by arbitrary subsets (not necessarily subsheaves). I think this is what enables them to interpret as “interior” in a way that’s stable under substitution.
From a category-theoretic perspective, they’re considering the surjection of topoi , where is a set equipped with a topology, and the induced lex comonad on . Then they interpret the types of FOL by -coalgebras and the terms by -maps, but the relations by subobjects in that are not necessarily -coalgebras. Then if is such a relation, is probably the pullback of along the -coalgebra structure .
The natural generalization to DTT would be to consider itself as a “modal operator” on . But then we run into the same problem that Urs and I had with : it doesn’t internalize as an endomap of the universe, or act on dependent types in a substitutive way.
I haven’t been following in any detail (no time), but I see one thread that we keep re-hashing. Just to highlight:
David says something like this: There is all this traditional study of modal logic, and now here we are suddenly talking about a bunch of modalities in (homotopy) type theory without connecting to this traditional theory. Shouldn’t one make the connection?
(Is that roughly an accurate paraphrase, David?)
One impression about the traditional theory that I have is that its translation to English language modalities such as “necessity” tends to be artificial and driven more by the wish to make an identification than by an actual argument that the identification makes sense. As a result one runs into puzzlements of the kind that David highlights above. (Beyond the initial puzzlement of why a necessary truth should be “necessarily necessary”, as the usual phrasing of S4 in English language suggests. )
It seems to me that to make good sense of modalities of the kind “is known to be true” would require a vastly elaborate axiomatic system that would have actual reflection of complex concepts such as “knowledge”. I can see why philosophers are interested in this, but it just seems far premature to try (or pretend to) actually formalize this.
Personally I feel that the more “technical” and less “complex” modalities that we discuss in modal type theory (such as “is discrete”, “is codiscrete”) give a much better sense of what formal modality really is and can achieve.
…a much better sense of what formal modality really is and can achieve.
That would a difficult message to sell to my colleagues. I’m sure they’d think we’d just changed the subject. You’d be surprised at the extent to which ’possible world’ talk has become second nature to many in philosophy departments.
Perhaps we could say there are three attitudes to take here about ’philosophical’ motivation:
A) That the aim should be to get to the bottom of the nature of modalities, one of the most important of which is metaphysical necessity.
B) That it’s possible that thinking about such things can inspire some interesting developments in logic and mathematics.
C) That it’s largely a distraction and that one should follow the mathematics.
That Kripke adopted (A) is clear. Read ’Naming and Necessity’ and you see him grapple with the metaphysics of possible worlds. Or consider the description of a recent book by one of the UK’s most prominent philosophers.
I’m more inclined to (B). Even if Kripke was motivated in (A) style, it inspired him to develop Kripke frame semantics, a useful logico-mathematical idea. On a different topic, had we thought about Russell’s treatment of definite descriptions earlier (The King of France is bald) and tried to understand it type theoretically, we might have been led, before the rise of HoTT, to the need for a notion of contractability. So looking to see if anyone’s thought about modalities applied to types might pay off in unexpected ways.
But I’m also led by (C) considerations, in particular here the idea that there might be a way to take an existing classical set-up and extend it to a dependent type-theoretic one. So there’s an idea that bolted onto some Stone-like duality between Theories and their Models, one can take Modal Theories as the algebras for some monad and Modal Models as the the coalgebras for a comonad. The latter has the effect of turning a semantics into a frame semantics. Maybe something similar is possible on top of a Stone-like duality between HoTTs and their models.
Interesting you mention that Kripke was fascinated by a “metaphysics of possible worlds”. He would be very much in the fashion these days, too.
But what kind of worlds are we going to capture with formalism? Worlds that usefully contain the king of France will be hard to capture, accordingly formal reasoning about them is out of reach.
But I suppose I get the point now. I guess you’d want to be talking assuming some theory has been specified, and then have formal statements about aspects of its models. Some will be theorems of the theory, hence will necessarily hold in all models. Some will hold only in some models. If they hold in at least one model, then they are possibly true.
If that last suggestion is right, or is adopted, then that would mean that given a type of models over a theory, the necessity modality should be the monad on the category of types dependent on that type of models which is induced by dependent product, possibility would similarly be the comonad induced by dependent sum. Does that resonate with anything that modal people consider?
Urs 18 sounds like you are imagining (although I doubt that you actually think this) that someone invented the formal theory of modalities first and then started trying to translate them into ordinary language and came up with ideas like “possiby”. I’m sure the situation is the reverse: people wanted to describe language like “possibly” and invented formal modalities in order to do it. One can argue about how successful they were, but I expect to a philosopher that’s the point of the whole subject.
I don’t see any a priori reason why making sense of (say) epistemic modalities must require a vastly elaborate system of axioms about knowledge, any more than making sense of cohesive modalities requires a vastly elaborate description of topological groupoids. Even if constructing the semantics is complex, the syntax can be simple.
I think the “ doesn’t act on dependent types” point of view would reply to #11 as follows. The equality “9 = the number of planets in the solar system” is in the identity type of . We’d like to transport along this equality in a dependent type , but there is no such dependent type; the best we can hope to get from is .
So what is ? It’s natural to pronounce it as “the type of necessary natural numbers”. In #13 you suggested that some types are already modal, and if all emeralds are necessarily emeralds, it seems that all natural numbers would also be necessarily natural numbers. But even if that’s the case (which I’m not sure of), I think it would only argue that the counit map is surjective. It might be the case that two necessary natural numbers have equal underlying natural numbers, but are not equal as necessary natural numbers, and that could be what’s happening here: 9 and “the number of planets in the solar system” are not necessarily equal, so we don’t have an equality in to transport along in the dependent type .
(I don’t quite understand the distinction that the syntax suggests between “equal as necessary natural numbers” and “necessarily equal as natural numbers”, though.)
Similarly, we have “Scott = the author of Waverley” as an equality in the type , but it might not lift to an equality in the type of “King George knows that ”. We might interpret the latter as “King George’s mental model of the people in the world”, which could both omit some people that King George doesn’t know about, and include duplicate entries for some names that King George doesn’t realize refer to the same person. (It seems that it might also in theory contain fictitious people that King George believes in, which is a problem for defining a counit map .)
It’s less clear to me what happens when we transport the “planets” puzzle along the classical equivalence , since the “possibility” modality is “monadic” and so one might expect to be able to apply it dependently. Perhaps it hinges on the interpretation of . Is it the type of all natural numbers that might possibly exist? If we have two terms of type which happen to be equal, but it is possible that they are unequal, what happens when we apply the unit map ? I feel like perhaps this map is problematic in general and should be only a total relation.
In a snatched moment, re #23
It seems that it might also in theory contain fictitious people that King George believes in
“It is believed that” is generally taken not to satisfy S4. “It is known that” is generally taken to be something more or less approximated by “It is a justified true belief that”, so in particular requires truth. In which case we would not include fictitious people.
Got it, thanks.
re #22: Maybe you might remind me, what is the reasoning that should translate as “necessarily” and as “possibly”?
What confuses me is that the axioms are just that of a plain (co-)monad on a poset, so arguing that this encodes specifically necessity and possibility says that no other modality will have a (co)monadic appearance (for if it did, it would be either necessity or possibility).
I am really confused about this. I don’t want to be argumentative. I will shut up as soon as somebody explains it to me.
re #19:
just to remind myself I have created Naming and Necessity and cross-linked with a brief comment in the “Related concepts”-sections of both modal logic and multiverse.
Re #26, modal logicians need not restrict themselves to necessity/possibility. They are many modalities, including tense operators (’It will always be the case that’). Then there’s a vast range of possible modal logics (e.g., T, K, S1,…, S5, S4.5, etc.) (See here.) People argue as to which logic best captures which modality.
Naturally there’s a complicated story to be told of how modal logic came to take the form it has. There’s an interesting SEP article Modern Origins of Modal Logic which shows that part of the story involves concerns about the difference between material implication and strict implication. Godel later gets involved relating intuitionistic to modal logic. This is not surprising as one interpretation of ’necessity’ is ’it can be proved that’.
I should try to find out when ’metaphysical necessity’ gets taken seriously. One part of this story is that the logical positivists, who as positivists naturally wished to avoid metaphysics, had to come to terms with the difference between what appeared to be lawlike universal generalisations, and contingent ones, e.g.,
They tried to do this by means of the linguistic form of the statements, but it was widely considered not to work. There seems something ’modal’ going on in the former. Throw in another planet and it moves in an ellipse; put a coin in my pocket and it might be copper.
Kripke breaks with mere linguistic analysis to suggest we must talk about the world and the way it might be.
I added a page for Carnap’s Meaning and Necessity.
so arguing that this encodes specifically necessity and possibility says that no other modality will have a (co)monadic appearance (for if it did, it would be either necessity or possibility).
No, I think the point is that necessity and possibility are particular (co)monads, just as (say) an open subtopos, or the sharp modality, is a particular monad. The general framework of (co)monadic modalities includes all of them, but each presumably has specific properties and intended semantics not shared by the others.
Re #29, yes, not forgetting that modal logicians work in systems weaker than S4, so not even monadic. Some hold that S4 doesn’t hold even for necessity, e.g., here.
Here is somewhat related comment on modal operators in topos theory. Let be a topos and a Lawvere-Tierney topology in . This is a morphism ; for any formula of the internal language of , one obtains a weakened formula , where the precise meaning of “weakening” depends on the topology in question.
The association is truth-functional, so the interesting philosophical puzzle mentioned in #1 does not apply here.
However, one can also define the -translation . Like the double negation translation, this is obtained by putting a in front of every subformula. (The meaning of is that holds on the subtopos of -sheaves, i.e. if and only if .)
There is then the following observation: Let and be two formulas which happen to be equivalent in . Then it is not necessarily true that and are equivalent as well. However, if there is an intuitionistic proof of (which in particular implies that and are equivalent in ), then the -translated formulas are equivalent as well: .
In the example of #1, there is no intuitionistic proof that Scott is the author of Waverly (this simply happens to be true), so the equivalence “Scott is Scott the author of Waverly is Scott” is not preserved when applying a -translation.
Revisiting this thread, Mike in #23 wrote
It’s less clear to me what happens when we transport the “planets” puzzle along the classical equivalence ,…
One thought is that in grafting on modalities to some type theory, we might start by extending intuitionistic modal logic rather than the classical variety. In propositional versions of the former, and are independent. It seems there is an , which has operating on conjunctions as you’d expect, and likewise on disjunctions. Then there’s which adds connecting axioms:
then adds in axioms to ensure that is a comonad and a monad. So it seems any interaction between a pair of modalities happens through those connecting axioms above. Can they be seen as arising from some category theoretic construction?
Is the paper by Eric Goubault and his brother relevant here? I sort of remember their use of intuitionistic S4 (in one of its forms) and then modelling it by simplicial sets. It was: On the Geometry of Intuitionistic S4 Proofs, published in “Homomogy, Homotopy and Applications” (2003) and is linked to from Eric Goubault’s homepage.
According to Characterising intermediate tense logics in terms of Galois connections, it’s better to see the connecting axioms of #32 as mediating between a pair of galois connections to form a tense logic, i.e. one with four operators
( is true at some future time), ( was true at some past time), ( will be true at all future times), and ( has always been true in the past).
Of course, Galois connections are a promising direction if we want to find pairs of modalities as adjoints in an adjoint cylinder.
Oh, wow, I hadn’t been aware that anyone discussed adjoint modalities in the context of Galois connections, as on the bottom of p. 3 of the article (arXiv:1401.7646) that you mention.
I need to chase those references…
The ones I’ve seen have all taken comonadic modalities only to be right adjoints, e.g., Hermida in A categorical outlook on relational modalities and simulations. I guess that result at the top of p. 11 is closely related to the paper of #35’s entwined pairs of tense operators.
Returning to Mike’s #23, with the base change idea from necesssity and possibility, we see now we want to take world-dependent types to world-dependent types, that is, the sections extended back to .
The constants and also .
Then we may have , but .
I see what you and Mike are getting at here, but I don’t quite see yet how what you write will actually do what it’s intended to. Maybe I am missing something, but while that is so, allow me to suggest that it works as follows:
Given any type let be the constant -bundle, i.e. .
Then the difference between and is that is a constant section of the constant bundle (taking the same value on all ) while is not a constant section.
(Has it ever been mentioned in this thread here that indeed in our particular world the number of planets in the solar system is not 9? )
So they are of the same type, the difference you are after is elsewhere:
Consider the squashed identity type for simplicity (i.e. the proposition which is the (-1)-truncation of the identity type). Then consider the -dependent type
This is a bundle of propositions over . Its fiber over is the unit type if is 9, otherwise it is the empty type.
So the W-dependent type is not inhabited. In other words for we have (where is the W-dependent proposition which is false for all ), which we read as: “It is false that it is necessary that the number of planets in the solar system is 9.”, just as it should be.
However, with we have is an inhabited -dependent type. This we read as “It is true that it is possible that the number of planets in the solar system is 9.”, just as it should be.
I have taken the liberty of adding that to necessity and possibility – Examples.
So, really, the possible-worlds-modal-logic reply to #11 is that “9 = the number of planets in the solar system” can’t be asserted in the empty context; only necessary truths can be asserted in the empty context. (As always, it seems unsatisfying that the possible-worlds semantics doesn’t do anything to distinguish this world from all the other possible ones.)
Re #39, that’s the proper rendering of what I was gesturing at. I’m afraid the number 9 is just a vestige from earlier, happier days for Pluto in the Kripkean past.
Re #40, without wishing to open up that discussion, could we not send the S4 discussion on necessity and possibility elsewhere. Maybe to the logic S4(m)? Perhaps we could rename to ’necessity and possibility in HOTT’, or some such title, to discourage it becoming a place for other topics.
Re #41, can’t I write
?
We then have reassuringly
implies implies .
Of course, there’s still work to be done even to form ’’. It relies on there being a contractible -dependent type . If at least were a ’rigid designator’, and we had a dependent type ’planets of star(s)’, then something could be done. Of course, the complications of astronomy start to kick in with rogue planets, and binary stars with no planets , etc.
With we meet the counterparts/rigid designator debate that was often phrased in terms of ’Nixon’. Either I use a phrase which characterised Nixon in this world and might be thought to designate an individual in all possible worlds, such as ’the 36th president of the US’ (generating its own transworld issues) and seemingly not indicating the ’essence’ of Nixon, or I claim it is possible to pick out counterparts to Nixon in other worlds. You may imagine what there is to be said on the subject, e.g., in a very close world a different sperm reached a different egg, etc.
I can see that my from #38 didn’t look like it, but I did intend what Urs would have in #39 as .
But then why do you have and not ? Surely you want it to be a section, and then extended back to .
Mike, re #41, how about if we say it like this:
A necessity modality is always attached to a given choice of context/slice over – and should therefore better always be subscripted as – but with that understood, then it is indeed an endofunction on the type universe, but on the type universe in the slice of , i.e. it is a function . (Hm, is that right? Or something like this.)
David, re #43,
But then why do you have and not ? Surely you want it to be a section, and then extended back to .
Here I am not sure what you are after, as the term already is a section (of ). Its categorical semantics is a horizontal map in
and this seems to do just what it’s supposed to.
Maybe starting with a non-dependent type such as isn’t helping since we need to even start, but what I’m really interested in is your applied to general types not just propositions.
So let’s see what happens through the steps of applying to .
is just the non-dependent type .
Extending back under , then gives us pairs fibred over the first component, where .
So this is , a world-dependent type, and at my world (and so at any world), the functions ’9’ and ’number of planets’ aren’t the same, even if evaluated at my world they give the same answer.
Maybe since we started with an extension, this seems less motivated. Let’s pick a more interesting world-dependent type such as for celestial bodies in universe . What happens if we apply to it? Again we have pairs , where takes a world to a celestial body of that world. Two such s are ’The evening star’ and ’The morning star’ (assume all universes have something unique that brightly shines at the right time). Assuming also that in some universe they differ, we have that ’The evening star’ and ’The morning star’ are not identical.
Of course, this is already true back over in the non-sliced situation, but since we’re looking at modalities as maps from slice over to itself, we can also say that and are not identical, so express the situation as a non-identity in .
Does that make sense?
Of course, we can also do it your way and reduce to a world-dependent proposition ’morning star(w) = evening star(w)’, but my point is that we don’t have to restrict ourselves to propositions when applying modalities.
I didn’t mean to suggest to concentrate only on dependent propositions. That just seemed to be the thing to do in the example at hand.
I agree with all you say above. I am just wondering what you have in mind where you say “isn’t helping”. Do you want to exclude explicitly applying ?
The -operation (maybe we should find a nicer symbol for it) has the nice feature that it captures the idea, mentioned in the above discussion, of “necessary terms”.
A term might be called necessary (or rather “-necessary”) precisely it is in the image under of a global term.
Maybe it’s possible to characterize the -necessary terms by just using and not itself? Hm, not sure.
By “isn’t helping”, I just meant “is making harder to see what’s going on”. But in fact working through the CB example, it didn’t make much of a difference.
All it seemed to boil down to in the question of whether to work here with necessity applied to all types rather than just propositions was something like the difference between being able to say straight out of two functions that they’re different, and only being able to express this in terms of a place where they differ.
A term might be called necessary…
Do we need to give a condition for when a term should be called necessary? Doesn’t a term always come as typed, in which case if its typed by a -necessary type, then it’s -necessary.
But then what is a -necessary type? Something in the image of ? We don’t have idempotency, but maybe that doesn’t matter.
The two things I see as needing doing are
1) To engage with philosophers, one would need to have thoughts on the Nixon/counterparts issues I mentioned in #42.
2) See what happens for more interesting s than discrete sets.
i) We already spoke once of allowing it to be . I had an inkling it might be possible to tie in with what people were saying about perceptual invariants.
ii) Then there could be cohesive world types, etc. When Judea Pearl takes up Lewis’s account of possible worlds to approach counterfactuals, he uses a notion of proximity of worlds in terms of certain minimal changes to make it the case that , when we say had been the case, would have happened.
Whether “necessary term” is a good English word to choose here may be debatable, I was just suggesting that reading it as “constant term” comes close to how you and Mike seemed to have imagined using it above.
A term of type does not need to be constant (while the type is constant) so calling these terms “necessary terms” would be an incompatible convention. I’d rather call terms of “witnesses of necessity”, and there may be a different witness in different worlds.
I am all in favor of discussing this for the case that . I keep trying to advertize to HoTT-practitioners that working with HoTT in the context of pointed connected types has the enormous potential of being a synthetic version of homotopy representation theory. Would seem to be a most excellent topic for everyone looking for topics in HoTT. But so far nothing much has happened. (Generally, presently nothing much seems to be happening on the HoTT-front?!)
A necessity modality is always attached to a given choice of context/slice over – and should therefore better always be subscripted as – but with that understood, then it is indeed an endofunction on the type universe, but on the type universe in the slice of , i.e. it is a function .
Yes, I agree. What I’m getting out of this discussion is that maybe doesn’t really deserve to be called “necessity” when applied to non-propositions. A term of , as David said, consists of, for each world, a function assigning a natural number to every world. (I don’t think it’s necessary to write , since this is in fact the natural numbers object in the slice over .) It’s not clear to me what is “necessary” about this. One might be tempted to say that an element of is “a natural number that exists in all worlds”, but in fact that’s already true of elements of itself as long as we are in the slice over . The same is true of ; “The morning star” and “The evening star” are already both elements of . The difference between and is that an element of is a single function assigning to each world a celestial body in that world, while an element of consists of one such function for each world.
So in homotopy type theory “necessarily” is to similar as is to : strictly speaking the former comes from the latter by composition with (-1)-truncation. It’s something to stay aware of, but is not troublesome, I’d say. Sometimes it’s useful to think of the untruncated as being “the real existential quantifier”, and maybe from some higher perspective the analog is true of , too.
Re #50, but I guess at least instantiating at our actual world gives us a way to talk about a full function, such as as fully existing for us in our world, if you see what I mean.
So we get a nice map .
Although “instantiating at a world” isn’t something that takes place in the modal logic on which acts, but is an external or metatheoretic operation.
Coming back to the suggested terminology of “necessary types”: if we had an idempotent adjunction, then we’d immediately be justified to call a -type. Now the we are looking at is not in general idempotent, but (assuming an ambient topos) it always factors through an idempotent operation (as here).
Hm, on the other hand, how does that factorization of monads through idempotent monads interact with adjoints of monads. When does an adjoint triple factor through an adjoint cylinder?
(This is slight abuse of terminology: Lawvere defined an adjoint cylonder to be an adjoint triple where the two outer adjoints are fully faithful, whereas here I am after the case where the middle one is.)
More concretely:
given a morphism in a topos , what is the co-localization of at the -equivalences?
The colocalization exists, and it does contain at least the objects in the image of the pullback , because (of course) for a -equivalence then is an equivalence. So in this sense the objects of the form really are “necessary types” (the -necessary types).
Are there more necessary types?
I didn’t follow why we know the colocalization exists. Is it because the idempotent comonad-core exists? Do we know that in the -case?
I was thinking:
First, a sufficient condition for Bousfield co-localizations of model categories to exist is their right properness. I take this from p. 9 of arXiv:0708.3435.
This is for small sets of localizing morphisms, but I was assuming now that the resolution of the size issue is as for the known cases. But maybe I am wrong about that.
Actually, it seems that Barwick’s condition is additionally for small sets of localizing objects. And it’s not clear to me that the usual sort of local-presentability tricks can be played to make large things small, since we are in the dual situation.
Thanks, good point. So I should take that back. Still we may ask for the class of co-local objects, which is maybe all that actually matters for the above discussion. It contains the objects in the image of and what else?
1 to 59 of 59