David Corfield
modal type theory

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’

  • X believes that Scott is the author of Waverley
  • X believes that Dickens is the author of Waverley

How does the interact with belief? If ‘the’ presupposes contractibility, must this presupposition be made by X?

  • King George knows that Scott is Scott
  • Scott is the author of Waverley
  • King George knows that the author of Waverley is Scott

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?

(pq)pq\Box(p \to q) \to \Box p \to \Box q.

Bas Spitters has its dependent type theoretic lift as

Dependent K: Π y:AB(y)Π x:AB[openx/y]\Box \Pi_{y:A} B(y) \to \Pi_{x: \Box A} \Box B [open x/y]

There are other formulations of axiom K:

(pq)pq\Box (p \wedge q) \leftrightarrow \Box p \wedge \Box q


(pq)pq\lozenge (p \vee q) \leftrightarrow \lozenge p \vee \lozenge q

Should the corresponding lift of the first be

x:AB(x) x:AB(x)\Box \sum_{x: A} B(x) \simeq \sum_{x: \Box A} \Box B(x)

Compare fact 2.10 of Wellen, https://arxiv.org/pdf/1806.05966.pdf

( x:AB(i A(x)))( x:A(B(x))) \Im (\sum_{x:A} B(i_A(x))) \simeq (\sum_{x: \Im A}\Im(B(x)))

When we have modalities in opposition on H\mathbf{H}, they take two forms:

\Box \dashv \bigcirc and \bigcirc \dashv \Box.

These arise from adjoint triples. Either two injections from an essential subcategory into H\mathbf{H}, or two projections onto a bireflective subcategory.


Essential subtopos \Box \dashv \bigcirc:

  • Illustrative: Even/odd inclusions in integers.
  • 010 \dashv 1, inclusions of 1\mathbf{1}.
  • \flat \dashv \sharp, inclusions of SetSet or of Grpd\infty Grpd as discrete/codiscrete.
  • \Re \dashv \Im, inclusions as reduced/coreduced.
  • R\rightsquigarrow \dashv \R
  • Reader/writer

Bireflective subcategory \bigcirc \dashv \Box:

  • Illustrative: Floor/ceiling projections of reals onto integers. From the point of view of Int, when Real’s thinking of π\pi, 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.

  • ʃʃ \dashv \flat, projections to discrete objects.

  • & \Im \dashv \&, projections to coreduced or formally etale objects.

  • \rightrightarrows \dashv \rightsquigarrow, projections to bosonic, even-graded, by taking even subalgebra and by quotienting out odd subalgebra.

Coalgebras of \Box = algebras of \bigcirc.

Base change, etc.

Given a map in H\mathbf{H} such as f:WVf: W \to V, or it could be a unit or counit, then f *. ff *. ff^{\ast} . \sum_{f} \dashv f^{\ast}. \prod_{f} (\bigcirc \dashv \Box), and f.f * f.f *\sum_f. f^{\ast} \dashv \prod_f . f^{\ast} ()\Box \dashv \bigcirc).

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 05:47:42. See the history of this page for a list of all contributions to it.