9
$\begingroup$

I have trouble understanding precisely how dependent type theories are intepreted in categories (in the most simple case, for example in a locally cartesian closed category). I know that a type in context is morally a bundle over the interpretation of the context, that a term in context is a section, etc.. But the actual interpretation seems only to work if the model (a lccc for example) is replaced by a split equivalent version of itself before hand. Let me cite from Martin Hofmann's 1994 paper On the interpretation of Type Theory in Locally Cartesian Closed Categories.

Interpreting dependent type theory in locally cartesian closed categories (lcccs) and more generally in (non split) fibrational models (...) is an intricate problem. The reason is that in order to interpret terms associated with substitution like pairing for $\Sigma$-types or applications for $\Pi$-types one needs a semantical equivalent to syntactic substitution. To clarify the issue (...)

And Martin Hofmann then proceeds to clarify the issue. The paper also contains a solution to the coherence problem, but it makes the interpretation process much harder to understand. I am not able to use the CwA in Hofmann's paper to quickly translate between type theoretic and categorical statements in the way I can for statements written in simply-typed first-order logic.

The paper is from 1994, and people (actual categorical logicians) which I met this week told me that today many effective shortcuts and techniques exist to deal with coherence problems, and that they are often unpublished. They haven't been able to tell me if the specific problem (from the paper I quoted above) is still a problem, and what its most effective solution is, but they encouraged me to ask here. I am afraid of going through a lot of technical details for no good reason.

  • What is the most effective and modern way to deal with coherence problems in the interpretation of dependent type theory? Where can I read about it?

  • Is the paper by Martin Hofmann outdated, or do I just have to try harder?

Improve this question
$\endgroup$
2
  • $\begingroup$ There is an older document: numdam.org/item/DIA_1990__23__43_0.pdf $\endgroup$
    – ice1000 ♦
    Commented Dec 15, 2022 at 19:11
  • $\begingroup$ @ice1000 i think this is explicitly mentioned in Hofmann's article. I am a bit afraid to read old stuff, because if have been told that the techniques have been fastly improved in the last 20 years. :/ $\endgroup$
    – Nico
    Commented Dec 15, 2022 at 19:23

1 Answer 1

Reset to default
5
$\begingroup$

I have commented with Curien's 1990 work on substitution up to isomorphisms, but you said it's too old. Here's a quite new reference, by Lumsdaine and Warren:

https://arxiv.org/abs/1411.1736

It was mentioned in Remark 1.1 on page 5 of https://arxiv.org/abs/1705.07088 which refers to the method as:

(it) replaces any well-behaved comprehension category by a split one in such a way that any “weakly stable” structure possessed by the original becomes “strictly stable” structure in the splitting

I wish that helps :)

Improve this answer
$\endgroup$
4
  • $\begingroup$ It looks nice, thank you! I have just found a super recent text by Emily Riehl from 2022 which also cites this paper. :) $\endgroup$
    – Nico
    Commented Dec 15, 2022 at 20:36
  • 3
    $\begingroup$ I agree, the paper by Lumsdaine and Warren is the most effective and modern approach. In the appendix of arxiv.org/abs/1904.07004 I extended this method to handle universe types. $\endgroup$
    – Mike Shulman
    Commented Dec 16, 2022 at 4:31
  • $\begingroup$ @MikeShulman did you write that paragraph I quoted? Or is it Lumsdaine? Just curious :) $\endgroup$
    – ice1000 ♦
    Commented Dec 16, 2022 at 5:18
  • 1
    $\begingroup$ That's so long ago, I don't remember. $\endgroup$
    – Mike Shulman
    Commented Dec 16, 2022 at 17:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.