Question about the formal rules of cohesive homotopy type theory

[Madeleine Birchfield]

In Mike Shulman's presentation of cohesive homotopy type theory in his 2018 article Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, he states in section 2 that "All the ordinary rules of type theory (∏-types, ∑-types, =-types, W -types, HITs) are imported into our theory only in the world of cohesive variables." Does this also include the structural rules of type theory such as the substitution and weakening rules?

Madeleine Birchfield

[Michael Shulman]

Substitution and weakening hold for all types with the restriction that only crisp terms (i.e. those involving only crisp variables) can be substituted for crisp variables.  This restriction is mentioned in the beginning of section 2.

On Fri, Nov 11, 2022 at 3:14 PM Madeleine Birchfield <madeleine...@gmail.com> wrote:

In Mike Shulman's presentation of cohesive homotopy type theory in his 2018 article Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, he states in section 2 that "All the ordinary rules of type theory (∏-types, ∑-types, =-types, W -types, HITs) are imported into our theory only in the world of cohesive variables." Does this also include the structural rules of type theory such as the substitution and weakening rules?

Madeleine Birchfield

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/96f15467-49c9-43cc-8868-40b1bdf2162dn%40googlegroups.com.

[andrej...@andrej.com]

> Does this also include the structural rules of type theory such as the substitution and weakening rules?

I would just like to point out that substutition and weakening typically are not part of the rules. They are shown to be admissible. In this spirit, the question should have been: what is the precise version of substitution and weakening (which is a special case of substitution) that is admissible in cohesive type theory?

With kind regards,

Andrej

[Thorsten Altenkirch]

That depends on what presentation of Type Theory you are using. Your remarks apply to the extrinsic approach from the last millennium. More recent presentation of Type Theory built in substitution and weakening and use an intrinsic approach which avoids talking about preterms you don’t really care about.

 

https://dl.acm.org/doi/10.1145/2837614.2837638

 

Cheers,

Thorsten

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D66F4584-A005-4F69-8E75-E976E0FF9957%40andrej.com.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

[Jon Sterling]

Indeed, I echo Thorsten's comment — to put it another way, even being able to tell whether these rules are derivable or only admissible is like knowing what an angel's favorite TV show is (in other words, a form of knowledge that cannot be applied toward anything by human beings). At least for structural type theory, there is nothing worth saying that cannot be phrased in a way that does not depend on whether structural rules are admissible or derivable. It may be that admissiblity of structural rules starts to play a role in substructural type theory, however, but this is not my area of expertise.

It is revealing that nobody has proposed a notion of **model** of type theory in which the admissible structural rules do not hold; this would be the necessary form taken by any evidence for the thesis that it is important for structural rules to not be derivable. Absent such a notion of model and evidence that it is at all compelling/useful, we would have to conclude that worrying about admissibility vs. derivability of structural rules in the official presentation of type theory is fundementally misguided.

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com.

[Michael Shulman]

As far as the mathematical study of type theories and their models goes, that may be true.  But I believe that when talking about the way type theories are used in practice, either on paper or in a proof assistant, there is still a difference.

Suppose I am teaching a calculus class, and I define f(x) = x^2 + 1 and I want to evaluate f(3).  I don't write

f(3) = (x^2+1)[3/x] = (x^2)[3/x] + 1[3/x] = 3^2 + 1 = 9 + 1 = 10.

Instead, I jump right to f(3) = 3^2+1, because substitution is an operation that happens immediately in my head, not a computational step analogous to 3^2 = 9.  Similarly, the user of a proof assistant never types or sees substitution as part of the syntax; it is an operation *on* syntax that happens behind the scenes.

Yes, this is a property of a particular *presentation* of a free structure rather than a property of the structure itself, but that doesn't intrinsically make it unimportant.  Groups and group presentations are both important.  Maybe you want to say that "a type theory" refers to the free structure rather than its presentation, but choosing to use words in that way doesn't by itself make "presentations of type theories" (or whatever you call them) less important.  Maybe you want to define an "admissible rule" to be a property that holds in the syntax but fails in some actual models; but that doesn't make "rules that hold in all models and can be made to hold in a particular presentation of the free model without being given explicitly as generating operations/equalities" (or whatever you call them) less important.

I do agree that Andrej's formulation sounds backwards.  In practice (in my experience) one doesn't write the rules down first and then try to figure out what kind of substitution is admissible.  Instead one decides what the substitution rule should be, and *then* (hopefully) works out a way of presenting the syntax to make that substitution rule admissible.  This is particularly tricky for modal type theories, where the categorically "obvious" rules do not admit substitution, and leads to the introduction of split contexts as used in the BFP paper.  I have trouble imagining how I could have written that paper if I had been forced to write explicit substitutions everywhere.  Thorsten and Jon, do you maintain that all the work that's gone into figuring out ways to present modal type theories with "admissible substitution" is meaningless?

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com.

[Tom Hirschowitz]

Only valid for simply-typed languages, so not (yet) contradicting Jon's claim: admissibility of substitution is important in the development of Howe's method for proving that applicative bisimilarity is a congruence. Essentially, the reason is that it provides a simpler induction principle. This is implicit in my recent work with Peio Borthelle and Ambroise Lafont on a categorical framework for Howe's method (e.g., [1]), used as motivation for "A unified treatment of structural definitions on syntax..." [2], and explicitly used (and extended to operations other than substitution) in ongoing work on a generalisation of [1]. 

More generally, I suspect that it is useful in programming language theory, where people tend to work with extrinsic presentations.

[1] https://hal.archives-ouvertes.fr/hal-02966439v6

[2] https://hal.archives-ouvertes.fr/hal-03633933

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpxcTpvy6%2BBS%2B-5yjOjVFkdXFHdmCX0U3Qre2J6t8Lfh_g%40mail.gmail.com.

[Jon Sterling]

Hi Mike, thanks for your comments — regarding modal type theory, please note that there are state of the art general modal type theories that do not employ admissible substitution! MTT is one of them.  

So what was the impact of the search for admissible substitution in the end? The point was absolutely not “to make it admissible because admissibility is important” but rather to discover what the correct equational rules of substitution are in the presence of difficult modal constructs.  The equational theory of substitution in this situation (particularly, how to commute substitutions past the modal forms) is the hard part, and it was this that was the real topic of the study of substitution in modal type theory. This is equally pertinent in the admissible and derivable styles, and the difference between the latter is somewhat less important.

On Nov 17, 2022, at 9:35 PM, Michael Shulman <shu...@sandiego.edu> wrote:



[Thorsten Altenkirch]

Hi Mike,

 

Certainly I would never claim that anybody’s work is meaningless, but I think that understanding and presentation can often by improved by using an appropriate level of abstraction. Often the obvious and naïve choice isn’t the best option. I experience this a lot with students who often use strings to represent syntactic objects like expressions. One of my mantras is “use trees not strings” – I even made a youtube video about it.

 

Now most people accept that we should use trees to represent syntax but many still believe that typing should be extrinsic: ie we first define untyped syntax (using trees) and then a typing relation. In my view they make a similar mistake as my students using strings but on a different level. When I think about type theory I only want to talk about typed objects. Properties like subject reduction, admissibility of substitution etc are just noise caused by using an inappropriate level of abstraction. The essence of what we want to say becomes clear once we overcome these misleading traditions. This becomes even more essential once we deal with dependent types where the overhead often becomes unbearable.

 

Now people we say that we do need to implement and verify programs like type checkers. That is true and it is similar to the need for parsers to translate from strings to trees. My understanding of a parser is that it is the partial inverse of the printing function which translates trees into strings. Similarly a type checker is the partial inverse of a function from intrinsically typed terms to untyped terms. Hence yes we do need to implement the whole toolchain of parsers, typecheckers and when we implement a type system but its specification should happen on the top.

 

I haven’t worked on modal type theories but I suspect that they can and should be presented intrinsically. I refer to Jon’s comments on this topic.

 

Cheers,

Thorsten

[Jon Sterling]

On 17 Nov 2022, at 21:35, Michael Shulman wrote:

> As far as the mathematical study of type theories and their models goes,
> that may be true. But I believe that when talking about the way type
> theories are used in practice, either on paper or in a proof assistant,
> there is still a difference.
>
> Suppose I am teaching a calculus class, and I define f(x) = x^2 + 1 and I
> want to evaluate f(3). I don't write
>
> f(3) = (x^2+1)[3/x] = (x^2)[3/x] + 1[3/x] = 3^2 + 1 = 9 + 1 = 10.
>
> Instead, I jump right to f(3) = 3^2+1, because substitution is an operation
> that happens immediately in my head, not a computational step analogous to
> 3^2 = 9. Similarly, the user of a proof assistant never types or sees
> substitution as part of the syntax; it is an operation *on* syntax that
> happens behind the scenes.

By the way, I find this calculus example to be supremely uncompelling --- not because I am hung up on the fact that it pertains to a presentation, but because mathematics is full of equations that we basically agree not to mention at various times.

It is also not particularly helpful to your point to bring up implementation, where it is extremely common to eschew implicit substitution for explicit substitutions --- or to use a mix of the two... In neither case are the details of this presented to the user, however, because the gender of an angel is not useful information to mere humans who use proof assistants.

Best,
Jon

[Jon Sterling]

Maybe just to put a finer point on it, re: the calculus example (and then I'll try to shut up, I have alreadyspoken too much):

I subscribe to the viewpoint of the HoTT book regarding the practice of informal mathematics (or at least, I subscribe to a version of the viewpoint of the HoTT book which I think at least some of its authors held, including Steve Awodey with whom I have discussed this topic at length in the past). Things like terms, variables, and substitution do not actually arise in informal mathematics: instead, we work *directly* with things that are functions of other things. Thus when doing informal mathematics, if we say "term" we usually mean something that someone might more precisely refer to as an "element". (But let me not open that can of worms!)

In that sense, it would be completely incorrect to say that when doing mathematics and we have a function `f(x) = x^2 + 1`, to evaluate f at 3 we must apply a syntactical operation that recursively walks a syntax tree and replaces a placeholder with 3. The function `f` has the same ontological status as a tree or as a friend or as a piece of stone: it is not a piece of code that tracks a function, rather it is *actually* a function --- in the same way that a stone is not a representation of an object, but an actual object. Thus to evaluate `f(3)`, we use what we know about `f`: namely that it is the function associated to the law that relates any number to the successor of its square.

So in ordinary math, "substitution" tends to be a façon de parler for an operation that is not really syntactical at all but is instead intrinsically constitutive of the informal notion of a "mapping", which exists long before any logicians could attempt to intervene with their syntactical gesticulations... (By the way: truly syntactic substitution also arises *separately* in mathematics, by the way, when thinking about free extensions of algebraic objects (like rings of the form R[x]). But this is a very specialized usage, and if we are being precise we will always distinguish between an element of R[x] and the function it encodes.)

It is true that it is possible to put aside this ontology, and think of mathematical objects in terms of their encodings and then make sure to only speak of syntactical operations that track mathematical operations (e.g. well-typed substitutions, but not ill-typed substitutions). But this is the way of logicians, and it is not really pertinent to the practice of everyday mathematics. Mathematics abstracts over these things, and we try to work "directly" with the objects we are concerned with, regardless of where we fall on the ancient debate of the "real-ness" of these objects.

I fear we have veered off topic from the original question! But I think it would be great if we could put this debate to rest once and for all --- I am constantly amazed to be the syntactician in the room, but having semanticists insist to me that the study of syntax needs raw terms and variables and admissible substitution, etc. If it were needed, then I would certainly have noticed it by now! The world of syntax is far richer than can be described with mere trees or strings, and many of us who study syntax for a living have moved on from that viewpoint. ;-)

Best,
Jon

[andrej...@andrej.com]

I am sorry I started such a long conversation about so little.

Of course one needs to distinguish structures from presentations of structures, which can be done without promoting one's personal preferences as value judgements about the 20th century type theories.

Mike already explained why presentations are important. Thank you.

With kind regards,

Andrej

[Michael Shulman]

On Fri, Nov 18, 2022 at 2:59 AM Jon Sterling <j...@jonmsterling.com> wrote:

Hi Mike, thanks for your comments — regarding modal type theory, please note that there are state of the art general modal type theories that do not employ admissible substitution! MTT is one of them.

Split-context modal type theories can also be presented without admissible substitutions.  Making substitutions explicit is easy; it's making them admissible that's hard.  And as far as I understand it, MTT does satisfy the primary desideratum when making substitutions admissible, namely that all rules have a fully general context in their conclusion.

MTT is also not equivalent to split-context theories, and IMHO is less pleasant to work with in practice.  I believe there should be some way to combine the ideas of the two theories.

By the way, in the followup paper "Modalities and parametric adjoints" by Gratzer, Cavallo, Kavvos, Guatto, and Birkedal (three of whom are also authors of the MTT paper) we read "The admissibility of substitution is a central property of type theory, and indeed of all logic" (section IB).

[Jon Sterling]

The real reason it is central is that making substitution admissible forces you to figure out the equational theory of substitutions (as I said), not the other way around. You are free to consult the other authors of that paper, and I guarantee to you that they will confirm my analysis. Admissibility seems to have been cargo-culted, as people forgot the reason why it was important in the first place.

It is important to recall that the first admissible rule was *cut* in Gentzen's analysis of sequent calculus, but Gentzen's cut-free sequent calculus is eliminating not only substitution but also all computational redexes simultaneously (this is due to the way that sequent calculus is arranged). This kind of admissibility is much more useful than mere admissibility of substitution, because it gives a normal-forms presentation, which (unlike mere admissible substitution) actually has a ton of practical applications (not just deciding equivalence, but also proof search, etc.). So I would characterize my viewpoint as an essentially orthodox one, though the language we use to say these things in 2022 is very different from what was available in the 1930s.

[Michael Shulman]

In general, I feel like we are still talking past each other.  Maybe the problem is that I still haven't found the words that will communicate my point to you.  I was trying to say that it isn't the word "admissible" that matters, but there are real mathematical questions going on whatever words you use to talk about them.

Last summer when I was explaining something about HOTT to a group that I think included you, I used the phrase "admissible" for a certain equality, and we got into a bit of this discussion.  But I felt like we agreed in the end that what I meant was "a rule that doesn't have to get used explicitly by the conversion-checker", and that it was useful to distinguish such things whatever we call them.  That's what I was trying to get at with "rules that hold in all models and can be made to hold in a particular presentation of the free model without being given explicitly as generating operations/equalities".

Similarly, I don't think the implicitness or explicitness of substitutions in the syntax is what's crucial.  If you formulate substitutions implicitly, then the statement you want is that substitution can be defined as an "admissible" operation on the syntax.  If you formulate substitutions explicitly, then the statement you want is that substitutions can be eliminated by a computation.  Isn't this what you mean by "The equational theory of substitution in this situation (particularly, how to commute substitutions past the modal forms) is the hard part"?  You don't just want an equational theory for substitution -- the equations in an equational theory are undirected -- but some kind of rewriting system that tells you how to push a substitution inside the modal forms.  Whether the substitutions are part of the syntax or not isn't the point.

[Jon Sterling]

Hi Mike,

Thanks for this! I think we are getting a lot closer.

I agree with a lot of what you have written here, but maybe not all of it. Let me put it my own way, which is probably similar to what you are getting at --- I see deciding the equational theory of substitution as a special case of deciding the rest of the equational theory. To me, it is basically useless to have a decision procedure for "reducing substitutions but not any other computations (like beta laws, etc.)". To put it another way, if I don't have an algorithm for full normalization (or at least deciding def.eq.), I really couldn't care less if I have an algorithm for reducing substitutions.

Regarding things that exist in the syntax but not necessarily in all models, this is indeed the point of admissibility and it's really really important! It just so happens, however, that substitutions are the main example of something that is both admissible **and** exists in all reasonable models. Even in weak models, we have substitution up to isomorphism --- and no existing solution to the Seely substitution coherence problem works by saying "Well, substitution is admissible, so we don't need it in the model anyway". So the one place to look for an example of substitution-admissibility being important in type theory is actually a non-example.

Not all admissible rules are as useless as this! To the contrary, there ARE very important examples of different admissible rules that must not be derivable unless we wish to degenerate the theory; the main examples that have practical import are injectivity laws, which allow you to deterministically reduce complex equality problems to simpler ones; without these, elaboration and type checking would be essentially impossible (whereas elaboration and typechecking are completely insensitive to the question of whether substitution is admissible). Injectivity of type constructors is the main example of an important admissible rule, but there are many more examples (and I expect, based on our conversations about HOTT over the summer) that there will be a lot more interesting and important ones to discover in the coming years.

So in case it clarifies me, I think admissibility is extremely important and it is, in some sense, the main topic that people like me study. My experience has led me, however, to make a distinction between admissibilities that matter (like injectivity laws) and ones that do not matter at all (like substitution). Nonetheless, there are many roads to the same idea, and the study of type theory and logic in terms of admissible substitutions has been (and remains) an extremely reliable and effective way to obtain well-behaved theories. All I am doing is trying to tease out which parts of this process were essential, and which parts were incidental.

Best,
Jon

[Michael Shulman]

Thanks.  It does sound like we mostly agree.  I would probably argue that even for type theories in development, where we don't yet know that full definitional equality is decidable -- or intrinsically ill-behaved type theories like Lean, or Agda with non-confluent rewrite rules, where definitional equality *isn't* decidable -- there is still value in being able to reduce just substitutions.  But I think that's a relatively minor point.

Maybe we can work out some way to use words so that this underlying agreement is evident.  For instance, can we find a third word to use alongside "admissible" and "derivable" to refer to operations/equalities like substitution and its theory, which hold in all reasonable models, and can be made admissible in some presentations, but more importantly can be eliminated in an equality-checking algorithm?

[Jon Sterling]

On 18 Nov 2022, at 11:56, Michael Shulman wrote:

> Thanks. It does sound like we mostly agree. I would probably argue that
> even for type theories in development, where we don't yet know that full
> definitional equality is decidable -- or intrinsically ill-behaved type
> theories like Lean, or Agda with non-confluent rewrite rules, where
> definitional equality *isn't* decidable -- there is still value in being
> able to reduce just substitutions. But I think that's a relatively minor
> point.
>
> Maybe we can work out some way to use words so that this underlying
> agreement is evident. For instance, can we find a third word to use
> alongside "admissible" and "derivable" to refer to operations/equalities
> like substitution and its theory, which hold in all reasonable models, and
> can be made admissible in some presentations, but more importantly can be
> eliminated in an equality-checking algorithm?
>

Cool, it's a relief to start getting this cleared up! I really agree with you that there is a need for terminology to describe the situation you mention, and maybe even more, there is a need to define this phenomenon...

I wonder if we can think of more concrete examples of this. For instance, in many versions of syntax (like bidirectional ones) we can choose to drop certain annotations because they will be available as part of the flow of information in the elaboration algorithm. Would these be an example of the phenomenon you are describing, or is it something different?

Best,
Jon

[Michael Shulman]

That's an interesting question.  I was thinking of operations and equalities, and annotations are neither of those, but I can see that they're somewhat similar in spirit.  But I find it even more difficult to imagine how to define this phenomenon precisely in a way that would include them...

[Andreas Nuyts]

Hi everyone,

I finally found time to read up on this lengthy conversation.

Jon wrote:

It is revealing that nobody has proposed a notion of **model** of type theory in which the admissible structural rules do not hold; this would be the necessary form taken by any evidence for the thesis that it is important for structural rules to not be derivable.

I think, on the contrary, that such models are not acknowledged as being models, because the language without substitution is in general not really the language of interest. An example of a model disrespecting substitution is the prettyprinter by Allais, Atkey, Chapman, McBride & McKinna (2021):
https://doi.org/10.1017/S0956796820000076
Indeed, substitution is no longer possible after prettyprinting, but all other language constructs are supported. Note that if a substitution operation is unavailable in a model, then the β-rule for functions cannot even be stated in that model, let alone asked to hold. So a model that fails to have a substitution operation necessarily also disrespects the equational theory of a language with such a β-rule. Prettyprinting indeed disrespects βη-equality.

Mike wrote:

MTT is also not equivalent to split-context theories, and IMHO is less pleasant to work with in practice.

I'm reluctant to postulate here that any split-context theory is equivalent to some instance of MTT, but I would be quite surprised if you ever face any practical problems when abandoning a split-context system in favour of MTT. If you're thinking in particular about a system with crisp and non-crisp variables: such a system is implemented by Andrea in agda-flat. At the last Agda meeting, we have been investigating how mature the current modality system in Agda is and how feasible it is to support full MTT. One thing we observed is that - of all the parallel modality systems implemented in Agda - the cohesive one (of which only the flat and non-flat modalities are exposed to the user) is actually the one that adheres to the discipline of MTT (by having a third "squash" modality that effectively removes variables from the context).
Both regarding usability and equivalence, do not be misled by the invasive-looking locks. These locks have two confluent histories:
- there is a history of fitch-style logics,
- there is a history of modal logics with left-division. When implementing Menkar, which was intended as a proof assistant for general multimode systems with left division, I observed at some point that the left division of all modalities in the context actually never needs to be computed and can thus be regarded as a context constructor, rather than as an operation (i.e. admissibility of left division was not required, in none of the senses of the word mentioned so far). Modal Agda does use an eagerly computed left division. These systems with left division are very closely related to dual context systems.

I think usability is hard to judge because there isn't yet good tool support to experiment with. But I believe that it can grow on the user. A lock simply means "we've moved into a modal subterm". The position of the lock in the context is important in order to keep track of which variables were introduced before/after moving into that modal subterm. When using a variable, you just need to make sure that the variable's modal annotation is ≤ the composition of the locks, i.e. the modality of the position where we currently are and where we want to use the variable.

I am happy to discuss this matter further if you have any questions or doubts.

Best regards,
Andreas Nuyts

--

You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com.

[Jon Sterling]

The issue regarding the beta law is kind of spurious: one of course states the beta law using the ADMISSIBLE substitution action. The problem with pretty printing is that it is indeed not satisfying the beta law but this has absolutely nothing to do with substitution — you can still check in the admissible-subst scenario whether the interpretation function respects the beta law on all terms, and in this case it just happens that it doesn’t.

On Dec 1, 2022, at 3:40 PM, Andreas Nuyts <andrea...@gmail.com> wrote:

 Hi everyone,

[Andreas Nuyts]

Right, but when looking for a model that misses a substitution operation and is not contrived, you're not going to find it among the models that try to respect equality, because that isn't even statable in the model. When you drop both the requirement of supporting substitution, and of respecting equality, then your search space has grown enough that prettyprinters can be found in it.

[Andreas Nuyts]

Actually, I think I disagree on a deeper level:
To say that a model (in the sense of algebraic theories) respects the equational theory of a language, does not *only* mean that the evaluation of syntactic programs in that model respects equality. It also means that the evaluation of programs containing subterms that are actually quoted elements from the model, respects equality. (Algebraically speaking, the model should be an Eilenberg-Moore-algebra for the quotiented version of the term monad.) But since *admissible* substitution is undefined for such quoted elements, this cannot be stated (the term monad cannot be quotiented satisfactorily).
So while it's true that "you can still check in the admissible-subst scenario whether the interpretation function respects the beta law on all terms", this is a much weaker property than respecting the equational theory of the language.

But I agree that my statement "Prettyprinting indeed disrespects βη-equality." made it sound as evidence of something, whereas I was merely arguing that it's a drawback that you cannot reasonably complain about if you were looking for a model without substitution in the first place.

[Michael Shulman]

On Thu, Dec 1, 2022 at 6:40 AM Andreas Nuyts <andrea...@gmail.com> wrote:

I think usability is hard to judge because there isn't yet good tool support to experiment with. But I believe that it can grow on the user. A lock simply means "we've moved into a modal subterm". The position of the lock in the context is important in order to keep track of which variables were introduced before/after moving into that modal subterm. When using a variable, you just need to make sure that the variable's modal annotation is ≤ the composition of the locks, i.e. the modality of the position where we currently are and where we want to use the variable.

This is a reasonable point.

I do think, however, that tool support is not necessary to evaluate usability.  A really usable theory should also be usable informally, as in the HoTT Book and my BFP paper.  This is what I have trouble with for locking modal type theories; but it's certainly possible that I could train myself to do it.  It certainly takes some mental training to use split-context modal type theories informally too.

A more serious and mathematical issue is that MTT requires all modalities to be right adjoints, semantically, because you have to have some operation to interpret the locking functors on contexts.  (And FitchTT even requires those left adjoints to themselves be (parametric) right adjoints.)  This seems a serious restriction on the kinds of situations we can model.

One can argue that the process of interpreting a split-context theory involves building a new category of contexts (some generalized kind of comma category, perhaps) that *does* interpret such context operations, and therefore could also interpret MTT.  But we don't have a general theory of this yet.

To be precise, given an arbitrary 2-category M of modes, I would like there to be a corresponding instance of a general modal type theory that can be interpreted in any M-shaped diagram of suitable categories, with all the morphisms of M corresponding to syntactic modalities, and not requiring the existence of any additional adjoints in the semantics.  The LSR fibrational framework achieves this for simple type theories, but I don't think there is any published framework that achieves it for dependent type theories.

Best,

Mike