<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div> Hello,</div><div><br></div><div> Martin-Lof type theory has a fixed collection of inductive types: typically Nat, List A, W A B and Id A a1 a2 with a collection</div><div>of universes Set:Set1:Set2:....</div><div><br></div><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><br></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></body></html>