0
$\begingroup$

A category $\mathrm{Ch}(\mathbf{Ab})$ of chain complex has a model category structure, which makes the category to interpret dependent type theory.

E.g. a term of a type $A$ is interpreted as an arrow from a terminal object to $A$.

However, there is no nontrivial such arrow because terminal and initial objects coincide in $\mathrm{Ch}(\mathbf{Ab})$. Doesn't this fact make the interpretation trivial?

Improve this question
$\endgroup$
5
  • 5
    $\begingroup$ I think you have confused different usages of the word “model” here. $\endgroup$
    – Zhen Lin
    Commented Aug 26, 2020 at 9:50
  • $\begingroup$ Could you please make it precise? I think model categories can interpret Martin Löf type theory with identity types. (By "dependent type theory", I meant Martin Löf type theory with identity types.) Is my understanding correct? $\endgroup$
    – Yuta
    Commented Aug 26, 2020 at 21:19
  • $\begingroup$ That is incorrect, or at least very imprecise. You need a lot more than just a model structure to interpret dependent type theory. For instance you need a locally cartesian closed category, or something very close, to interpret $\Pi$-types. $\endgroup$
    – Zhen Lin
    Commented Aug 26, 2020 at 22:11
  • $\begingroup$ By "Martin Löf type theory with identity types", I was thinking of the fragment without Π and Σ. Then by Thm 3.1. of arxiv.org/pdf/0709.0248.pdf, I think finitely completeness and weak factorization system is enough to model Martin Löf type theory with identity types. Or isn't the stability condition satisfied? $\endgroup$
    – Yuta
    Commented Aug 27, 2020 at 0:31
  • $\begingroup$ I suppose if you omit $\Pi$ and $\Sigma$ and $0$ and $+$ you may have a model, yes. But that’s not a very expressive fragment of type theory. $\endgroup$
    – Zhen Lin
    Commented Aug 27, 2020 at 0:56

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .