StrictlyPositive.agda

open import Data.Nat
open import Data.Fin

module StrictlyPositive where

  -- The following datatype is accepted by Agda, but rejected
  -- by Coq
  data Ty : Set0 -> Set0 where
    c1 : Ty ℕ
    c2 : Ty (Ty ℕ)
    c3 : Ty (Ty (Ty ℕ))
  -- Coq complains that the occurrences of [Ty _] in the index positions of
  -- c2 and c3 violate strict positivity.

  {- So apparently Coq and Agda have different notions of strictly positive,
     which I thought was a well-defined syntactic restriction on inductive
     schema.

     I found no explanation online of *why* this is permitted, but apparently Nils
     Anders Danielsson thinks this should be prohibited, and Voevodsky claims
     this is incompatible with univalence:
     https://lists.chalmers.se/pipermail/agda/2012/004249.html
     
     Looking at one of Dybjer's early inductive type papers, after a vague offhand
     comment in the introduction that Paulin-Möhring and Coquand's version has slight
     differences due to being in an impredicative theory on page 7 of Inductive Families
     (http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf) Dybjer presents
     a scheme for inductive definitions of a type P where P seems to be allowed as
     an index in the result of any constructor (e.g. ctor_i : ... -> P (P ...) is allowed)
     as in Agda, whereas the Coq documentation and Paulin-Möhring's CID paper is quite
     explicit that this is disallowed.  This suggests that this discrepancy might be
     a result of predicativity vs. impredicativity (though Set in Coq has been predicative
     by default since version 7), though I can't find any clear description of the different
     restrictions imposed on inductive definitions in impredicative vs. predicative
     type theories.
  -}
    
  {- The following is also permitted, and equivalent to the single inductive family
     above.  But is this accepted because it's a baseline inductive-recursive
     definition, or because Agda again has a more liberal view of strict positivity than Coq would?
     (There's no direct Coq equivalent, since Coq doesn't support direct IR definitions.)
  -}
  mutual
    data U : Set0 -> Set0 where
      c : (i : Fin 3) -> U (T i)
    T : Fin 3 -> Set0
    T zero = ℕ
    T (suc zero) = U ℕ
    T (suc (suc i)) = U (U ℕ)

StrictlyPositive.v

Inductive Ty : Set -> Set :=
  | c1 : Ty nat
  | c2 : Ty (Ty nat)
  | c3 : Ty (Ty (Ty nat)).

(* Apparently Coq'Art uses almost the same definition in demonstrating a definition
   that violates strict positivity (Section 14.1.2.1, p.379):
*)
Inductive T : Set -> Set := c : (T (T nat)).