<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>There's also a perspective on this that one can take from the Elims. For P the elim should be something like</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span>Elim-P : (A : Set) (M : P A -> Set)</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span> -> (base : (a : A) -> P (pack a))</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif;
background-color: transparent; font-style: normal; "><span> -> (p : P A) -> M p</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span>whereas for N</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span>Elim-N : (A : Set) (M : (B : Set) -> N B -> Set)</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif;
background-color: transparent; font-style: normal; "><span> -> (base : (B : Set) -> (b : B) -> M B (packn b))</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span> -> (n : N A) -> M A n</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span>The second one is obviously different. The motive and base cases are parametric on the value stored in the packing type, which will highly restrict their values. This just falls out of the parameter/index distinction formally: motives and inductive
subproofs musthave as arguments everything the functors/constructors have as arguments, plus some additional stuff (additional recursive proofs).</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div>- darryl<br></div> <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "> <div dir="ltr"> <font size="2" face="Arial"> <hr size="1"> <b><span style="font-weight:bold;">From:</span></b> Andreas Abel <andreas.abel@ifi.lmu.de><br> <b><span style="font-weight: bold;">To:</span></b> Jan Malakhovski <oxij@oxij.org> <br><b><span style="font-weight: bold;">Cc:</span></b> agda@lists.chalmers.se <br> <b><span style="font-weight: bold;">Sent:</span></b> Friday, January 25, 2013 12:03 PM<br> <b><span
style="font-weight: bold;">Subject:</span></b> Re: [Agda] Datatype parameters and indices<br> </font> </div> <br>
[This is a candidate for a FAQ.]<br><br>That P passes but N not is an artefact of data type declarations.<br><br>Parameters are actually *absent* from constructors, so pack is really<br><br> pack : ?A -> P ?A<br><br>for ?A to be instantiated according to the context where pack occurs. <br>The syntax<br><br> pack {A = Nat} zero<br><br>is valid, but the instantiation of parameter of A to Nat should only <br>regarded as a hint to the type checker, and not an actual setting of an <br>argument of pack.<br><br>In contrast, packn actually expects a first argument of type Set, which <br>is too big for type N : ... -> Set, so Agda complains.<br><br>Hope that helps,<br><br>Andreas<br><br>On 25.01.13 12:05 AM, Jan Malakhovski wrote:<br>> Hello everyone,<br>><br>> A question that doesn't leave me for a while (like a year or so).<br>><br>> If I remember right, a dozen of versions ago the following code did type
check.<br>><br>> ~~~~<br>> data P (A : Set) : Set where<br>> pack : A → P A<br>><br>> data N : Set → Set where<br>> packn : {A : Set} → A → N A<br>> ~~~~<br>><br>> Now it complains:<br>><br>> ~~~~<br>> The type of the constructor does not fit in the sort of the<br>> datatype, since Set₁ is not less or equal than Set<br>> when checking the constructor packn in the declaration of N<br>> ~~~~<br>><br>> I can't help but wonder about a justification for this.<br>> It is said that parameters transform into constructors' implicit arguments, but the code above makes me think that, strictly speaking, it isn't the case.<br>><br>> Best regards,<br>> Jan<br>> _______________________________________________<br>> Agda mailing list<br>> <a ymailto="mailto:Agda@lists.chalmers.se"
href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>><br><br>-- <br>Andreas Abel <>< Du bist der geliebte Mensch.<br><br>Theoretical Computer Science, University of Munich<br>Oettingenstr. 67, D-80538 Munich, GERMANY<br><br><a ymailto="mailto:andreas.abel@ifi.lmu.de" href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a><br>http://www2.tcs.ifi.lmu.de/~abel/<br>_______________________________________________<br>Agda mailing list<br><a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br><br> </div> </div> </div></body></html>