Ah, I see; it&#39;s more subtle than I initially thought. I initially thought it was just a matter of observing that rho wasn&#39;t used to the left of the arrow. Thanks. I see now it&#39;s exactly as you said that it would need to see that the occurrences of mu&#39; to the left of the arrow are in some way &quot;different&quot; mus.<div>
<br></div><div>Regards,</div><div>Andrew<br><div><br></div><div><div><div class="gmail_quote">On Tue, Nov 13, 2012 at 2:27 PM, Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Yes, but please do not expect Agda to see this... :)<br>
<br>
Basically, what you are saying is that the mu&#39; in the second clause of [[ ... ]] is never the &quot;same&quot; mu&#39; you started with in the constructor of mu&#39;.  But can you make this formal by a static analysis?<br>


<br>
Cheers,<br>
Andreas<div><div><br>
<br>
On 13.11.2012 20:15, Andrew Cave wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div>
Hi all,<br>
<br>
The following fails the positivity check, but it seems to me that it<br>
could be allowed to pass without introducing inconsistency. Thoughts?<br>
<br>
Regards,<br>
Andrew<br>
<br>
open import Data.Nat<br>
open import Data.Fin<br>
<br>
data functor (n : ℕ) : Set where<br>
  ▹ : (X : Fin n) -&gt; functor n<br>
  μ : (F : functor (suc n)) -&gt; functor n<br>
  _⇒_ : (A : functor zero) (F : functor n) -&gt; functor n<br>
<br>
env : ℕ -&gt; Set₁<br>
env n = ∀ (X : Fin n) -&gt; Set<br>
<br>
extend : ∀ {n} -&gt; env n -&gt; Set -&gt; env (suc n)<br>
extend ρ A zero = A<br>
extend ρ A (suc i) = ρ i<br>
<br>
mutual<br>
  data μ&#39; {n} (F : functor (suc n)) (ρ : env n) : Set where<br>
   ⟨_⟩ : ⟦ F ⟧ (extend ρ (μ&#39; F ρ)) -&gt; μ&#39; F ρ<br>
<br>
  ⟦_⟧ : ∀ {n} -&gt; functor n -&gt; (ρ : env n) -&gt; Set<br>
  ⟦ ▹ X ⟧ ρ = ρ X<br>
  ⟦ μ F ⟧ ρ = μ&#39; F ρ<br>
  ⟦ A ⇒ F ⟧ ρ = ⟦ A ⟧ (λ ()) → ⟦ F ⟧ ρ<br>
<br>
<br>
<br></div></div>
______________________________<u></u>_________________<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" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br><span><font color="#888888">
</font></span></blockquote><span><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</font></span></blockquote></div><br></div>
</div></div>