<div dir="ltr"><div>I think Agda checks for each function definition whether it is (strictly) positive in each of its arguments. The 'depth' of this check is not limited AFAICT, but it is determined at the definition site of the function, not at the use site. I've seen this used quite often for universe constructions such as in your example.<br></div><div><br></div><div>-- Jesper<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jul 19, 2018 at 1:15 PM, Neel Krishnaswami <span dir="ltr"><<a href="mailto:nk480@cl.cam.ac.uk" target="_blank">nk480@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello,<br>
<br>
I wrote the following bit of code, to experiment with generic programming.<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
data _×_ (A B : Set) : Set where<br>
   _,_ : A → B → A × B<br>
<br>
<br>
data _+_ (A B : Set) : Set where<br>
  inl : A → A + B<br>
  inr : B → A + B<br>
<br>
<br>
data Poly : Set₁ where<br>
  K : Set → Poly<br>
  _⊗_ : Poly → Poly → Poly<br>
  _⊕_ : Poly → Poly → Poly<br>
  Id : Poly<br>
<br>
[_] : Poly → Set → Set<br>
[ K X ] A = X<br>
[ p ⊗ q ] A = [ p ] A × [ q ] A<br>
[ p ⊕ q ] A = [ p ] A + [ q ] A<br>
[ Id ] A = A<br>
<br>
data μ (F : Poly) : Set where<br>
  into : [ F ] (μ F) → μ F<br>
</blockquote>
and Agda accepted the declaration of μ. I was surprised by this -- did Agda look at the body of the definition of [_] to decide that every  recursive occurrence was  positive? If so, how deeply does it look?<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
Neel Krishnaswami<br>
<a href="mailto:nk480@cl.cam.ac.uk" target="_blank">nk480@cl.cam.ac.uk</a><br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>