<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div> One other difference between Agda and Martin-Lof type theory, which seems relevant here, is that if one uses only the </div><div>elimination rule over Id, it does not seem possible to show that the set constructor I is injective. At least, the proof</div><div><br></div><div><div><font size="2" face="Arial">data I : (Set -> Set) -> Set where</font></div><div> </div><div><font size="2" face="Arial"> Iinj : ∀ { x y : Set -> Set } -> Eq1 (I x) (I y) -> Eq1 x y <br> Iinj refleq1 = refleq1</font></div><div> </div><div>uses some operations (unification of I x and I y and hence of x and y) that apparently go beyond the elimination </div><div>rule for the Id type. </div></div></div></blockquote><div><br></div><div>It isn't even possible to prove that List : Set -> Set is injective (e.g. one can use W-types to define List), I think. The reason is that one can identify sets upto isomorphism (this can be justified by the groupoid model) and List is not injective upto isomorphism. However, if we add universe elimination then we should be able to show injectivity for List.</div><div><br></div><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div> Can one then conjecture that in Martin-Lof type theory extended with a data type</div><div><br></div><div> I F : Set (F: Set -> Set)</div><div><br></div><div>(which is injective for -conversion-) one cannot prove the injectivity of I, in the sense</div><div>that one cannot prove</div><div><br></div><div> Id Set (I F) (I G) -> Id (Set->Set) F G</div><div><br></div><div>and that this system is consistent with classical logic? (This seems possible via the set theoretic model</div><div>by interpreting I F to be always the empty set.)</div><div><br></div><div> Best regards,</div><div><br></div></div><div> Thierry </div><div><br></div><div>PS: For proving the injectivity of S : Nat -> Nat using only the elimination rule over Id, one can for instance define a function</div><div><div><br></div><div> pred : Nat -> Nat</div><div><br></div><div> pred (S x) = x</div><div> pred 0 = 0</div></div><div><br></div><div>and then prove Id Nat (S x) (S y) -> Id Nat x y using this function pred.</div><div>Even if we consider I as a constructor for building elements of the type Set, this type Set is not</div><div>"closed" as the type Nat (only constructors 0 and S) and one cannot define functions by case on the type Set.</div><div><br></div><div><br></div><div>On Jan 7, 2010, at 11:01 AM, Chung Kil Hur wrote:</div><div><br class="Apple-interchange-newline"><blockquote type="cite"><div>Dear Dan,<br><br>Thanks for your answer.<br>Ok, Agda is a kind of constructive math assuming an anti-classical axiom.<br><br>Then, I have a few more questions.<br><br>Does the orginal Martin-Lof type theory also assume the injectivity of inductive type constructors ? or Agda added it later?<br>If the latter is the case, has the consistency of Agda been shown?<br>Or, is there a set-theoretic model of Agda ?<br><br>Thanks,<br>Chung-Kil Hur<br></div></blockquote></div><br></div>_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>https://lists.chalmers.se/mailman/listinfo/agda<br></blockquote></div><br></body></html>