Hi Brandon<br><br>I'm sorry to say my only motivation was to see what kinds of declaration are possible and whether it matches what people generally have in mind should be.<br><br>For example, this works<br> bar : ℕ → Set1<br>
bar n = ℕ → Set<br> data foo (x : ℕ) : (n : ℕ) → bar n where<br> baz : foo x x (suc x)<br><br>But I wonder if it's only accidental that it works, since if I were to make the definition of bar any more complicated (even if it was ultimately just a constant function) I'd run into similar problems. That is, with<br>
bar zero = ℕ → Set<br> bar (suc _) = ℕ → Set<br>I get the error<br> bar x != Set of type Set₁<br> when checking the definition of foo<br><div class="gmail_quote"><br>On Wed, Feb 22, 2012 at 8:59 PM, Brandon Moore <span dir="ltr"><<a href="mailto:brandon_m_moore@yahoo.com">brandon_m_moore@yahoo.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div style="font-size:12pt;font-family:times new roman,new york,times,serif"><div style="font-family:'times new roman','new york',times,serif;font-size:12pt">
Hello Ramana</div><div style="font-family:'times new roman','new york',times,serif;font-size:12pt"><br></div><div style="font-family:'times new roman','new york',times,serif;font-size:12pt">
Could you motivate your definition a bit more?</div><div style="font-family:'times new roman','new york',times,serif;font-size:12pt">I don't have much idea what it should mean.</div><div style="font-family:'times new roman','new york',times,serif;font-size:12pt">
It seems very similar to a this definition,</div><div style="font-family:'times new roman','new york',times,serif;font-size:12pt">which I am not surprised to see rejected</div><div style="font-family:'times new roman','new york',times,serif;font-size:12pt">
<br></div><div style="font-family:'times new roman','new york',times,serif;font-size:12pt"><span style="font-size:12pt">data foo : (y : Bool) -> Bool where</span><br></div><div style="font-family:'times new roman','new york',times,serif;font-size:12pt">
-- no constructors</div><div style="font-family:'times new roman','new york',times,serif;font-size:12pt"><br></div><div style="font-family:'times new roman','new york',times,serif;font-size:12pt">
If the idea is to have an inductive family where some indices</div><div style="font-family:'times new roman','new york',times,serif;font-size:12pt">live at different levels, you might compare to this definition:</div>
<div style="font-family:'times new roman','new york',times,serif;font-size:12pt"><br></div><div><div>data foo : (y : Bool) → Set (if y then zero else suc zero) where</div><div> bar : foo true</div><div><br>
</div><div>which produces
a more straightforward error message</div><div><br></div></div><div><div>home/brandon/test/test.agda:5,6-9</div><div>The sort of foo cannot depend on its indices in the type (y : Bool)</div><div>→ Set (if y then zero else suc zero)</div>
<div class="im"><div>when checking the definition of foo</div><div><br></div></div><span class="HOEnZb"><font color="#888888"><div>Brandon</div></font></span></div> </div></div></blockquote></div><br>