<p>Here is an example exploiting positivity of an index to prove false:</p>
<pre><code>module Whatever where

open import Level using (Level)
open import Relation.Binary.PropositionalEquality
open import Data.Empty

variable
  ℓ : Level
  A B : Set ℓ

data _≅_ (A : Set ℓ) : Set ℓ → Set ℓ where
  trefl : A ≅ A

Subst : (P : Set ℓ → Set ℓ) → A ≅ B → P A → P B
Subst P trefl PA = PA

data U : Set where
  d : U

El : U → Set
data D : Set

El d = D

{-# NO_POSITIVITY_CHECK #-}
data D where
  neg : ∀(c : U) → El c ≅ D → (El c → ⊥) → D

¬D : D → ⊥
¬D v@(neg c eq f) = Subst (λ D → D → ⊥) eq f v

spin : ⊥
spin = ¬D (neg d trefl ¬D)
</code></pre>
<p>Technically it also makes use of the fact that induction-recursion can create small universes, and that type equality can be smaller than general equality applied to the universe, but those are otherwise not really problematic to my knowledge (Coq has impredicative equality anyway, I believe). It's possible the simultaneous definition could be eliminated, too, but it's not straight forward, at least.</p>
<hr />
<p>Edit: I asked around about your first bullet point. It was pointed out to me that there is essentially nothing special about a nested type that is nested in itself. <a href="https://gallais.github.io/blog/non-regular-parameters.html" rel="nofollow noreferrer">This article</a> shows how to use a non-native translation of nested types into indexed types of equivalent size. When you do that, as long as nesting is strictly positive, it's not difficult to apply the translation to a strictly positive indexed type.</p>
<p>Or for instance, the example translation I was shown uses a nested <span class="math-container">$ℕ$</span> parameter instead of self-nesting:</p>
<pre><code>data D' (A : Set) (n : ℕ) : Set where
  c : D' A (suc n) → D' A n
  t : (case n of λ where
         zero → A
         (suc m) → D' A m
      ) → D' A n
</code></pre>
<p>Where I added the <code>t</code> constructor to make something actually use <code>A</code>, and <code>D A</code> is meant to be equivalent to <code>D' A 0</code>. I think another way to write this would be:</p>
<pre><code>data D' (A : Set) : ℕ → Set where
  c : D' A (suc n) → D' A n
  t : D' A n → D' A (suc n)
  t' : A → D' A zero
</code></pre>
<p>Essentially, the <span class="math-container">$ℕ$</span> is a tree tracking how much nesting we need to unfold.</p>

CC BY-SA 4.0
2021-01-06T21:11:19.373Z
I have a suspicion that since `(El c → ⊥)` reduces to `(D → ⊥)`, the definition might not pass plain positivity (as opposed to merely violating nested positivity), but there doesn't seem to be a way to turn off *only* nested positivity in Agda anyway.
ionchy
CC BY-SA 4.0
2021-01-06T21:23:35.297Z
`El c` does not reduce to `D`. `El c` is a neutral term, because `c` is a variable. In my example, `d` is the only value for `c` to take, but I could easily add more.
Dan Doel
CC BY-SA 4.0
2021-01-06T19:15:21.303Z
2021-01-07T00:23:44.073Z
2021-01-07T00:23:44.073Z
Dan Doel
<p>I'm going to partially answer point 2 here. If you allowed the inductive type to appear even strictly positively in another inductive's index, <em>and you had impredicative Prop</em>, you could derive an inconsistency through an equality type with a type that <em>does</em> occur negatively, as Dan stated in the comments. Here's an example in Coq, with the inductive type stated as axioms.</p>
<pre><code>Inductive Equal (A: Prop) : Prop -&gt; Prop :=
| refl : Equal A A.

(** These axioms correspond to the following inductive definition:
 *  Inductive D : Prop :=
 *  | C : forall (E: Prop) (p: Equal D E), (E -&gt; False) -&gt; D. *)
Axiom D : Prop.
Axiom introD: forall (E: Prop) (p: Equal D E), (E -&gt; False) -&gt; D.
Axiom matchD: forall (E: Prop) (p: Equal D E), D -&gt; (E -&gt; False).

Definition DnotD (d: D): (D -&gt; False) := matchD D (refl D) d.
Definition notD (d: D): False := (DnotD d) d.
Definition isD: D := introD D (refl D) notD.
Definition bottom: False := notD isD.
</code></pre>
<p>I'm not sure whether you can do the same when you only have predicative universes without resorting to universe polymorphism tricks or the like.</p>

CC BY-SA 4.0
2021-01-06T19:18:24.747Z
2021-01-06T19:18:24.747Z
ionchy
<p>I'm looking at the nested positivity conditions for inductive types stated in the <a href="https://coq.inria.fr/distrib/current/refman/language/core/inductive.html#nested-positivity" rel="nofollow noreferrer">Coq manual</a>. First off, are there any other references (not necessarily for Coq, but in dependent type theories generally) for the nested positivity conditions and how they come about? I've found older papers like Dybjer's <em>Inductive Families</em> and Coquand and Paulin's <em>Inductively Defined Types</em>, but I believe these only mention the strict positivity condition, and newer papers like the pCuIC one and <em>A Comprehensible Guide to CIC</em> don't mention nested positivity either.</p>
<p>Now, I'm trying to gain an intuitive understanding of why nested positivity is required. In essence, nested positivity states that when defining a constructor C for some inductive type <span class="math-container">$D$</span>, if the type of an argument to <span class="math-container">$C$</span> is something like <span class="math-container">$I ~ \vec{p} ~ \vec{t}$</span>, then <span class="math-container">$D$</span> can only appear strictly positively in <span class="math-container">$\vec{p}$</span>, and only if <span class="math-container">$I \neq D$</span>. I understand that allowing <span class="math-container">$D$</span> in negative positions of <span class="math-container">$\vec{p}$</span> basically allows for proofs of <span class="math-container">$(D \to \bot) \to \bot$</span>, and allowing <span class="math-container">$D$</span> in other positive positions essentially allows for double negation elimination (and some inconsistency stuff with impredicative Prop). What I don't understand are these:</p>
<ul>
<li><p>Why can't <span class="math-container">$D$</span> appear strictly positively in <span class="math-container">$\vec{p}$</span> if <span class="math-container">$I = D$</span> (either as constructor argument or return type)? For instance, for a constructor <span class="math-container">$C$</span> of an inductive type <span class="math-container">$D ~ (A: \textrm{Type}): \textrm{Type}$</span> (with <span class="math-container">$A$</span> as the sole parameter), why is <span class="math-container">$C: D ~ (D ~ A) \to D ~ A$</span> disallowed?</p>
<p>EDIT: Not only is this accepted in Agda 2.6.1.2, <span class="math-container">$C: D ~ (D ~ A \to \bot) \to D ~ A$</span> is also accepted, which seems suspicious to me.</p>
</li>
<li><p>Why can <span class="math-container">$D$</span> otherwise appear strictly positively in the <em>parameters</em> <span class="math-container">$\vec{p}$</span>, but not in the <em>indices</em> <span class="math-container">$\vec{t}$</span>? <del>Consider for instance the (rather silly) constructor <span class="math-container">$C: (D =_{\textrm{Type}} D) \to D$</span> for the inductive type <span class="math-container">$D: \textrm{Type}$</span>, where <span class="math-container">$=$</span> is the usual equality type.</del></p>
<p>EDIT: It turns out this doesn't type check in Agda for unrelated universe level reasons, so consider instead the following which Agda rejects for positivity reasons:</p>
<pre><code>data Box : (A : Set) → Set where
  box : (A : Set) → Box A

data D : Set where
  C : Box D → D
</code></pre>
<p>This <em>is</em> accepted by Agda if <code>A</code> is instead a parameter, as expected from the nested positivity rules.</p>
</li>
</ul>
<p>I'm particularly interested in finding examples where violating nested positivity conditions (specifically these two I've listed) causes inconsistencies and proofs of <span class="math-container">$\bot$</span>, which personally would be easier to understand than arguments about monotonicity.</p>

CC BY-SA 4.0
2021-01-04T14:30:52.333Z
Probably useful to mention https://cstheory.stackexchange.com/questions/18797/why-do-agda-and-coq-disagree-on-strict-positivity
cody
CC BY-SA 4.0
2021-01-06T06:25:28.140Z
In general, it would (I believe) be possible to encode non strictly positive types by proxy if indices were considered strictly positive. Like `neg : C = D -> ...` where `C` occurs negatively elsewhere, but is not subject to the check. I'm not certain why your particular example isn't accepted by Agda, because it has analysis for detecting that `X` is actually like a parameter (that's why `Box` is well-sized). I guess it doesn't take that into account with respect to positivity checking.
Dan Doel
CC BY-SA 4.0
2021-01-06T12:00:21.580Z
@DanDoel So I tried to construct an example and this was about as far as I could get:

`data _≡_ (A : Set) : Set → Set where refl : A ≡ A`, 

`data D : Set where neg : (E : Set) → (E → ⊥) → D ≡ E → D`. 

This isn't accepted but it's because `neg` needs to be in the same universe as `D`, but `E: Set` means that it's actually in `Set₁`. 

Interestingly, with the constructor `c: D ≡ ⊤ → D`, Agda complains about `D` not being strictly positive in `≡`, but not if I change the type of `refl` to `A ≡ ⊤`, so it seems Agda doesn't merely check whether it's a parameter or index.
ionchy
CC BY-SA 4.0
2021-01-06T12:03:25.023Z
It also turns out that I can't use code blocks in comments :/
ionchy
CC BY-SA 4.0
2021-01-06T22:11:05.310Z
FYI, in the example in your first bullet point, if you add a constructor that actually uses $A$ in the dangerous example, Agda will complain that $D$ is no longer strictly positive. So it is just noticing that your $D (D A → ⊥)$ doesn't matter. It is odd that $D (D A)$ is allowed, though, since it doesn't make much sense under the usual semantics.
Dan Doel
CC BY-SA 4.0
2021-01-07T01:32:17.180Z
Interesting! I think what Agda's doing is it's checking the constructor type e.g. `A → D (D A → ⊥) → D A` by doing the substitution `A := (D A → ⊥)` , which leads to `(D A → ⊥) → D (D (D A → ⊥) → ⊥) → D (D A → ⊥)`, and `D` then appears negatively. So `D (D A)` is fine since it never leads to a negative appearance. I wonder why `D` is allowed to appear negatively as its own parameter in the first place, though, and whether any kind of negative appearance is at all "useful" or at the very least even inhabited.
ionchy
CC BY-SA 4.0
2021-01-07T05:22:56.127Z
I edited my answer to provide information about nested parameters. In general, Agda needs to trace through things like recursive functions to determine strict positivity, so it's probably easier to let that handle finding actual negative occurrences than immediately rule out negative occurrences in parameters that are never used.
Dan Doel
<reference-request><pl.programming-languages><type-theory><dependent-type><inductive-type>
Intuition behind nested positivity and counterexamples
ionchy
# Intuition behind nested positivity and counterexamples

(Asked by: username_0 on 2021-01-03)

I'm looking at the nested positivity conditions for inductive types stated in the Coq manual. First off, are there any other references (not necessarily for Coq, but in dependent type theories generally) for the nested positivity conditions and how they come about? I've found older papers like Dybjer's Inductive Families and Coquand and Paulin's Inductively Defined Types, but I believe these only mention the strict positivity condition, and newer papers like the pCuIC one and A Comprehensible Guide to CIC don't mention nested positivity either.
Now, I'm trying to gain an intuitive understanding of why nested positivity is required. In essence, nested positivity states that when defining a constructor C for some inductive type $D$, if the type of an argument to $C$ is something like $I ~ \vec{p} ~ \vec{t}$, then $D$ can only appear strictly positively in $\vec{p}$, and only if $I \neq D$. I understand that allowing $D$ in negative positions of $\vec{p}$ basically allows for proofs of $(D \to \bot) \to \bot$, and allowing $D$ in other positive positions essentially allows for double negation elimination (and some inconsistency stuff with impredicative Prop). What I don't understand are these:

Why can't $D$ appear strictly positively in $\vec{p}$ if $I = D$ (either as constructor argument or return type)? For instance, for a constructor $C$ of an inductive type $D ~ (A: \textrm{Type}): \textrm{Type}$ (with $A$ as the sole parameter), why is $C: D ~ (D ~ A) \to D ~ A$ disallowed?
EDIT: Not only is this accepted in Agda 2.6.1.2, $C: D ~ (D ~ A \to \bot) \to D ~ A$ is also accepted, which seems suspicious to me.

Why can $D$ otherwise appear strictly positively in the parameters $\vec{p}$, but not in the indices $\vec{t}$? Consider for instance the (rather silly) constructor $C: (D =_{\textrm{Type}} D) \to D$ for the inductive type $D: \textrm{Type}$, where $=$ is the usual equality type.
EDIT: It turns out this doesn't type check in Agda for unrelated universe level reasons, so consider instead the following which Agda rejects for positivity reasons:
data Box : (A : Set) → Set where
  box : (A : Set) → Box A

data D : Set where
  C : Box D → D

This is accepted by Agda if A is instead a parameter, as expected from the nested positivity rules.


I'm particularly interested in finding examples where violating nested positivity conditions (specifically these two I've listed) causes inconsistencies and proofs of $\bot$, which personally would be easier to understand than arguments about monotonicity.

**Tags:** reference-request, pl.programming-languages, type-theory, dependent-type, inductive-type

> **Comments:**
> **username_1**: Probably useful to mention https://cstheory.stackexchange.com/questions/18797/why-do-agda-and-coq-disagree-on-strict-positivity  
> **username_2**: In general, it would (I believe) be possible to encode non strictly positive types by proxy if indices were considered strictly positive. Like `neg : C = D -> ...` where `C` occurs negatively elsewhere, but is not subject to the check. I'm not certain why your particular example isn't accepted by Agda, because it has analysis for detecting that `X` is actually like a parameter (that's why `Box` is well-sized). I guess it doesn't take that into account with respect to positivity checking.  
> **username_0**: @DanDoel So I tried to construct an example and this was about as far as I could get:  `data _≡_ (A : Set) : Set → Set where refl : A ≡ A`,   `data D : Set where neg : (E : Set) → (E → ⊥) → D ≡ E → D`.   This isn't accepted but it's because `neg` needs to be in the same universe as `D`, but `E: Set` means that it's actually in `Set₁`.   Interestingly, with the constructor `c: D ≡ ⊤ → D`, Agda complains about `D` not being strictly positive in `≡`, but not if I change the type of `refl` to `A ≡ ⊤`, so it seems Agda doesn't merely check whether it's a parameter or index.  
> **username_0**: It also turns out that I can't use code blocks in comments :/  
> **username_2**: FYI, in the example in your first bullet point, if you add a constructor that actually uses $A$ in the dangerous example, Agda will complain that $D$ is no longer strictly positive. So it is just noticing that your $D (D A → ⊥)$ doesn't matter. It is odd that $D (D A)$ is allowed, though, since it doesn't make much sense under the usual semantics.  
> **username_0**: Interesting! I think what Agda's doing is it's checking the constructor type e.g. `A → D (D A → ⊥) → D A` by doing the substitution `A := (D A → ⊥)` , which leads to `(D A → ⊥) → D (D (D A → ⊥) → ⊥) → D (D A → ⊥)`, and `D` then appears negatively. So `D (D A)` is fine since it never leads to a negative appearance. I wonder why `D` is allowed to appear negatively as its own parameter in the first place, though, and whether any kind of negative appearance is at all "useful" or at the very least even inhabited.  
> **username_2**: I edited my answer to provide information about nested parameters. In general, Agda needs to trace through things like recursive functions to determine strict positivity, so it's probably easier to let that handle finding actual negative occurrences than immediately rule out negative occurrences in parameters that are never used.  

---

## 2 answers

### Answer by username_2 on 2021-01-06. Score: 1 | Accepted answer

Here is an example exploiting positivity of an index to prove false:
module Whatever where

open import Level using (Level)
open import Relation.Binary.PropositionalEquality
open import Data.Empty

variable
  ℓ : Level
  A B : Set ℓ

data _≅_ (A : Set ℓ) : Set ℓ → Set ℓ where
  trefl : A ≅ A

Subst : (P : Set ℓ → Set ℓ) → A ≅ B → P A → P B
Subst P trefl PA = PA

data U : Set where
  d : U

El : U → Set
data D : Set

El d = D

{-# NO_POSITIVITY_CHECK #-}
data D where
  neg : ∀(c : U) → El c ≅ D → (El c → ⊥) → D

¬D : D → ⊥
¬D v@(neg c eq f) = Subst (λ D → D → ⊥) eq f v

spin : ⊥
spin = ¬D (neg d trefl ¬D)

Technically it also makes use of the fact that induction-recursion can create small universes, and that type equality can be smaller than general equality applied to the universe, but those are otherwise not really problematic to my knowledge (Coq has impredicative equality anyway, I believe). It's possible the simultaneous definition could be eliminated, too, but it's not straight forward, at least.

Edit: I asked around about your first bullet point. It was pointed out to me that there is essentially nothing special about a nested type that is nested in itself. This article shows how to use a non-native translation of nested types into indexed types of equivalent size. When you do that, as long as nesting is strictly positive, it's not difficult to apply the translation to a strictly positive indexed type.
Or for instance, the example translation I was shown uses a nested $ℕ$ parameter instead of self-nesting:
data D' (A : Set) (n : ℕ) : Set where
  c : D' A (suc n) → D' A n
  t : (case n of λ where
         zero → A
         (suc m) → D' A m
      ) → D' A n

Where I added the t constructor to make something actually use A, and D A is meant to be equivalent to D' A 0. I think another way to write this would be:
data D' (A : Set) : ℕ → Set where
  c : D' A (suc n) → D' A n
  t : D' A n → D' A (suc n)
  t' : A → D' A zero

Essentially, the $ℕ$ is a tree tracking how much nesting we need to unfold.

> **Comments:**
> **username_0**: I have a suspicion that since `(El c → ⊥)` reduces to `(D → ⊥)`, the definition might not pass plain positivity (as opposed to merely violating nested positivity), but there doesn't seem to be a way to turn off *only* nested positivity in Agda anyway.  
> **username_2**: `El c` does not reduce to `D`. `El c` is a neutral term, because `c` is a variable. In my example, `d` is the only value for `c` to take, but I could easily add more.  

---

### Answer by username_0 on 2021-01-06. Score: 0

I'm going to partially answer point 2 here. If you allowed the inductive type to appear even strictly positively in another inductive's index, and you had impredicative Prop, you could derive an inconsistency through an equality type with a type that does occur negatively, as Dan stated in the comments. Here's an example in Coq, with the inductive type stated as axioms.
Inductive Equal (A: Prop) : Prop -> Prop :=
| refl : Equal A A.

(** These axioms correspond to the following inductive definition:
 *  Inductive D : Prop :=
 *  | C : forall (E: Prop) (p: Equal D E), (E -> False) -> D. *)
Axiom D : Prop.
Axiom introD: forall (E: Prop) (p: Equal D E), (E -> False) -> D.
Axiom matchD: forall (E: Prop) (p: Equal D E), D -> (E -> False).

Definition DnotD (d: D): (D -> False) := matchD D (refl D) d.
Definition notD (d: D): False := (DnotD d) d.
Definition isD: D := introD D (refl D) notD.
Definition bottom: False := notD isD.

I'm not sure whether you can do the same when you only have predicative universes without resorting to universe polymorphism tricks or the like.


---

