[Agda] Relaxing the strict positivity requirement

[Peter Hancock]

On 06/12/2011 21:49, Andreas Abel wrote:
> Hello Daniel,
>
> first of all, I think it is not inconsistent, because you have
> already given it a semantics in terms of recursion. You can even
> define Context by recursion over a natural number (its length).

I'd like to seize on this, as it came up in some conversations I've
had last week.  Is it better to use recursion over natural numbers?
Or induction recursion? Or induction-induction?

* Correct me if I am mistaken, but if you define contexts by
   recursion on their length, you are iterating an operator, namely
   (. F) (precomposition with an operator of type Set -> Set), of
   quite a high type, namely (Set -> Set) -> Set -> Set.  We are among
   the high peaks of so called "nested" fixed points, where the Yeti live.

   This isn't allowed in a type-theory in which a recursion/induction/iteration/eliminator
   must have for its codomain/motive "C" a family of sets; one has to replace
   Set by a universe { T a | a : U }, and iterate things in (U -> U) -> U -> U

   On the other hand, by defining contexts with induction recursion, we
   don't use a pre-given universe explicitly, but construct a purpose built one,
   closed under the right kind of Sigma.  We get a convenient "snoc" constructor,
   giving ready access to the most recently introduced type in an extended context.
   This is somehow the business end of a context, if one looks "upwards" into it.

   Another possibility is to transform a definition of a family (U,T)
   by induction recursion into an inductive definition of the U together
   with an inductive definition of the relation that is T's graph.

> Second, your suggestion to use the termination checker on inductive
> families comes natural if you understand inductive families as being
> defined by recursion over some suitably large enough ordinal in the
> first place. Then also, the inductive-inductive-coinductive-recursive
> jungle disappears.

Actually, the constructive treatment of inductive definitions doesn't
use ordinals much, as they are worse behaved than their classical cousins.
(They don't form an orderly trichotomous line.)  Instead of large ordinals,
you use large sets.
The best written explanation of inductive definitions from a constructive point
of view is maybe in Peter Aczel and Michael Rathjen's (2007?) notes on CZF.
I think there is another paper of Rathjen's about coinduction in CZF, or at
least about Aczel's related anti-foundation axiom.

As for a type-theoretic notion of ordinal, one can use induction recursion to
define sets whose elements are trees with ordinal-like properties, with
enormous hight (wrt a certain hierarchy of enormity devised by Paul Mahlo).
But they are very awkward to deal with, and clumsy compared to God's own
classical set-theoretical ordinals.  In any case, the concept of "ordinal"
is really a class, intrinsically something large, and this cannot be
captured by any set of trees.

In the classical theory of least fixed points, you take a colimit of a
diagram which is a trichotomous chain of in general transfinite length,
indexed by ordinals.  In the constructive theory, you take a colimit of
a diagram that is quite a bit nastier.


Hank