Modal types, especially Neel’s comment and next quotation.
See also nForum discussion.
If ‘X believes that’ is seen as a modality, do we make sense of substitution of Scott for ‘the author of Waverley’
How does the interact with belief? If ‘the’ presupposes contractibility, must this presupposition be made by X?
Famously, (iii) is false since King George had to ask for this information.
Two kinds of solution developed. (i) Restrict substitution of identicals to occur within simple (atomic) propositions, thereby excluding the appearance of modalities; (ii) Russell suggested that ‘the author of Waverley’ is not a term, so cannot be used to replace Scott.
Both seem wrong from modal HoTT point of view.
How do standard axioms of propositional modal logic get lifted to modal dependent type theory?
.
Bas Spitters has its dependent type theoretic lift as
Dependent K:
There are other formulations of axiom K:
and
Should the corresponding lift of the first be
Compare fact 2.10 of Wellen, https://arxiv.org/pdf/1806.05966.pdf
When we have modalities in opposition on , they take two forms:
and .
These arise from adjoint triples. Either two injections from an essential subcategory into , or two projections onto a bireflective subcategory.
Illustrative: Floor/ceiling projections of reals onto integers. From the point of view of Int, when Real’s thinking of , he returns 3. So necessarily 3. Or possibly 4. I glimpse a dial and can tell which interval it’s in.
Projection from world-varying types to invariant types via dependent sum and product. As expected, necessity here is right adjoint and preserves products.
, projections to discrete objects.
, projections to coreduced or formally etale objects.
, projections to bosonic, even-graded, by taking even subalgebra and by quotienting out odd subalgebra.
Coalgebras of = algebras of .
Given a map in such as , or it could be a unit or counit, then (), and (.
Does it work better one way with unit/counit?
For negative types, elimination rules are the counit, and introduction rules are form the defining adjunction. Elimination rules define the connective, and the introduction rule is derived from that requirement. Pragmatic.
For positive types, introduction rules are the unit, and elimination rules are from the defining adjunction. Introduction rule defines the connective, and the elimination rule is derived from that definition. Verificationist.
So unit/counit define the connective.
Last revised on November 13, 2018 at 10:47:42. See the history of this page for a list of all contributions to it.