5
$\begingroup$

I am reading through the papers, "Observational equality: Now for good" (${TT}^{obs}$) and "Impredicative Observational Equality" (${CC}^{obs}$) by Pujet and Tabareau, and I am trying to understand a couple of distinctions here, regarding injectivity. As far as I understand these are the only 2 extensions of intensional Martin-Löf type theory with open universes, normalization, function extensionality, UIP and decidable type-checking. In $CC^{obs}$ there is a remark that the added impredicativity should make the language a good internal language of toposes. While in $TT^{obs}$ it is remarked that injectivity somewhat strays away from desired semantics in terms of Grothendieck universes.

On the other hand from what I have seen on Agda issue tracker, some form of injectivity is anti-classical.

Is the injectivity of ${TT}^{obs}/{CC}^{obs}$ also anti-classical? When would it be desirable to have a good internal language of toposes without injectivity, but with the other good features of these theories? Of course the second question has a trivial answer if the answer to first one is positive.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
5
$\begingroup$

Is the injectivity of 𝑇𝑇𝑜𝑏𝑠/𝐶𝐶𝑜𝑏𝑠 also anti-classical?

It isn't.

  • The setoid model in the TTobs paper supports LEM (meaning that every setoid is empty or nonempty).
  • This note explains that we can inductively define universes with injective type formers in any Gröthendieck topos.

As far as I see, the Agda proofs of anti-classicality always use some failure of type codes to be inductive. This means breaking positivity or sizing restrictions. For example, the following type former has no semantics in the above references:

data T (F : U -> U) : U

Because it's not positive when read as an inductive rule:

data U 
   ...
   Tcode : (U -> U) -> U
   ...

In contrast, List : U -> U is strictly positive and thus fine, even though we have a large type parameter in the rule. It's also fine to have T : (U i -> U i) -> U (i + 1).

So, the sizing of type formers in the presence of injectivity is a bit subtle, because it's not enough to look at sizes of parameters and indices. We have to additionally bump sizes when a type former is not strictly positive.

Improve this answer
$\endgroup$
4
  • $\begingroup$ In your example, though, the issue is not with strict positivity, but with the size of the parameter not counting towards the size of the whole inductive, right? That is, U -> U cannot be of type U, so if datatypes are constrained to be larger than their parameters then only your T : (U i -> U i) -> U (i+1) is valid? $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented May 19, 2023 at 8:53
  • $\begingroup$ More generally, I though the issue with injectivity of type constructors is that in Coq or Agda, the size of parameters does not count towards the size of the inductive type. I don't know how exactly Agda does it, but afaik in Coq only the size of constructor arguments counts towards the size of the datatype (and the size of indices if the indices-matter flag is used, which was I think added when HoTT people bumped into similar issues). So in particular a datatype with no constructors will always be small, which feels like a form of resizing, and seems dubious with types-as-codes. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented May 19, 2023 at 8:57
  • $\begingroup$ @MevenLennon-Bertrand U and U -> U are both in U1. But List (A : U) : U is fine while T (F : U -> U) : U isn't; the difference between the two is positivity. If we want general injectivity for all type formers, indices-matter is not enough, we need to check positivity for parameters (incl. those unused in constructors). I've heard though from Loic Pujet that the current OTT implementation strategy in Coq is to not have general injectivity, we only get enough injectivity so that constructor coercions can be computed. $\endgroup$
    – András Kovács
    Commented May 19, 2023 at 12:11
  • $\begingroup$ You are right, indeed, my bad, there is a difference between List and F here. So I guess for general injectivity you'd need to make basically any type constructor large, which is somewhat too disruptive and you'd need to go for a restricted for instead, as you suggest. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented May 19, 2023 at 14:43

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