Separately from my day-job at University of Cambridge, I am independently researching tools for scientific thought and developing software like Forester that you can use to unlock your brain. If you have benefited from this work or the writings on my blog, please considering supporting me with a sponsorship on Ko-fi.

I have been thinking about monoidal closed structures induced by slicing over a monoid, which has been considered by Combette and Munch-Maccagnoni as a potential denotational semantics of destructors à la C++. It occurred to me that this construction is, in fact, almost a degenerate case of Day convolution on an internal monoidal category — and this made me realize that there might be a nice way to understand Day convolution in the language of fibered categories. In fact, many of these results (in particular the relativization to internal monoidal categories) are probably a special case of Theorem 11.22 of Shulman’s paper on enriched indexed categories.

Under appropriate assumptions, we may also compute a “Day hom” by adjointness.

I believe, but did not check carefully, that when E and F are discrete fibrations over a semimonoidal category { \left ( B , \otimes , \alpha \right )} then the Day tensor is precisely the discrete fibration corresponding to the (contravariant) Day convolution of the presheaves corresponding to E and F. Likewise when { \left ( B , \otimes ,I, \alpha , \lambda , \rho \right )} is monoidal, it appears that the Day unit corresponds precisely to the traditional one.

There remain some interesting directions to explore. First of all, the claims above would obviously lead to a new construction of the Day convolution monoidal structure on the 1-category of discrete fibrations on B that coincides with the traditional one up to the Grothendieck construction. But in general, we should expect to exhibit both { \mathbf{Cat} } _{ / B } and \mathbf{Fib} _{ B } as monoidal bicategories, a result that I have not seen before.

The conjecture above is highly non-trivial, as monoidal bicategories are extremely difficult to construct explicitly. I am hoping that Michael Shulman’s ideas involving monoidal double categories could potentially help.

I have been thinking again about the relationship between quantitative type theory and synthetic Tait computability and other approaches to type refinements. One of the defining characteristics of QTT that I thought distinguished it from STC was the treatment of types: in QTT, types only depend on the “computational” / unrefined aspect of their context, whereas types in STC are allowed to depend on everything. In the past, I mistakenly believed that this was due to the realizability-style interpretation of QTT, in contrast with STC’s gluing interpretation. It is now clear to me that (1) QTT is actually glued (in the sense of q-realizability, no pun intended), and (2) the nonstandard interpretation of types in QTT corresponds to adding an additional axiom to STC, namely the tininess of the generic proposition.

It has been suggested to me by Neel Krishnaswami that this property of QTT may not be desirable in all cases (sometimes you want the types to depend on quantitative information), and that for this reason, graded type theories might be a better way forward in some applications. My results today show that STC is, in essence, what you get when you relax the QTT’s assumption that types do not depend on quantitative information. This suggests that we should explore the idea of multiplicities within the context of STC — as any monoidal product on the subuniverse spanned by closed-modal types induces quite directly a form of variable multiplicity in STC, I expect this direction to be fruitful.

My thoughts on the precise relationship between the QTT models and Artin gluing will be elucidated at a different time. Today, I will restrict myself to sketching an interpretation of a QTT-style language in STC assuming the generic proposition is internally tiny.

Let \mathscr{Q} be an elementary topos equipped with a subterminal object \P \hookrightarrow \mathbf{1} inducing an open subtopos \mathscr{E} \simeq { \mathscr{Q} } _{ / \P } \hookrightarrow \mathscr{Q} and its complementary closed subtopos \mathscr{F} \hookrightarrow \mathscr{Q}. This structure is the basis of the interpretation of STC; if you think of STC in terms of refinements, then stuff from \mathscr{E} is “computational” and stuff from \mathscr{F} is “logical”.

We now consider the interpretation of a language of (potentially quantitative) refinements into \mathscr{Q}. A context \Gamma is interpreted by an object of \mathscr{Q}; a type \Gamma \vdash A is interpreted by a family A \to \bigcirc{\Gamma}; a term \Gamma \vdash a : A is interpreted as a map \Gamma \to A such that \Gamma \to A \to \bigcirc \Gamma is the unit of the monad.

So far we have not needed anything beyond the base structure of STC in order to give an interpretation of types in QTT’s style. But to extend this interpretation to a universe, we must additionally assume that \P is internally tiny, in the sense that the exponential functor { \left ( - \right )} ^ \P is a left adjoint. Under these circumstances, the idempotent monad \bigcirc \equiv j_*j^* : \mathscr{Q} \to \mathscr{Q} corresponding to the open immersion j : \mathscr{E} \hookrightarrow \mathscr{Q} has a right adjoint \square : \mathscr{Q} \to \mathscr{Q}, an idempotent comonad.

Although \square lifts to each slice of \mathscr{Q}, these liftings do not commute with base change; this will, however, not be an obstacle for us.

We will now see how to use the adjunction \bigcirc \dashv \square to interpret a universe, either for the purpose of interpreting universes of refinement types, or for the purpose of strictifying the model that we have sketched. Let \mathcal{V} be a (standard) universe in \mathscr{Q}, e.g. a Hofmann–Streicher universe; we shall then interpret the corresponding universe of refinements as \mathcal{U} : \equiv \square \mathcal{V}. To see that \mathcal{U} classifies \mathcal{V}-small families of refinements, we compute as follows:

1. A code \Gamma \vdash \hat{A} : \mathcal{U} amounts to nothing more than a morphism \hat{A} : \Gamma \to \square{\mathcal{V}}.
2. By adjoint transpose, this is the same as a morphism \hat{A} ^ \sharp : \bigcirc{\Gamma} \to \mathcal{V}.

Thus we see that if \mathcal{V} is generic for \mathcal{V}-small families of (arbitrary) types in \mathscr{Q}, then \mathcal{U} \equiv \square \mathcal{V} is generic for \mathcal{V}-small families of type refinements, i.e. types whose context is \bigcirc-modal.

Finally, we comment that the tininess of \P is satisfied in many standard examples, the simplest of which is the Sierpiński topos \mathbf{Set} ^{ \to }.

For any small category \mathscr{C}, Fiore treats \mathscr{C}-sorted abstract syntax in the functor category { \left [ \mathscr{C} , \operatorname{Pr} { \left ( \operatorname{\mathbb{L}} { \mathscr{C} } \right )} \right ]} where \operatorname{\mathbb{L}} is some 2-monad on \mathbf{Cat}; any such functor P denotes a set that is indexed in sorts and contexts (where the 2-monad \operatorname{\mathbb{L}} takes a category of sorts to the corresponding category of contexts). When \mathscr{C} is a set and \operatorname{\mathbb{L}} is either finite limit or finite product completion, we recover the standard notions of many-sorted abstract syntax; in general, we get a variety of forms of dependently sorted or generalized abstract syntax.

We will assume here that \operatorname{\mathbb{L}} is the free finite limit completion 2-monad; our goal is to study Fiore’s general substitution monoidal structure from the point of view of classifying topoi, building on Johnstone’s analogous observations (Elephant, D3.2) on the non-symmetric monoidal structure of the object classifier. The topos theoretic viewpoint that we will explore is nothing more than a rephrasing of Fiore’s account in terms of the Kleisli composition in a 2-monad; nonetheless the perspective of classifying topoi is enlightening, as it provides an explanation for precisely what internal geometrical structure one expects in a given topos for abstract syntax, potentially leading to improved internal languages.

For any small category \mathscr{C}, the category of presheaves \operatorname{Pr} { \left ( \operatorname{\mathbb{L}} \mathscr{C} \right )} corresponds to the classifying topos of diagrams of shape \mathscr{C}. Following Anel and Joyal, we shall write \mathbb{A} ^{ \mathscr{C} } for this “affine” classifying topos; under the conventions of op. cit., we may then identify the category of sheaves \operatorname{Sh} { \mathbb{A} ^{ \mathscr{C} } } with the presheaf category \operatorname{Pr} { \left ( \operatorname{\mathbb{L}} { \mathscr{C} } \right )}.

The universal property of \mathbb{A} ^{ \mathscr{C} } as the classifying topos of \mathscr{C}-diagrams means that for any topos \mathcal{X}, a diagram { \mathscr{C} } \xrightarrow{P} { \operatorname{Sh} { \mathcal{X} } } corresponds essentially uniquely (by left Kan extension) to a morphism of topoi { \mathcal{X} } \xrightarrow{\bar{P}} { \mathbb{A} ^{ \mathscr{C} } }. We have a generic \mathscr{C}-shaped diagram { \mathscr{C} } \xrightarrow{\mathrm{G} _{ \mathscr{C} }} { \operatorname{Sh} { \mathbb{A} ^{ \mathscr{C} } } } corresponding under this identification to the identity map on \mathbb{A} ^{ \mathscr{C} }. More explicitly, the diagram \mathrm{G} _{ \mathscr{C} } is the following composite:

Given a morphism of topoi { \mathcal{X} } \xrightarrow{f} { \mathbb{A} ^{ \mathscr{C} } }, we may recover the diagram \mathscr{C} \to{\operatorname{Sh} { \mathcal{X} }} that it classifies as the composite \mathscr{C} \xrightarrow{\mathrm{G} _{ \mathscr{C} }} \operatorname{Sh} { \mathbb{A} ^{ \mathscr{C} } } \xrightarrow{f ^{ * }} \operatorname{Sh} { \mathcal{X} }.

In case \mathcal{X} \equiv \mathbb{A} ^{ \mathscr{C} }, then, we have a correspondence between \mathscr{C}-shaped diagrams of sheaves on \mathbb{A} ^{ \mathscr{C} } and endomorphisms of \mathbb{A} ^{ \mathscr{C} }; we are interested in representing the compositions of such endomorphisms as a tensor product on the functor category { \left [ \mathscr{C} , \operatorname{Sh} { \mathbb{A} ^{ \mathscr{C} } } \right ]}.

In particular, let { \mathscr{C} } \xrightarrow{P,Q} { \operatorname{Sh} { \mathbb{A} ^{ \mathscr{C} } } } be two diagrams; taking characteristic maps, we have endomorphisms of affine topoi { \mathbb{A} ^{ \mathscr{C} } } \xrightarrow{\bar{P} , \bar{Q}} { \mathbb{A} ^{ \mathscr{C} } }, which we may compose to obtain { \mathbb{A} ^{ \mathscr{C} } } \xrightarrow{\bar{Q} \circ \bar{P}} { \mathbb{A} ^{ \mathscr{C} } }; then, we will define the tensor P \bullet Q to be the diagram whose characteristic morphism of affine topoi is \bar{P} \circ \bar{Q}. In other words:

To give an explicit computation of the tensor product, we first compute the inverse image of any { \mathbb{A} ^{ \mathscr{C} } } \xrightarrow{f} { \mathbb{A} ^{ \mathscr{C} } } on representables よ_{ \mathscr{C} } \Gamma for \Gamma \in \operatorname{\mathbb{L}} \mathscr{C}. As any left exact functor { \operatorname{\mathbb{L}} \mathscr{C} } \xrightarrow{H} { \mathscr{E} } is the right Kan extension of { \mathscr{C} } \xrightarrow{H \circ \eta _ \mathscr{C}} { \mathscr{E} } along { C } \xrightarrow{\eta _ \mathscr{C}} { \operatorname{\mathbb{L}} \mathscr{C} }, we can conclude that H \Gamma \cong \operatorname{lim} _{ \Gamma \to \eta _ \mathscr{C} {d} } H { \left ( \eta _ \mathscr{C} {d} \right )}. We will use this in our calculation below, setting H: \equiv f ^{ * } \circ よ_{ \mathscr{C} }.

We are now prepared to compute the tensor product of any { \mathscr{C} } \xrightarrow{P,Q} { \operatorname{Sh} { \mathbb{A} ^{ \mathscr{C} } } }.

Finally, we can relate the computation above to that of Fiore in terms of coends.

Above, we have written { \left ( \cdot \right )} and { \left ( \pitchfork \right )} for the tensoring and cotensoring of \operatorname{Sh} { \mathbb{A} ^{ \mathscr{C} } } over \mathbf{Set} respectively. Thus, the fully pointwise computation is as follows:

Thanks to Marcelo Fiore and Daniel Gratzer for helpful discussions.

I have long been an enthusiast for outliners, a genre of computer software that deserves more than almost any other to be called an “elegant weapon for a more civilized age”. Recently I have been enjoying experimenting with Jesse Grosjean’s highly innovative outliner for macOS called Bike, which builds on a lot of his previous (highly impressive) work in the area with a level of fit and finish that is rare even in the world of macOS software. Bike costs $29.99 and is well-worth it; watch the introductory video or try the demo to see for yourself.

The purpose of outliners is to provide room to actively think; Grothendieck is said to have been unable to think at all without a pen in his hand, and I think of outliners as one way to elevate the tactile aspect of active thinking using the unique capabilities of software. Tools for thinking must combat stress and mental weight, and the most immediate way that outliners achieve this is through the ability to focus on a subtree — narrowing into a portion of the hierarchy and treating it as if it were the entire document, putting its context aside. This feature, which some of my readers may recognize from Emacs org-mode, is well-represented in Bike — without, of course, suffering the noticeable quirks that come from the Emacs environment, nor the ill-advised absolute/top-down model of hierarchy sadly adopted by org-mode.

As a scientist in academia, one of the most frequent things I am doing when I am not writing my own papers or working with students is refereeing other scientists’ papers. For those who are unfamiliar, this means carefully studying a paper and then producing a detailed and well-structured report that includes a summary of the paper, my personal assessment of its scientific validity and value, and a long list of corrections, questions, comments, and suggestions. Referee reports of this kind are then used by journal editors and conference program committees to decide which papers deserve to be published.

In this post, I will give an overview of my refereeing workflow with Bike and how I overcame the challenges transferring finished referee reports from Bike into the text-based formats used by conference refereeing platforms like HotCRP and EasyChair using a combination of XSLT 2.0 and Pandoc. This tutorial applies to Bike 1.14; I hope the format will not change too much, but I cannot make promises about what I do not control.

5424 jms-0089.rss.xml jms-0089 jms-0089.xml 2023 8 29 Jon Sterling

Most scientific conferences solicit and organize reviews for papers using a web platform such as HotCRP and EasyChair; although these are not the same, the idea is similar. Once you have been assigned to referee a paper, you will receive a web form with several sections and large text areas in which to put the components of your review; not all conferences ask for the same components, but usually one is expected to include the following in addition to your (numerical) assessment of the paper’s merit and your expertise:

1. A summmary of the paper
2. Your assessment of the paper
3. Detailed comments for the authors
4. Questions to be addressed by author response
5. Comments for the PC (program committee) and other reviewers

Usually you will be asked to enter your comments under each section in a plain text format like Markdown. The first thing a new referee learns is not to type answers directly into the web interface, because this is an extremely reliable way to lose hours of your time when a browser or server glitch deletes all your work. Most of us instead write out our answers in a separate text editor, and paste them into the web interface when we are satisfied with them. In the past, I have done this with text files on my computer, but today I want to discuss how to draft referee reports as outlines in Bike; then I will show you how to convert them to the correct plain text format that can be pasted into your conference’s preferred web-based refereeing platform.

To start off, have a look at the figure below, which shows my refereeing template outline in Bike.

5425 jms-0086.rss.xml Figure jms-0086 jms-0086.xml 2023 8 28 Jon Sterling https://git.sr.ht/~jonsterling/bike-convertors/tree/main/item/example.bike

As you can see, there is a healthy combination of hierarchy and formatting in a Bike outline.

5426 jms-008B.rss.xml jms-008B jms-008B.xml 2023 8 29 Jon Sterling

Bike is a rich text editor, but one that (much like GNU TeXmacs) avoids the classic pitfalls of nearly all rich text editors, such as the ubiquitous and dreaded “Is the space italic?!” user-experience failure; I will not outline Bike innovative approach to rich text editing here, but I suggest you check it out for yourself.

5427 jms-008A.rss.xml jms-008A jms-008A.xml 2023 8 29 Jon Sterling

One of the most useful features of Bike’s approach to formatting is the concept of a row type, which is a semantic property of a row that has consequences for its visual presentation. Bike currently supports the following row types:

• Plain rows
• Heading rows, formatted in boldface
• Note rows, formatted in gray italics
• Quote rows, formatted with a vertical bar to their left
• Ordered rows, formatted with an (automatically chosen) numeral to their left
• Unordered rows, formatted with a bullet to their left
• Task rows, formatted with a checkbox to their left

My refereeing template uses several of these row types (headings, notes, tasks) as well as some of the rich text formatting (highlighting). When I fill out the refereeing outline, I will use other row types as well — including quotes, ordered, and unordered rows. I will create a subheading under Detailed comments for the author to contain my questions and comments, which I enter in as ordered rows; then I make a separate subheading at the same level for Typographical errors, which I populate with unordered rows. Unordered rows are best for typos, because they are always accompanied already by line numbers. If I need to quote an extended portion of the paper, I will use a quote row.

When working on the report outline, I will constantly be focusing on individual sections to avoid not only distractions but also the intense mental weight of unfinished sections. Focusing means that the entire outline is narrowed to a subtree that can be edited away from its context; this is achieved in Bike by pressing the gray south-easterly arrows to the right of each heading, as seen in the figure.

<?xml version="1.0" encoding="UTF-8"?>
<html xmlns="http://www.w3.org/1999/xhtml">
  <head>
    <meta charset="utf-8"/>
  </head>
  <body>
    <ul id="2sbcmmms">
      <li id="3C" data-type="heading">
        <p>Tasks</p>
        <ul>
          <li id="cs" data-type="task">
            <p>read through paper on iPad and highlight</p>
          </li>
        </ul>
      </li>
      <li id="XZ" data-type="heading">
        <p>Syntax and semantics of foo bar baz</p>
        <ul>
          <li id="Kp">
            <p><mark>Overall merit:</mark><span> </span></p>
          </li>
          <li id="d9">
            <p><mark>Reviewer Expertise:</mark></p>
          </li>
          <li id="uM" data-type="heading">
            <p>Summary of the paper</p>
            <ul>
              <li id="oB" data-type="note">
                <p>Please give a brief summary of the paper</p>
              </li>
              <li id="TWZ">
                <p>This paper describes the syntax and semantics of foo, bar, and baz.</p>
              </li>
            </ul>
          </li>
          <li id="V8" data-type="heading">
            <p>Assessment of the paper</p>
            <ul>
              <li id="vD" data-type="note">
                <p>Please give a balanced assessment of the paper's strengths and weaknesses and a clear justification for your review score.</p>
              </li>
            </ul>
          </li>
          <li id="zo" data-type="heading">
            <p>Detailed comments for authors</p>
            <ul>
              <li id="o0" data-type="note">
                <p>Please give here any additional detailed comments or questions that you would like the authors to address in revising the paper.</p>
              </li>
              <li id="bgy" data-type="heading">
                <p>Minor comments</p>
                <ul>
                  <li id="tMq" data-type="unordered">
                    <p>line 23: "teh" =&gt; "the"</p>
                  </li>
                  <li id="EmX" data-type="unordered">
                    <p>line 99: "fou" =&gt; "foo"</p>
                  </li>
                </ul>
              </li>
            </ul>
          </li>
          <li id="aN" data-type="heading">
            <p>Questions to be addressed by author response</p>
            <ul>
              <li id="7s" data-type="note">
                <p>Please list here any specific questions you would like the authors to address in their author response. Since authors have limited time in which to prepare their response, please only ask questions here that are likely to affect your accept/reject decision.</p>
              </li>
            </ul>
          </li>
          <li id="4S" data-type="heading">
            <p>Comments for PC and other reviewers</p>
            <ul>
              <li id="bN" data-type="note">
                <p>Please list here any additional comments you have which you want the PC and other reviewers to see, but not the authors.</p>
              </li>
              <li id="i2b">
                <p>In case any one is wondering, I am an expert in foo, but not in bar nor baz.</p>
              </li>
            </ul>
          </li>
        </ul>
      </li>
    </ul>
  </body>
</html>

brew install saxon

brew install pandoc

<?xml version="1.0"?>

<xsl:stylesheet version="2.0"
  xmlns="http://www.w3.org/1999/xhtml"
  xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  xmlns:xhtml="http://www.w3.org/1999/xhtml"
  exclude-result-prefixes="xhtml">

  <xsl:output method="xml" version="1.0" encoding="UTF-8" indent="yes" />
  <xsl:strip-space elements="*" />

  <xsl:template match="xhtml:html | xhtml:body | xhtml:code | xhtml:strong | xhtml:em | xhtml:mark">
    <xsl:copy>
      <xsl:apply-templates select="node()|@*" />
    </xsl:copy>
  </xsl:template>

  <xsl:template match="xhtml:span">
    <xsl:apply-templates />
  </xsl:template>

  <xsl:template match="xhtml:ul">
    <xsl:for-each-group select="xhtml:li" group-adjacent="string(@data-type)">
      <xsl:choose>
        <xsl:when test="@data-type='ordered' or @data-type='task'">
          <ol>
            <xsl:apply-templates select="current-group()" />
          </ol>
        </xsl:when>
        <xsl:when test="@data-type='unordered'">
          <ul>
            <xsl:apply-templates select="current-group()" />
          </ul>
        </xsl:when>
        <xsl:otherwise>
          <xsl:apply-templates select="current-group()" />
        </xsl:otherwise>
      </xsl:choose>
    </xsl:for-each-group>
  </xsl:template>

  <xsl:template match="xhtml:li">
    <xsl:apply-templates />
  </xsl:template>

  <xsl:template
    match="xhtml:li[@data-type='ordered' or @data-type='unordered' or @data-type='task']/xhtml:p">
    <li>
      <xsl:apply-templates />
    </li>
  </xsl:template>

  <xsl:template match="xhtml:li[@data-type='heading']/xhtml:p">
    <xsl:element
      name="h{count(ancestor::xhtml:li[@data-type='heading'])}">
      <xsl:apply-templates />
    </xsl:element>
  </xsl:template>

  <xsl:template match="xhtml:li[@data-type='quote']/xhtml:p">
    <blockquote>
      <xsl:apply-templates />
    </blockquote>
  </xsl:template>

  <xsl:template match="xhtml:li[@data-type='note']/xhtml:p">
    <p>
      <em>
        <xsl:apply-templates />
      </em>
    </p>
  </xsl:template>

  <xsl:template match="xhtml:li[not(@data-type)]/xhtml:p">
    <p>
      <xsl:apply-templates />
    </p>
  </xsl:template>
</xsl:stylesheet>

cat review.bike | saxon -xsl:bike-to-html.xsl - > review.html

<?xml version="1.0" encoding="UTF-8"?>
<html xmlns="http://www.w3.org/1999/xhtml">
   <body>
      <h1>Tasks</h1>
      <ol>
         <li>read through paper on iPad and highlight</li>
      </ol>
      <h1>Syntax and semantics of foo bar baz</h1>
      <p>
         <mark>Overall merit:</mark>
      </p>
      <p>
         <mark>Reviewer Expertise:</mark>
      </p>
      <h2>Summary of the paper</h2>
      <p>
         <em>Please give a brief summary of the paper</em>
      </p>
      <p>This paper describes the syntax and semantics of foo, bar, and baz.</p>
      <h2>Assessment of the paper</h2>
      <p>
         <em>Please give a balanced assessment of the paper's strengths and weaknesses and a clear justification for your review score.</em>
      </p>
      <h2>Detailed comments for authors</h2>
      <p>
         <em>Please give here any additional detailed comments or questions that you would like the authors to address in revising the paper.</em>
      </p>
      <h3>Minor comments</h3>
      <ul>
         <li>line 23: "teh" =&gt; "the"</li>
         <li>line 99: "fou" =&gt; "foo"</li>
      </ul>
      <h2>Questions to be addressed by author response</h2>
      <p>
         <em>Please list here any specific questions you would like the authors to address in their author response. Since authors have limited time in which to prepare their response, please only ask questions here that are likely to affect your accept/reject decision.</em>
      </p>
      <h2>Comments for PC and other reviewers</h2>
      <p>
         <em>Please list here any additional comments you have which you want the PC and other reviewers to see, but not the authors.</em>
      </p>
      <p>In case any one is wondering, I am an expert in foo, but not in bar nor baz.</p>
   </body>
</html>

cat review.html | pandoc -f html -t markdown-raw_html-native_divs-native_spans-fenced_divs-bracketed_spans-smart | sed 's/\\//g'

# Tasks

1.  read through paper on iPad and highlight

# Syntax and semantics of foo bar baz

Overall merit:

Reviewer Expertise:

## Summary of the paper

*Please give a brief summary of the paper*

This paper describes the syntax and semantics of foo, bar, and baz.

## Assessment of the paper

*Please give a balanced assessment of the paper's strengths and
weaknesses and a clear justification for your review score.*

## Detailed comments for authors

*Please give here any additional detailed comments or questions that you
would like the authors to address in revising the paper.*

### Minor comments

-   line 23: "teh" => "the"
-   line 99: "fou" => "foo"

## Questions to be addressed by author response

*Please list here any specific questions you would like the authors to
address in their author response. Since authors have limited time in
which to prepare their response, please only ask questions here that are
likely to affect your accept/reject decision.*

## Comments for PC and other reviewers

*Please list here any additional comments you have which you want the PC
and other reviewers to see, but not the authors.*

In case any one is wondering, I am an expert in foo, but not in bar nor
baz.

cat review.bike | saxon -xsl:bike-to-html.xsl - | pandoc -f html -t markdown-raw_html-native_divs-native_spans-fenced_divs-bracketed_spans-smart | sed 's/\\//g'

Lurie states the following result as Proposition 7.2.1.14 of Higher Topos Theory:

Let \mathcal{X} be an ∞-topos and let { \mathcal{X} } \xrightarrow{\tau _{ \leq 0}} { \tau _{ \leq 0} \mathcal{X} } be the left adjoint to the inclusion. A morphism { U } \xrightarrow{\phi} { X } in \mathcal{X} is an effective epimorphism if and only if in \tau _{ \leq 0} { \left ( \phi \right )} is an effective epimorphism in the ordinary topos \mathrm{h} { \left ( \tau _{ \leq0 } \mathcal{X} \right )}.

Several users of MathOverflow have noticed that the proof of this result given by Lurie is circular. The result is true and can be recovered in a variety of ways, as pointed out in the MathOverflow discussion. For expository purposes, I would like to show how to prove this result directly in univalent foundations using standard results about n-truncations from the HoTT Book.

First we observe a trivial lemma about truncations.

It follows from the above that \left \lVert { \textstyle \sum _{ x:A }} B \left \lvert x \right \rvert _{ 0 } \right \rVert _{ -1 } is equivalent to \left \lVert { \textstyle \sum _{ x: \left \lVert A \right \rVert _{ 0 } }} Bx \right \rVert _{ -1 }. This is enough to deduce the main result.

The Stacks project is the most successful scientific hypertext project in history. Its goal is to lay the foundations for the theory of algebraic stacks; to facilitate its scalable and sustainable development, several important innovations have been introduced, with the tags system being the most striking.

Each tag refers to a unique item (section, lemma, theorem, etc.) in order for this project to be referenceable. These tags don't change even if the item moves within the text. (Tags explained, The Stacks Project).

Many working scientists, students, and hobbyists have wished to create their own tag-based hypertext knowledge base, but the combination of tools historically required to make this happen are extremely daunting. Both the Stacks project and Kerodon use a cluster of software called Gerby, but bitrot has set in and it is no longer possible to build its dependencies on a modern environment without significant difficulty, raising questions of longevity.

Moreover, Gerby’s deployment involves running a database on a server (in spite of the fact that almost the entire functionality is static HTML), an architecture that is incompatible with the constraints of the everyday working scientist or student who knows at most how to upload static files to their university-provided public storage. The recent experience of the nLab’s pandemic-era hiatus and near death experience has demonstrated with some urgency the pracarity faced by any project relying heavily on volunteer system administrators.

In this article, I will show you how to set up your own forest using the Forester software. These instructions pertain to the Forester 2.3 version.

opam install forester

git init forest
cd forest

git pull https://git.sr.ht/~jonsterling/forest-template

forester build --dev --root=xxx-0001 trees/

python3 -m http.server 1313 -d output

\title{Jon Sterling}
\taxon{person}
\meta{external}{https://www.jonmsterling.com/}
\meta{institution}{University of Cambridge}
\meta{orcid}{0000-0002-0585-5564}
\meta{position}{Associate Professor}

\p{Associate Professor in Logical Foundations and Formal Methods at University of Cambridge. Formerly a [Marie Skłodowska-Curie Postdoctoral Fellow](jms-0061) hosted at Aarhus University by [Lars Birkedal](larsbirkedal), and before this a PhD student of [Robert Harper](robertharper).}

forester new --dir=trees --prefix=xxx

\date{2023-08-15}

\title{my first tree}
\author{jonmsterling}

\transclude{xxx-NNNN}

\title{creation of (co)limits}
\date{2023-02-11}
\taxon{definition}
\author{jonmsterling}

\def\CCat{#{\mathcal{C}}}
\def\DCat{#{\mathcal{D}}}
\def\ICat{#{\mathcal{I}}}
\def\Mor[arg1][arg2][arg3]{#{{\arg2}\xrightarrow{\arg1}{\arg3}}}

\p{Let \Mor{U}{\CCat}{\DCat} be a functor and let \ICat be a category. The functor #{U} is said to \em{create (co)limits of #{\ICat}-figures} when for any diagram \Mor{C_\bullet}{\ICat}{\CCat} such that #{\ICat\xrightarrow{C_\bullet}\CCat\xrightarrow{F}\DCat} has a (co)limit, then #{C_\bullet} has a (co)limit that is both preserved and reflected by #{F}.}

It is easy to teach a student how to give a naïve denotational semantics to a language like System T, and then use it to reason about the equational theory: a type might as well be a set, and a program might as well be a function, and equational adequacy at base type is established using a logical relation between the initial model and the category of sets. Adding any non-trivial feature to this language (e.g. general recursion, polymorphism, state, etc.) immediately increases the difficulty beyond the facility of a beginner: to add recursion, one must replace sets and functions with domains and continuous maps, and to accommodate polymorphism and state, one must pass to increasingly inaccessible variations on this basic picture.

The dream of the 1990s was to find a category that behaves like \mathbf{Set} in which even general recursive and effectful programming languages could be given naïve denotational semantics, where types are interpreted as “sets” and programs are interpreted as a “functions”, without needing to check any arduous technical conditions like continuity. The benefit of this synthetic domain theory is not only that it looks “easy” for beginners, as more expert-level constructions like powerdomains or even domain equations for recursively defined semantic worlds become simple and direct. Although there have been starts and stops, the dream of synthetic domain theory is alive and well in the 21st Century. Today’s synthetic domain theory is, however, both more modular and more powerful than ever before, and has yielded significant results in programming language semantics including simple denotational semantics for an state of the art programming language with higher-order polymorphism, dependent types, recursive types, general reference types, and first-class module packages that can be stored in the heap.

In this talk, I will explain some important classical results in synthetic domain theory as well as more recent results that illustrate the potential impact of “naïve denotational semantics” on the life of a workaday computer scientist.

Impredicative guarded dependent type theory (iGDTT) is a new version of type theory that combines guarded recursion (the "later" modality) with impredicative polymorphism (universal and existential types). It turns out that these two features are sufficient to define a very simple denotational semantics for System F with recursive types and higher-order store. We believe that the expressivity of iGDTT brings us one step closer to a general metalanguage for realistic denotational semantics, and provides a compelling strategy to elude the burden of operational semantics. As a further benefit, we are now able to justify the extension of full dependent type theory with a Haskell-style IO-monad and IORef types.

Jacobs has proposed definitions for (weak, strong, split) generic objects for a fibered category; building on his definition of (split) generic objects, Jacobs develops a menagerie of important fibrational structures with applications to categorical logic and computer science, including higher order fibrations, polymorphic fibrations, 𝜆2-fibrations, triposes, and others. We observe that a split generic object need not in particular be a generic object under the given definitions, and that the definitions of polymorphic fibrations, triposes, etc. are strict enough to rule out some fundamental examples: for instance, the fibered preorder induced by a partial combinatory algebra in realizability is not a tripos in this sense. We propose a new alignment of terminology that emphasizes the forms of generic object appearing most commonly in nature, i.e. in the study of internal categories, triposes, and the denotational semantics of polymorphism. In addition, we propose a new class of acyclic generic objects inspired by recent developments in higher category theory and the semantics of homotopy type theory, generalizing the realignment property of universes to the setting of an arbitrary fibration.

Separation logic is used to reason locally about stateful programs. State of the art program logics for higher-order store are usually built on top of untyped operational semantics, in part because traditional denotational methods have struggled to simultaneously account for general references and parametric polymorphism. The recent discovery of simple denotational semantics for general references and polymorphism in synthetic guarded domain theory has enabled us to develop Tulip, a higher-order separation logic over the typed equational theory of higher-order store for a monadic version of System \textbf{F} ^{ \mu , \textit{ref} }. The Tulip logic differs from operationally-based program logics in two ways: predicates range over the meanings of typed terms rather than over the raw code of untyped terms, and they are automatically invariant under the equational congruence of higher-order store, which applies even underneath a binder. As a result, “pure” proof steps that conventionally require focusing the Hoare triple on an operational redex are replaced by a simple equational rewrite in Tulip. We have evaluated Tulip against standard examples involving linked lists in the heap, comparing our abstract equational reasoning with more familiar operational-style reasoning. Our main result is the soundness of Tulip, which we establish by constructing a BI-hyperdoctrine over the denotational semantics of \textbf{F} ^{ \mu , \textit{ref} } in an impredicative version of synthetic guarded domain theory.

It often happens that free algebras for a given theory satisfy useful reasoning principles that are not preserved under homomorphisms of algebras, and hence need not hold in an arbitrary algebra. For instance, if M is the free monoid on a set A, then the scalar multiplication function A \times M \to M is injective. Therefore, when reasoning in the formal theory of monoids under A, it is possible to use this injectivity law to make sound deductions even about monoids under A for which scalar multiplication is not injective — a principle known in algebra as the permanence of identity. Properties of this kind are of fundamental practical importance to the logicians and computer scientists who design and implement computerized proof assistants like Lean and Coq, as they enable the formal reductions of equational problems that make type checking tractable.

As type theories have become increasingly more sophisticated, it has become more and more difficult to establish the useful properties of their free models that facilitate effective implementation. These obstructions have facilitated a fruitful return to foundational work in type theory, which has taken on a more geometrical flavor than ever before. Here we expose a modern way to prove a highly non-trivial injectivity law for free models of Martin-Löf type theory, paying special attention to the ways that contemporary methods in type theory have been influenced by three important ideas of the Grothendieck school: the relative point of view, the language of universes, and the recollement of generalized spaces.

Several different topoi have played an important role in the development and applications of synthetic guarded domain theory (SGDT), a new kind of synthetic domain theory that abstracts the concept of guarded recursion frequently employed in the semantics of programming languages. In order to unify the accounts of guarded recursion and coinduction, several authors have enriched SGDT with multiple “clocks” parameterizing different time-streams, leading to more complex and difficult to understand topos models. Until now these topoi have been understood very concretely qua categories of presheaves, and the logico-geometrical question of what theories these topoi classify has remained open. We show that several important topos models of SGDT classify very simple geometric theories, and that the passage to various forms of multi-clock guarded recursion can be rephrased more compositionally in terms of the lower bagtopos construction of Vickers and variations thereon due to Johnstone. We contribute to the consolidation of SGDT by isolating the universal property of multi-clock guarded recursion as a modular construction that applies to any topos model of single-clock guarded recursion.

We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets à la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) by Artin gluing.

We present calf, a cost-aware logical framework for studying quantitative aspects of functional programs. Taking inspiration from recent work that reconstructs traditional aspects of programming languages in terms of a modal account of phase distinctions, we argue that the cost structure of programs motivates a phase distinction between intension and extension. Armed with this technology, we contribute a synthetic account of cost structure as a computational effect in which cost-aware programs enjoy an internal noninterference property: input/output behavior cannot depend on cost. As a full-spectrum dependent type theory, calf presents a unified language for programming and specification of both cost and behavior that can be integrated smoothly with existing mathematical libraries available in type theoretic proof assistants.

We evaluate calf as a general framework for cost analysis by implementing two fundamental techniques for algorithm analysis: the method of recurrence relations and physicist’s method for amortized analysis. We deploy these techniques on a variety of case studies: we prove a tight, closed bound for Euclid’s algorithm, verify the amortized complexity of batched queues, and derive tight, closed bounds for the sequential and parallel complexity of merge sort, all fully mechanized in the Agda proof assistant. Lastly we substantiate the soundness of quantitative reasoning in calf by means of a model construction.

We propose a new sheaf semantics for secure information flow over a space of abstract behaviors, based on synthetic domain theory: security classes are open/closed partitions, types are sheaves, and redaction of sensitive information corresponds to restricting a sheaf to a closed subspace. Our security-aware computational model satisfies termination-insensitive noninterference automatically, and therefore constitutes an intrinsic alternative to state of the art extrinsic/relational models of noninterference. Our semantics is the latest application of Sterling and Harper’s recent re-interpretation of phase distinctions and noninterference in programming languages in terms of Artin gluing and topos-theoretic open/closed modalities. Prior applications include parametricity for ML modules, the proof of normalization for cubical type theory by Sterling and Angiuli, and the cost-aware logical framework of Niu et al. In this paper we employ the phase distinction perspective twice: first to reconstruct the syntax and semantics of secure information flow as a lattice of phase distinctions between “higher” and “lower” security, and second to verify the computational adequacy of our sheaf semantics with respect to a version of Abadi et al.’s dependency core calculus to which we have added a construct for declassifying termination channels.

The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design: the phase distinction, computational effects, and type abstraction. We contribute a fresh “synthetic” take on program modules that treats modules as the fundamental constructs, in which the usual suspects of prior module calculi (kinds, constructors, dynamic programs) are rendered as derived notions in terms of a modal type-theoretic account of the phase distinction. We simplify the account of type abstraction (embodied in the generativity of module functors) through a lax modality that encapsulates computational effects, placing projectibility of module expressions on a type-theoretic basis.

Our main result is a (significant) proof-relevant and phase-sensitive generalization of the Reynolds abstraction theorem for a calculus of program modules, based on a new kind of logical relation called a parametricity structure. Parametricity structures generalize the proof-irrelevant relations of classical parametricity to proof-relevant families, where there may be non-trivial evidence witnessing the relatedness of two programs—simplifying the metatheory of strong sums over the collection of types, for although there can be no “relation classifying relations,” one easily accommodates a “family classifying small families.”

Using the insight that logical relations/parametricity is itself a form of phase distinction between the syntactic and the semantic, we contribute a new synthetic approach to phase separated parametricity based on the slogan logical relations as types, by iterating our modal account of the phase distinction. We axiomatize a dependent type theory of parametricity structures using two pairs of complementary modalities (syntactic, semantic) and (static, dynamic), substantiated using the topos theoretic Artin gluing construction. Then, to construct a simulation between two implementations of an abstract type, one simply programs a third implementation whose type component carries the representation invariant.

We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of \beta/\eta-normal forms. As corollaries we obtain both decidability of judgmental equality and the injectivity of type constructors.

Extending Martín Hötzel Escardó’s effectful forcing technique, we give a new proof of a well-known result: Brouwer’s monotone bar theorem holds for any bar that can be realized by a functional of type { \left ( \mathbb{N} \to \mathbb{N} \right )} \to \mathbb{N} in Gödel’s System T. Effectful forcing is an elementary alternative to standard sheaf-theoretic forcing arguments, using ideas from programming languages, including computational effects, monads, the algebra interpretation of call-by-name λ-calculus, and logical relations. Our argument proceeds by interpreting System T programs as well-founded dialogue trees whose nodes branch on a query to an oracle of type \mathbb{N} \to \mathbb{N}, lifted to higher type along a call-by-name translation. To connect this interpretation to the bar theorem, we then show that Brouwer’s famous "mental constructions" of barhood constitute an invariant form of these dialogue trees in which queries to the oracle are made maximally and in order.

We contribute XTT, a cubical reconstruction of Observational Type Theory [Altenkirch et al., 2007] which extends Martin-Löf's intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity proofs principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel extension of the logical families or categorical gluing argument inspired by Coquand and Shulman: every closed element of boolean type is derivably equal to either true or false.

Modalities are everywhere in programming and mathematics! Despite this, however, there are still significant technical challenges in formulating a core dependent type theory with modalities. We present a dependent type theory MLTT🔒 supporting the connectives of standard Martin-Löf Type Theory as well as an S4-style necessity operator. MLTT🔒 supports a smooth interaction between modal and dependent types and provides a common basis for the use of modalities in programming and in synthetic mathematics. We design and prove the soundness and completeness of a type checking algorithm for MLTT🔒, using a novel extension of normalization by evaluation. We have also implemented our algorithm in a prototype proof assistant for MLTT🔒, demonstrating the ease of applying our techniques.

Nakano’s later modality can be used to specify and define recursive functions which are causal or synchronous; in concert with a notion of clock variable, it is possible to also capture the broader class of productive (co)programs. Until now, it has been difficult to combine these constructs with dependent types in a way that preserves the operational meaning of type theory and admits a hierarchy of universes. We present an operational account of guarded dependent type theory with clocks called Guarded Computational Type Theory, featuring a novel clock intersection connective that enjoys the clock irrelevance principle, as well as a predicative hierarchy of universes which does not require any indexing in clock contexts. Guarded Computational Type Theory is simultaneously a programming language with a rich specification logic, as well as a computational metalanguage that can be used to develop semantics of other languages and logics.

In this paper, we present an extension to Martin-Löf’s Intuitionistic Type Theory which gives natural solutions to problems in pragmatics, such as pronominal reference and presupposition. Our approach also gives a simple account of donkey anaphora without resorting to exotic scope extension of the sort used in Discourse Representation Theory and Dynamic Semantics, thanks to the proof-relevant nature of type theory.

We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voevodsky’s univalent foundations. We observe for the first time the profound impact of univalence on the denotational semantics of mutable state. Univalence automatically ensures that all computations are invariant under symmetries of the heap—a bountiful source of free theorems. In particular, even the most simplistic univalent model enjoys many new program equivalences that do not hold when the same constructions are carried out in the universes of traditional set-level (extensional) type theory.

We present decalf, a directed, effectful cost-aware logical framework for studying quantitative aspects of functional programs with effects. Like calf, the language is based on a formal phase distinction between the extension and the intension of a program, its pure behavior as distinct from its cost measured by an effectful step-counting primitive. The type theory ensures that the behavior is unaffected by the cost accounting. Unlike calf, the present language takes account of effects, such as probabilistic choice and mutable state; this extension requires a reformulation of calf’s approach to cost accounting: rather than rely on a “separable” notion of cost, here a cost bound is simply another program. To make this formal, we equip every type with an intrinsic preorder, relaxing the precise cost accounting intrinsic to a program to a looser but nevertheless informative estimate. For example, the cost bound of a probabilistic program is itself a probabilistic program that specifies the distribution of costs. This approach serves as a streamlined alternative to the standard method of isolating a recurrence that bounds the cost in a manner that readily extends to higher-order, effectful programs.

The development proceeds by first introducing the decalf type system, which is based on an intrinsic ordering among terms that restricts in the extensional phase to extensional equality, but in the intensional phase reflects an approximation of the cost of a program of interest. This formulation is then applied to a number of illustrative examples, including pure and effectful sorting algorithms, simple probabilistic programs, and higher-order functions. Finally, we justify decalf via a model in the topos of augmented simplicial sets.

It often happens that free algebras for a given theory satisfy useful reasoning principles that are not preserved under homomorphisms of algebras, and hence need not hold in an arbitrary algebra. For instance, if M is the free monoid on a set A, then the scalar multiplication function A \times M \to M is injective. Therefore, when reasoning in the formal theory of monoids under A, it is possible to use this injectivity law to make sound deductions even about monoids under A for which scalar multiplication is not injective — a principle known in algebra as the permanence of identity. Properties of this kind are of fundamental practical importance to the logicians and computer scientists who design and implement computerized proof assistants like Lean and Coq, as they enable the formal reductions of equational problems that make type checking tractable.

As type theories have become increasingly more sophisticated, it has become more and more difficult to establish the useful properties of their free models that facilitate effective implementation. These obstructions have facilitated a fruitful return to foundational work in type theory, which has taken on a more geometrical flavor than ever before. Here we expose a modern way to prove a highly non-trivial injectivity law for free models of Martin-Löf type theory, paying special attention to the ways that contemporary methods in type theory have been influenced by three important ideas of the Grothendieck school: the relative point of view, the language of universes, and the recollement of generalized spaces.

We present a novel mechanism for controlling the unfolding of definitions in dependent type theory. Traditionally, proof assistants let users specify whether each definition can or cannot be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core type theory with extension types, a connective first introduced in the context of homotopy type theory. We prove a normalization theorem for our core calculus and have implemented our system in the cooltt proof assistant, providing both theoretical and practical evidence for it.

We contribute the first denotational semantics of polymorphic dependent type theory extended by an equational theory for general (higher-order) reference types and recursive types, based on a combination of guarded recursion and impredicative polymorphism; because our model is based on recursively defined semantic worlds, it is compatible with polymorphism and relational reasoning about stateful abstract datatypes. We then extend our language with modal constructs for proof-relevant relational reasoning based on the logical relations as types principle, in which equivalences between imperative abstract datatypes can be established synthetically. Finally we develop a decomposition of the store model as a general construction that extends an arbitrary polymorphic call-by-push-value adjunction with higher-order store, improving on Levy's possible worlds model construction; what is new in relation to prior typed denotational models of higher-order store is that our Kripke worlds need not be syntactically definable, and are thus compatible with relational reasoning in the heap. Our work combines recent advances in the operational semantics of state with the purely denotational viewpoint of synthetic guarded domain theory.

Existential types are reconstructed in terms of small reflective subuniverses and dependent sums. The folklore decomposition detailed here gives rise to a particularly simple account of first class modules as a mode of use of traditional second class modules in connection with the modal operator induced by a reflective subuniverse, leading to a semantic justification for the rules of first-class modules in languages like OCaml and MoscowML. Additionally, we expose several constructions that give rise to semantic models of ML-style programming languages with both first-class modules and realistic computational effects, culminating in a model that accommodates higher-order first class recursive modules and higher-order store.

Logical relations are the main tool for proving positive properties of logics, type theories, and programming languages: canonicity, normalization, decidability, conservativity, computational adequacy, and more. Logical relations combine pure syntax with non-syntactic objects that are parameterized in syntax in a somewhat complex way; the sophistication of possible parameterizations makes logical relations a tool that is primarily accessible to specialists. In the spirit of Halmos' book Naïve Set Theory, I advocate for a new viewpoint on logical relations based on synthetic Tait computability, the internal language of categories of logical relations. In synthetic Tait computability, logical relations are manipulated as if they were sets, making the essence of many complex logical relations arguments accessible to non-specialists.

Hofmann and Streicher famously showed how to lift Grothendieck universes into presheaf topoi, and Streicher has extended their result to the case of sheaf topoi by sheafification. In parallel, van den Berg and Moerdijk have shown in the context of algebraic set theory that similar constructions continue to apply even in weaker metatheories. Unfortunately, sheafification seems not to preserve an important realignment property enjoyed by the presheaf universes that plays a critical role in models of univalent type theory as well as synthetic Tait computability, a recent technique to establish syntactic properties of type theories and programming languages. In the context of multiple universes, the realignment property also implies a coherent choice of codes for connectives at each universe level, thereby interpreting the cumulativity laws present in popular formulations of Martin-Löf type theory.

We observe that a slight adjustment to an argument of Shulman constructs a cumulative universe hierarchy satisfying the realignment property at every level in any Grothendieck topos. Hence one has direct-style interpretations of Martin-Löf type theory with cumulative universes into all Grothendieck topoi. A further implication is to extend the reach of recent synthetic methods in the semantics of cubical type theory and the syntactic metatheory of type theory and programming languages to all Grothendieck topoi.

PhD student of Robert Harper.

The course aims to introduce the mathematics of discrete structures, showing it as an essential tool for computer science that can be clever and beautiful.