The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

Hi,

Here is a funny example using the new form of sort polymorphism of  
the inductive types
and the new rules for parameters of V8.1.

It is a variation over Peter Aczel's inductive encoding of sets in  
type theory.
We see that the universe inconsistency happens when we are *very* close
to the paradox.


(BTW, this idea may help you for your categories)


Cheers,


Benjamin


(in the code, ens and ENS stand for set, which is already used in Coq)

------------------


(* the type of sets whose elements are indexed by type A *)
Inductive ens (A:Type) : Type :=
sup :  (A-> {B:Type & (ens B)})->(ens A).

(* A set is a set together with its carrier type *)
Definition ENS := {A:Type & (ens A)}.

(* The canonical way to construct a set *)
Definition SUP : forall A : Type, (A -> ENS) -> ENS.
intros A f; exists A.
apply sup.
assumption.
Defined.

(* the set of all sets, indexed by the type of sets *)
Definition big : (ens ENS).
apply sup.
intros [B e].
exists B; exact e.
Defined.


(* Is this set a set ??? *)
Definition BIG : ENS.
exists ENS.
exact big.
Defined.