Impredicative universe?

[UlfNorell]

From nils.anders.danielsson on April 23, 2013 14:15:26

Do we really want to allow the following code?

mutual

data U : Set where u : U

El : U → Set El u = U

Original issue: http://code.google.com/p/agda/issues/detail?id=837

[UlfNorell]

From guillaum...@gmail.com on April 23, 2013 07:05:43

I don’t see the problem with this particular piece of code: the mutual block is useless given that U does not depend on El, U is isomorphic to Unit and El is the constant function from Unit to Set picking out U.

I tried to do the following instead:

mutual

data U : Set where u : U pi : (A : U) (B : El A → U) → U

El : U → Set El u = U El (pi A B) = (x : El A) → El (B x)

but it’s not accepted by Agda’s positivity checker:

U is not strictly positive, because it occurs in the type of the constructor pi in the definition of U, which occurs in the first clause in the definition of El, which occurs to the left of an arrow in the type of the constructor pi in the definition of U.

[UlfNorell]

From nils.anders.danielsson on April 23, 2013 09:50:11

You can define a universe with a code for itself using "proper" mutual recursion, but (I hope that) you can't use El in a negative way:

mutual

data U : Set where
  u          : U
  _but-only_ : (a : U) → El a → U

El : U → Set
El u              = U
El (a but-only x) = Σ (El a) λ y → x ≡ y

I'm not claiming that this feature leads to an inconsistency. However, I wonder if anyone claims that it doesn't.

[UlfNorell]

From andreas....@gmail.com on April 30, 2013 11:01:28

To answer the original question, no, I would not want to allow it. If one explains induction-recursion by induction on ordinals, then one would have something like

U : Size -> Set El : (i : Size) -> U i -> Set

U i = 1 + exists j<i. ... U j ... El i (inl ()) = here I can only refer to U j for some j < i, not to the whole of U

So, from my perspective there is no justification of a universe with a code for itself.

However, currently there is no component in Agda devoted to check induction-recursion. We just have the positivity and the termination checker, but their interplay in the context of i-r has not been formally studied. By chance, positivity and termination checking might exclude inconsistencies, but it is not guaranteed. However, as long as no inconsistency is known, fixing this is not a high prio.

[UlfNorell]

From nils.anders.danielsson on September 17, 2013 03:32:05

Status: Accepted
Labels: Type-Defect Priority-Low InductionRecursion