1
$\begingroup$

Since 2010/01/07, when the Anti-classicality of Agda was proved by Chung-Kil Hur, Agda's --injective-type-constructors is separated from the main branch of Agda (making the main branch avoid Anti-classical) and stabilized to its current state.

This flag is marked as "possibly inconsistent" and there is a lack of further research and disclosure of the rules.

If this flag enjoys canonicity, it would be helpful for studying its consistency.

$\endgroup$
8
  • $\begingroup$ You should try asking your question in a manner that sounds less than an attack on those working on/in Agda. Also, have you done any research on the question? $\endgroup$ Sep 6, 2022 at 8:22
  • $\begingroup$ @MevenLennon-Bertrand emmmm...I'm sorry, but I don't know what I said wrong?" possibly inconsistent" is clearly stated in Agda's documentation. $\endgroup$ Sep 6, 2022 at 10:05
  • $\begingroup$ @MevenLennon-Bertrand I don't have the ability to reduce the rules for --injective-type-constructors from Agda's source code. But I don't think I should be blamed for this, there are quite a few papers that mention that "no specification file for Agda's rules was found" $\endgroup$ Sep 6, 2022 at 10:09
  • $\begingroup$ Your original version sounded very close to "Nobody seems to care that Agda is inconsistent", which to me (and probably the other downvoters too) sounds like an unnecessary attack on people working hard on Agda’s consistency. But your new version is much better! You give some previous research, and (to me) do not sound like an unnecessary attack on the Agda community anymore. Cheers! $\endgroup$ Sep 6, 2022 at 11:36
  • 1
    $\begingroup$ Voted to close this question for lack of context. It may be reopened if question is improved. For example, you could provide context for the work you cite (Is this a thesis or article? What does it say?), and you could elaborate on what you mean by 'canonical form of Agda's injectivity of type constructors'. $\endgroup$
    – Couchy
    Sep 7, 2022 at 4:15

1 Answer 1

2
$\begingroup$

If you look at models where types are built using an inductive-recursive universe of codes, then you get injectivity/discrimination of type constructors as for any inductive type. In a slightly different context, that of observational equality, injectivity/discrimination of type constructors is true by computation. These might not apply to Agda per se, but are at least hints as to why this flag seems reasonable.

$\endgroup$
5
  • $\begingroup$ I believe MLTT + Injectivity of type constructors has canonical form, but I still can't understand why Agda doesn't put it in --safe? Just because it is anti-classical? If there is no better answer after some time, I will accept this answer. $\endgroup$ Sep 6, 2022 at 10:19
  • 2
    $\begingroup$ I am not an Agda expert, but the --safe keyword seems to be reserved to well-understood and "standard" features. While injectivity of type constructors seems consistent, I do not think it fulfils these criteria. Moreover, it is a strong commitment, which excludes a lot of reasonable axioms: it is not only anti-classical, but also contradicts univalence… All in all, these seem to me like enough reasons to not flag this feature as safe. $\endgroup$ Sep 6, 2022 at 11:52
  • 3
    $\begingroup$ Injectivity of type constructors lets us exhibit a non-splitting monomorphism. This is essentially the proof that Mahlo universes (which Agda has) cannot have eliminators. Constructor injectivity is a similar axiom that is barely weak enough to not be outright inconsistent. At least, that's as far as anyone knows; I wouldn't bet anything substantial on it. This is also sort of the root of some of its other conflicts (like anti-classicality and anti-impredicativity). $\endgroup$
    – Dan Doel
    Sep 6, 2022 at 18:39
  • $\begingroup$ Interesting, I did not know about all this! Do you know where I can read more (if that place exists)? $\endgroup$ Sep 7, 2022 at 9:14
  • 3
    $\begingroup$ I read the argument about Mahlo universes in Setzer's "Proof Theory of Martin-löf Type Theory." It cites Palmgren's "On Universes in Type Theory" as the original source. The expected eliminator lets you write the splitting by cases. For impredicativity, it is the usual trick of defining something by quantifying over all things with the desired property, like $S(X) = ΠZ. G(Z) = X → Z$. This is isomorphic to a splitting via injectivity of $G$ and the Yoneda lemma. Excluded middle makes propositions impredicative and small, and some anti-classical results reduce just to that. This seems like one. $\endgroup$
    – Dan Doel
    Sep 7, 2022 at 18:38

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.