<div>Hi all,</div><div><br></div><div>The following fails the positivity check, but it seems to me that it could be allowed to pass without introducing inconsistency. Thoughts?</div><div><br></div><div><div>Regards,</div><div>
Andrew</div></div><div><br></div><div><div>open import Data.Nat</div><div>open import Data.Fin</div><div><br></div><div>data functor (n : ℕ) : Set where</div><div> ▹ : (X : Fin n) -&gt; functor n</div><div> μ : (F : functor (suc n)) -&gt; functor n</div>
<div> _⇒_ : (A : functor zero) (F : functor n) -&gt; functor n</div><div><br></div><div>env : ℕ -&gt; Set₁</div><div>env n = ∀ (X : Fin n) -&gt; Set</div><div><br></div><div>extend : ∀ {n} -&gt; env n -&gt; Set -&gt; env (suc n)</div>
<div>extend ρ A zero = A</div><div>extend ρ A (suc i) = ρ i</div><div><br></div><div>mutual</div><div> data μ&#39; {n} (F : functor (suc n)) (ρ : env n) : Set where</div><div>  ⟨_⟩ : ⟦ F ⟧ (extend ρ (μ&#39; F ρ)) -&gt; μ&#39; F ρ</div>
<div><br></div><div> ⟦_⟧ : ∀ {n} -&gt; functor n -&gt; (ρ : env n) -&gt; Set</div><div> ⟦ ▹ X ⟧ ρ = ρ X</div><div> ⟦ μ F ⟧ ρ = μ&#39; F ρ</div><div> ⟦ A ⇒ F ⟧ ρ = ⟦ A ⟧ (λ ()) → ⟦ F ⟧ ρ</div></div><div><br></div>