Imported Upstream version 8.5~beta1+dfsg

33 files changed, 1870 insertions, 262 deletions

diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index 9f01c565..d72f4072 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -67,18 +67,13 @@ Variables A B : Prop.
 
 Record retract : Prop :=
   {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}.
-
 Record retract_cond : Prop :=
   {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}.
 
-
 (** The dependent elimination above implies the axiom of choice: *)
-Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a.
-Proof.
-intros r.
-case r; simpl.
-trivial.
-Qed.
+
+Lemma AC : forall r:retract_cond, retract -> forall a:A, r.(j2) (r.(i2) a) = a.
+Proof. intros r. exact r.(inv2). Qed.
 
 End Retracts.
 
@@ -114,7 +109,7 @@ Proof.
 exists g f.
 intro a.
 unfold f, g; simpl.
-apply AC.
+apply AC. 
 exists (fun x:pow U => x) (fun x:pow U => x).
 trivial.
 Qed.
@@ -132,9 +127,10 @@ Lemma not_has_fixpoint : R R = Not_b (R R).
 Proof.
 unfold R at 1.
 unfold g.
-rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)).
+rewrite AC.
+trivial.
+exists (fun x:pow U => x) (fun x:pow U => x).
 trivial.
-exists (fun x:pow U => x) (fun x:pow U => x); trivial.
 Qed.
 
 
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index d8fb5dd4..d2327498 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -52,7 +52,7 @@ We let also
 - IPL^2   = 2nd-order functional minimal predicate logic (with ex. quant.)
 - IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal pred. logic (with ex. quant.)
 
-with no prerequisite on the non-emptyness of domains
+with no prerequisite on the non-emptiness of domains
 
 Table of contents
 
@@ -89,12 +89,19 @@ intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
 *)
 
 Set Implicit Arguments.
+Local Unset Intuition Negation Unfolding.
 
 (**********************************************************************)
 (** * Definitions *)
 
 (** Choice, reification and description schemes *)
 
+(** We make them all polymorphic. Most of them have existentials as conclusion
+    so they require polymorphism otherwise their first application (e.g. to an
+    existential in [Set]) will fix the level of [A].
+*)
+(* Set Universe Polymorphism. *)
+
 Section ChoiceSchemes.
 
 Variables A B :Type.
@@ -216,39 +223,39 @@ End ChoiceSchemes.
 (** Generalized schemes *)
 
 Notation RelationalChoice :=
-  (forall A B, RelationalChoice_on A B).
+  (forall A B : Type, RelationalChoice_on A B).
 Notation FunctionalChoice :=
-  (forall A B, FunctionalChoice_on A B).
+  (forall A B : Type, FunctionalChoice_on A B).
 Definition FunctionalDependentChoice :=
-  (forall A, FunctionalDependentChoice_on A).
+  (forall A : Type, FunctionalDependentChoice_on A).
 Definition FunctionalCountableChoice :=
-  (forall A, FunctionalCountableChoice_on A).
+  (forall A : Type, FunctionalCountableChoice_on A).
 Notation FunctionalChoiceOnInhabitedSet :=
-  (forall A B, inhabited B -> FunctionalChoice_on A B).
+  (forall A B : Type, inhabited B -> FunctionalChoice_on A B).
 Notation FunctionalRelReification :=
-  (forall A B, FunctionalRelReification_on A B).
+  (forall A B : Type, FunctionalRelReification_on A B).
 
 Notation GuardedRelationalChoice :=
-  (forall A B, GuardedRelationalChoice_on A B).
+  (forall A B : Type, GuardedRelationalChoice_on A B).
 Notation GuardedFunctionalChoice :=
-  (forall A B, GuardedFunctionalChoice_on A B).
+  (forall A B : Type, GuardedFunctionalChoice_on A B).
 Notation GuardedFunctionalRelReification :=
-  (forall A B, GuardedFunctionalRelReification_on A B).
+  (forall A B : Type, GuardedFunctionalRelReification_on A B).
 
 Notation OmniscientRelationalChoice :=
-  (forall A B, OmniscientRelationalChoice_on A B).
+  (forall A B : Type, OmniscientRelationalChoice_on A B).
 Notation OmniscientFunctionalChoice :=
-  (forall A B, OmniscientFunctionalChoice_on A B).
+  (forall A B : Type, OmniscientFunctionalChoice_on A B).
 
 Notation ConstructiveDefiniteDescription :=
-  (forall A, ConstructiveDefiniteDescription_on A).
+  (forall A : Type, ConstructiveDefiniteDescription_on A).
 Notation ConstructiveIndefiniteDescription :=
-  (forall A, ConstructiveIndefiniteDescription_on A).
+  (forall A : Type, ConstructiveIndefiniteDescription_on A).
 
 Notation IotaStatement :=
-  (forall A, IotaStatement_on A).
+  (forall A : Type, IotaStatement_on A).
 Notation EpsilonStatement :=
-  (forall A, EpsilonStatement_on A).
+  (forall A : Type, EpsilonStatement_on A).
 
 (** Subclassical schemes *)
 
@@ -292,7 +299,7 @@ Proof.
 Qed.
 
 Lemma funct_choice_imp_rel_choice :
-  forall A B, FunctionalChoice_on A B -> RelationalChoice_on A B.
+  forall A B : Type, FunctionalChoice_on A B -> RelationalChoice_on A B.
 Proof.
   intros A B FunCh R H.
   destruct (FunCh R H) as (f,H0).
@@ -305,7 +312,7 @@ Proof.
 Qed.
 
 Lemma funct_choice_imp_description :
-  forall A B, FunctionalChoice_on A B -> FunctionalRelReification_on A B.
+  forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B.
 Proof.
   intros A B FunCh R H.
   destruct (FunCh R) as [f H0].
@@ -318,10 +325,10 @@ Proof.
 Qed.
 
 Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
-  forall A B, FunctionalChoice_on A B <->
+  forall A B : Type, FunctionalChoice_on A B <->
     RelationalChoice_on A B /\ FunctionalRelReification_on A B.
 Proof.
-  intros A B; split.
+  intros A B. split.
   intro H; split;
     [ exact (funct_choice_imp_rel_choice H)
       | exact (funct_choice_imp_description H) ].
@@ -333,7 +340,7 @@ Qed.
 
 (** We show that the guarded formulations of the axiom of choice
    are equivalent to their "omniscient" variant and comes from the non guarded
-   formulation in presence either of the independance of general premises
+   formulation in presence either of the independence of general premises
    or subset types (themselves derivable from subtypes thanks to proof-
    irrelevance) *)
 
@@ -362,7 +369,7 @@ Proof.
 Qed.
 
 Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice :
-  forall A B, inhabited B -> RelationalChoice_on A B ->
+  forall A B : Type, inhabited B -> RelationalChoice_on A B ->
     IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B.
 Proof.
   intros A B Inh AC_rel IndPrem P R H.
@@ -374,7 +381,7 @@ Proof.
 Qed.
 
 Lemma guarded_rel_choice_imp_rel_choice :
-  forall A B, GuardedRelationalChoice_on A B -> RelationalChoice_on A B.
+  forall A B : Type, GuardedRelationalChoice_on A B -> RelationalChoice_on A B.
 Proof.
   intros A B GAC_rel R H.
   destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)).
@@ -793,12 +800,13 @@ be applied on the same Type universes on both sides of the first
 Require Import Setoid.
 
 Theorem constructive_definite_descr_excluded_middle :
-  ConstructiveDefiniteDescription ->
+  (forall A : Type, ConstructiveDefiniteDescription_on A) ->
   (forall P:Prop, P \/ ~ P) -> (forall P:Prop, {P} + {~ P}).
 Proof.
   intros Descr EM P.
   pose (select := fun b:bool => if b then P else ~P).
   assert { b:bool | select b } as ([|],HP).
+  red in Descr.
   apply Descr.
   rewrite <- unique_existence; split.
   destruct (EM P).
@@ -814,14 +822,13 @@ Corollary fun_reification_descr_computational_excluded_middle_in_prop_context :
   (forall P:Prop, P \/ ~ P) ->
   forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.
 Proof.
-  intros FunReify EM C H.
-  apply relative_non_contradiction_of_definite_descr; trivial.
-  auto using constructive_definite_descr_excluded_middle.
+  intros FunReify EM C H. intuition auto using
+    constructive_definite_descr_excluded_middle,
+    (relative_non_contradiction_of_definite_descr (C:=C)).
 Qed.
 
 (**********************************************************************)
 (** * Choice => Dependent choice => Countable choice *)
-
 (* The implications below are standard *)
 
 Require Import Arith.
diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v
index 6085594b..600db472 100644
--- a/theories/Logic/Classical.v
+++ b/theories/Logic/Classical.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index ba7e87d1..07153b35 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 7d79913a..bdad50e2 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v
index 161db112..2d9a1ffd 100644
--- a/theories/Logic/ClassicalEpsilon.v
+++ b/theories/Logic/ClassicalEpsilon.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index c6e140f5..6f736e45 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -339,8 +339,8 @@ Section Proof_irrelevance_EM_CC.
 
   (** [p2b] and [b2p] form a retract if [~b1=b2] *)
 
-  Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A).
-  Definition b2p b := b1 = b.
+  Let p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A).
+  Let b2p b := b1 = b.
 
   Lemma p2p1 : forall A:Prop, A -> b2p (p2b A).
   Proof.
@@ -367,16 +367,90 @@ Section Proof_irrelevance_EM_CC.
   Proof.
     refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H.
     trivial.
-    apply (paradox B p2b b2p (p2p2 H) p2p1).
+    apply (NoRetractFromSmallPropositionToProp.paradox B p2b b2p (p2p2 H) p2p1).
   Qed.
 
 End Proof_irrelevance_EM_CC.
 
-(** Remark: Hurkens' paradox still holds with a retract from the
-    _negative_ fragment of [Prop] into [bool], hence weak classical
-    logic, i.e. [forall A, ~A\/~~A], is enough for deriving
-    proof-irrelevance.
-*)
+(** Hurkens' paradox still holds with a retract from the _negative_
+    fragment of [Prop] into [bool], hence weak classical logic,
+    i.e. [forall A, ~A\/~~A], is enough for deriving a weak version of
+    proof-irrelevance. This is enough to derive a contradiction from a
+    [Set]-bound weak excluded middle wih an impredicative [Set]
+    universe. *)
+
+Section Proof_irrelevance_WEM_CC.
+
+  Variable or : Prop -> Prop -> Prop.
+  Variable or_introl : forall A B:Prop, A -> or A B.
+  Variable or_intror : forall A B:Prop, B -> or A B.
+  Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C.
+  Hypothesis
+    or_elim_redl :
+    forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A),
+      f a = or_elim A B C f g (or_introl A B a).
+  Hypothesis
+    or_elim_redr :
+    forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B),
+      g b = or_elim A B C f g (or_intror A B b).
+  Hypothesis
+    or_dep_elim :
+    forall (A B:Prop) (P:or A B -> Prop),
+      (forall a:A, P (or_introl A B a)) ->
+      (forall b:B, P (or_intror A B b)) -> forall b:or A B, P b.
+
+  Hypothesis wem : forall A:Prop, or (~~A) (~ A).
+
+  Local Notation NProp := NoRetractToNegativeProp.NProp.
+  Local Notation El := NoRetractToNegativeProp.El.
+  
+  Variable B : Prop.
+  Variables b1 b2 : B.
+
+  (** [p2b] and [b2p] form a retract if [~b1=b2] *)
+
+  Let p2b (A:NProp) := or_elim (~~El A) (~El A) B (fun _ => b1) (fun _ => b2) (wem (El A)).
+  Let b2p b : NProp := exist (fun P=>~~P -> P) (~~(b1 = b)) (fun h x => h (fun k => k x)).
+
+  Lemma wp2p1 : forall A:NProp, El A -> El (b2p (p2b A)).
+  Proof.
+    intros A. unfold p2b.
+    apply or_dep_elim with  (b := wem (El A)).
+    + intros nna a.
+      rewrite <- or_elim_redl.
+      cbn. auto.
+    + intros n x.
+      destruct (n x).
+  Qed.
+
+  Lemma wp2p2 : b1 <> b2 -> forall A:NProp, El (b2p (p2b A)) -> El A.
+  Proof.
+    intro not_eq_b1_b2.
+    intros A. unfold p2b.
+    apply or_dep_elim with  (b := wem (El A)).
+    + cbn.
+      intros x _.
+      destruct A. cbn in x |- *.
+      auto.
+    + intros na.
+      rewrite <- or_elim_redr. cbn.
+      intros h. destruct (h not_eq_b1_b2).
+  Qed.
+
+  (** By Hurkens's paradox, we get a weak form of proof irrelevance. *)
+
+  Theorem wproof_irrelevance_cc : ~~(b1 = b2).
+  Proof.
+    intros h.
+    refine (let NB := exist (fun P=>~~P -> P) B _ in _).
+    { exact (fun _ => b1). }
+    pose proof (NoRetractToNegativeProp.paradox NB p2b b2p (wp2p2 h) wp2p1) as paradox.
+    refine (let F := exist (fun P=>~~P->P) False _ in _).
+    { auto. }
+    exact (paradox F).
+  Qed.
+
+End Proof_irrelevance_WEM_CC.
 
 (************************************************************************)
 (** ** CIC |- excluded-middle -> proof-irrelevance               *)
@@ -405,6 +479,23 @@ Section Proof_irrelevance_CCI.
 
 End Proof_irrelevance_CCI.
 
+(** The same holds with weak excluded middle. The proof is a little
+    more involved, however. *)
+
+
+
+Section Weak_proof_irrelevance_CCI.
+
+  Hypothesis wem : forall A:Prop, ~~A \/ ~ A.
+
+  Theorem wem_proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), ~~b1 = b2.
+  Proof.
+    exact (wproof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl
+      or_elim_redr or_indd wem).
+  Qed.
+
+End Weak_proof_irrelevance_CCI.
+
 (** Remark: in the Set-impredicative CCI, Hurkens' paradox still holds with
     [bool] in [Set] and since [~true=false] for [true] and [false]
     in [bool] from [Set], we get the inconsistency of
diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
index 1cdff497..4b0ec15e 100644
--- a/theories/Logic/ClassicalUniqueChoice.v
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -42,8 +42,8 @@ intros A B.
 apply (dependent_unique_choice A (fun _ => B)).
 Qed.
 
-(** The following proof comes from [[ChicliPottierSimpson02]] *)
 
+(** The following proof comes from [[ChicliPottierSimpson02]] *)
 Require Import Setoid.
 
 Theorem classic_set_in_prop_context :
@@ -78,7 +78,7 @@ destruct (f P).
   right.
   destruct HfP as [[_ Hfalse]| [Hna _]].
     discriminate.
-    assumption.
+    assumption. 
 Qed.
 
 Corollary not_not_classic_set :
diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v
deleted file mode 100644
index d634217f..00000000
--- a/theories/Logic/Classical_Pred_Set.v
+++ /dev/null
@@ -1,48 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* File created for Coq V5.10.14b, Oct 1995, by duplication of
-   Classical_Pred_Type.v *)
-
-(** This file is obsolete, use Classical_Pred_Type.v via Classical.v
-instead *)
-
-(** Classical Predicate Logic on Set*)
-
-Require Import Classical_Pred_Type.
-
-Section Generic.
-Variable U : Set.
-
-(** de Morgan laws for quantifiers *)
-
-Lemma not_all_ex_not :
- forall P:U -> Prop, ~ (forall n:U, P n) ->  exists n : U, ~ P n.
-Proof (Classical_Pred_Type.not_all_ex_not U).
-
-Lemma not_all_not_ex :
- forall P:U -> Prop, ~ (forall n:U, ~ P n) ->  exists n : U, P n.
-Proof (Classical_Pred_Type.not_all_not_ex U).
-
-Lemma not_ex_all_not :
- forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
-Proof (Classical_Pred_Type.not_ex_all_not U).
-
-Lemma not_ex_not_all :
- forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n.
-Proof (Classical_Pred_Type.not_ex_not_all U).
-
-Lemma ex_not_not_all :
- forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n).
-Proof (Classical_Pred_Type.ex_not_not_all U).
-
-Lemma all_not_not_ex :
- forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n).
-Proof (Classical_Pred_Type.all_not_not_ex U).
-
-End Generic.
diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v
index 78eae431..8468ced3 100644
--- a/theories/Logic/Classical_Pred_Type.v
+++ b/theories/Logic/Classical_Pred_Type.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index 7fbd6da8..be75c4e9 100644
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v
deleted file mode 100644
index 90d55160..00000000
--- a/theories/Logic/Classical_Type.v
+++ /dev/null
@@ -1,14 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This file is obsolete, use Classical.v instead *)
-
-(** Classical Logic for Type *)
-
-Require Export Classical_Prop.
-Require Export Classical_Pred_Type.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 7403208a..6f5bfae4 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -51,9 +51,9 @@ Hypothesis P_dec : forall n, {P n}+{~(P n)}.
 any number before any witness (not necessarily the [x] of [exists x :A, P x])
 makes the search eventually stops. *)
 
-Inductive before_witness : nat -> Prop :=
-  | stop : forall n, P n -> before_witness n
-  | next : forall n, before_witness (S n) -> before_witness n.
+Inductive before_witness (n:nat) : Prop :=
+  | stop : P n -> before_witness n
+  | next : before_witness (S n) -> before_witness n.
 
 (* Computation of the initial termination certificate *)
 Fixpoint O_witness (n : nat) : before_witness n -> before_witness 0 :=
@@ -67,9 +67,9 @@ is structurally smaller even in the [stop] case. *)
 Definition inv_before_witness :
   forall n, before_witness n -> ~(P n) -> before_witness (S n) :=
   fun n b =>
-    match b in before_witness n return ~ P n -> before_witness (S n) with
-      | stop n p => fun not_p => match (not_p p) with end
-      | next n b => fun _ => b
+    match b return ~ P n -> before_witness (S n) with
+      | stop _ p => fun not_p => match (not_p p) with end
+      | next _ b => fun _ => b
     end.
 
 Fixpoint linear_search m (b : before_witness m) : {n : nat | P n} :=
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 3724d8e2..545f92bd 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -175,7 +175,16 @@ Proof.
 unfold decidable. tauto.
 Qed.
 
+(* Functional relations on decidable co-domains are decidable *)
 
+Theorem dec_functional_relation :
+  forall (X Y : Type) (A:X->Y->Prop), (forall y y' : Y, decidable (y=y')) ->
+  (forall x, exists! y, A x y) -> forall x y, decidable (A x y).
+Proof.
+intros X Y A Hdec H x y.
+destruct (H x) as (y',(Hex,Huniq)).
+destruct (Hdec y y') as [->|Hnot]; firstorder.
+Qed.
 
 (** With the following hint database, we can leverage [auto] to check
     decidability of propositions. *)
diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v
index 69ed908f..70cc0787 100644
--- a/theories/Logic/Description.v
+++ b/theories/Logic/Description.v
@@ -1,13 +1,13 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 (** This file provides a constructive form of definite description; it
-    allows to build functions from the proof of their existence in any
+    allows building functions from the proof of their existence in any
     context; this is weaker than Church's iota operator *)
 
 Require Import ChoiceFacts.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 71458647..64517354 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -99,7 +99,7 @@ Lemma AC_bool_subset_to_bool :
 Proof.
   destruct (guarded_rel_choice _ _
    (fun Q:bool -> Prop =>  exists y : _, Q y)
-   (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)).
+   (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)). 
     exact (fun _ H => H).
   exists R; intros P HP.
   destruct (HR P HP) as (y,(Hy,Huni)).
@@ -113,23 +113,23 @@ Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.
 Proof.
 intro P.
 
-(** first we exhibit the choice functional relation R *)
+(* first we exhibit the choice functional relation R *)
 destruct AC_bool_subset_to_bool as [R H].
 
 set (class_of_true := fun b => b = true \/ P).
 set (class_of_false := fun b => b = false \/ P).
 
-(** the actual "decision": is (R class_of_true) = true or false? *)
+(* the actual "decision": is (R class_of_true) = true or false? *)
 destruct (H class_of_true) as [b0 [H0 [H0' H0'']]].
 exists true; left; reflexivity.
 destruct H0.
 
-(** the actual "decision": is (R class_of_false) = true or false? *)
+(* the actual "decision": is (R class_of_false) = true or false? *)
 destruct (H class_of_false) as [b1 [H1 [H1' H1'']]].
 exists false; left; reflexivity.
 destruct H1.
 
-(** case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *)
+(* case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *)
 right.
 intro HP.
 assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b).
@@ -145,7 +145,7 @@ rewrite <- H0''. reflexivity.
 rewrite Heq.
 assumption.
 
-(** cases where P is true *)
+(* cases where P is true *)
 left; assumption.
 left; assumption.
 
@@ -154,7 +154,7 @@ Qed.
 End PredExt_RelChoice_imp_EM.
 
 (**********************************************************************)
-(** * B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *)
+(** * Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *)
 
 (** This is an adaptation of Diaconescu's theorem, exploiting the
     form of extensionality provided by proof-irrelevance *)
@@ -172,7 +172,7 @@ Variables a1 a2 : A.
 
 (** We build the subset [A'] of [A] made of [a1] and [a2] *)
 
-Definition A' := sigT (fun x => x=a1 \/ x=a2).
+Definition A' := @sigT A (fun x => x=a1 \/ x=a2).
 
 Definition a1':A'.
 exists a1 ; auto.
diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v
index e4663604..fe17cde4 100644
--- a/theories/Logic/Epsilon.v
+++ b/theories/Logic/Epsilon.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index e6c38c77..d9ffe68d 100644
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index c0fc0d72..34aba486 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -52,6 +52,8 @@ Table of contents:
 
 Import EqNotations.
 
+(* Set Universe Polymorphism. *)
+
 Section Dependent_Equality.
 
   Variable U : Type.
@@ -140,7 +142,7 @@ Qed.
 Notation equiv_eqex_eqdep := eq_sigT_iff_eq_dep (only parsing). (* Compat *)
 
 Lemma eq_sig_eq_dep :
-  forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
+  forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
     exist P p x = exist P q y -> eq_dep p x q y.
 Proof.
   intros.
@@ -149,24 +151,25 @@ Proof.
 Qed.
 
 Lemma eq_dep_eq_sig :
-  forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
+  forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
     eq_dep p x q y -> exist P p x = exist P q y.
 Proof.
   destruct 1; reflexivity.
 Qed.
 
 Lemma eq_sig_iff_eq_dep :
-  forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
+  forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
     exist P p x = exist P q y <-> eq_dep p x q y.
 Proof.
   split; auto using eq_sig_eq_dep, eq_dep_eq_sig.
 Qed.
 
-(** Dependent equality is equivalent to a dependent pair of equalities *)
+(** Dependent equality is equivalent tco a dependent pair of equalities *)
 
 Set Implicit Arguments.
 
-Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rew H in H1 = H2}.
+Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <->
+                                                   {H:x1=x2 | rew H in H1 = H2}.
 Proof.
   intros; split; intro H.
   - change x2 with (projT1 (existT P x2 H2)).
@@ -234,82 +237,113 @@ Section Equivalences.
 
   (** Invariance by Substitution of Reflexive Equality Proofs *)
 
-  Definition Eq_rect_eq :=
-    forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+  Definition Eq_rect_eq_on (p : U) (Q : U -> Type) (x : Q p) :=
+    forall (h : p = p), x = eq_rect p Q x p h.
+  Definition Eq_rect_eq := forall p Q x, Eq_rect_eq_on p Q x.
 
   (** Injectivity of Dependent Equality *)
 
-  Definition Eq_dep_eq :=
-    forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y.
+  Definition Eq_dep_eq_on (P : U -> Type) (p : U) (x : P p) :=
+    forall (y : P p), eq_dep p x p y -> x = y.
+  Definition Eq_dep_eq := forall P p x, Eq_dep_eq_on P p x.
 
   (** Uniqueness of Identity Proofs (UIP) *)
 
-  Definition UIP_ :=
-    forall (x y:U) (p1 p2:x = y), p1 = p2.
+  Definition UIP_on_ (x y : U) (p1 : x = y) :=
+    forall (p2 : x = y), p1 = p2.
+  Definition UIP_ := forall x y p1, UIP_on_ x y p1.
 
   (** Uniqueness of Reflexive Identity Proofs *)
 
-  Definition UIP_refl_ :=
-    forall (x:U) (p:x = x), p = eq_refl x.
+  Definition UIP_refl_on_ (x : U) :=
+    forall (p : x = x), p = eq_refl x.
+  Definition UIP_refl_ := forall x, UIP_refl_on_ x.
 
   (** Streicher's axiom K *)
 
-  Definition Streicher_K_ :=
-    forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.
+  Definition Streicher_K_on_ (x : U) (P : x = x -> Prop) :=
+    P (eq_refl x) -> forall p : x = x, P p.
+  Definition Streicher_K_ := forall x P, Streicher_K_on_ x P.
 
   (** Injectivity of Dependent Equality is a consequence of *)
   (** Invariance by Substitution of Reflexive Equality Proof *)
 
-  Lemma eq_rect_eq__eq_dep1_eq :
-    Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y.
+  Lemma eq_rect_eq_on__eq_dep1_eq_on (p : U) (P : U -> Type) (y : P p) :
+    Eq_rect_eq_on p P y -> forall (x : P p), eq_dep1 p x p y -> x = y.
   Proof.
     intro eq_rect_eq.
     simple destruct 1; intro.
     rewrite <- eq_rect_eq; auto.
   Qed.
+  Lemma eq_rect_eq__eq_dep1_eq :
+    Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y.
+  Proof (fun eq_rect_eq P p y x =>
+           @eq_rect_eq_on__eq_dep1_eq_on p P x (eq_rect_eq p P x) y).
 
-  Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq.
+  Lemma eq_rect_eq_on__eq_dep_eq_on (p : U) (P : U -> Type) (x : P p) :
+    Eq_rect_eq_on p P x -> Eq_dep_eq_on P p x.
   Proof.
     intros eq_rect_eq; red; intros.
-    apply (eq_rect_eq__eq_dep1_eq eq_rect_eq); apply eq_dep_dep1; trivial.
+    symmetry; apply (eq_rect_eq_on__eq_dep1_eq_on _ _ _ eq_rect_eq).
+    apply eq_dep_sym in H; apply eq_dep_dep1; trivial.
   Qed.
+  Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq.
+  Proof (fun eq_rect_eq P p x y =>
+           @eq_rect_eq_on__eq_dep_eq_on p P x (eq_rect_eq p P x) y).
 
   (** Uniqueness of Identity Proofs (UIP) is a consequence of *)
   (** Injectivity of Dependent Equality *)
 
-  Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_.
+  Lemma eq_dep_eq_on__UIP_on (x y : U) (p1 : x = y) :
+    Eq_dep_eq_on (fun y => x = y) x eq_refl -> UIP_on_ x y p1.
   Proof.
     intro eq_dep_eq; red.
-    intros; apply eq_dep_eq with (P := fun y => x = y).
-    elim p2 using eq_indd.
     elim p1 using eq_indd.
+    intros; apply eq_dep_eq.
+    elim p2 using eq_indd.
     apply eq_dep_intro.
   Qed.
+  Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_.
+  Proof (fun eq_dep_eq x y p1 =>
+           @eq_dep_eq_on__UIP_on x y p1 (eq_dep_eq _ _ _)).
 
   (** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *)
 
-  Lemma UIP__UIP_refl : UIP_ -> UIP_refl_.
+  Lemma UIP_on__UIP_refl_on (x : U) :
+    UIP_on_ x x eq_refl -> UIP_refl_on_ x.
   Proof.
-    intro UIP; red; intros; apply UIP.
+    intro UIP; red; intros; symmetry; apply UIP.
   Qed.
+  Lemma UIP__UIP_refl : UIP_ -> UIP_refl_.
+  Proof (fun UIP x p =>
+           @UIP_on__UIP_refl_on x (UIP x x eq_refl) p).
 
   (** Streicher's axiom K is a direct consequence of Uniqueness of
       Reflexive Identity Proofs *)
 
-  Lemma UIP_refl__Streicher_K : UIP_refl_ -> Streicher_K_.
+  Lemma UIP_refl_on__Streicher_K_on (x : U) (P : x = x -> Prop) :
+    UIP_refl_on_ x -> Streicher_K_on_ x P.
   Proof.
     intro UIP_refl; red; intros; rewrite UIP_refl; assumption.
   Qed.
+  Lemma UIP_refl__Streicher_K : UIP_refl_ -> Streicher_K_.
+  Proof (fun UIP_refl x P =>
+           @UIP_refl_on__Streicher_K_on x P (UIP_refl x)).
 
   (** We finally recover from K the Invariance by Substitution of
       Reflexive Equality Proofs *)
 
-  Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq.
+  Lemma Streicher_K_on__eq_rect_eq_on (p : U) (P : U -> Type) (x : P p) :
+    Streicher_K_on_ p (fun h => x = rew -> [P] h in x)
+    -> Eq_rect_eq_on p P x.
   Proof.
     intro Streicher_K; red; intros.
-    apply Streicher_K with (p := h).
+    apply Streicher_K.
     reflexivity.
   Qed.
+  Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq.
+  Proof (fun Streicher_K p P x =>
+           @Streicher_K_on__eq_rect_eq_on p P x (Streicher_K p _)).
 
 (** Remark: It is reasonable to think that [eq_rect_eq] is strictly
     stronger than [eq_rec_eq] (which is [eq_rect_eq] restricted on [Set]):
@@ -317,7 +351,7 @@ Section Equivalences.
    [Definition Eq_rec_eq :=
       forall (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h.]
 
-    Typically, [eq_rect_eq] allows to prove UIP and Streicher's K what
+    Typically, [eq_rect_eq] allows proving UIP and Streicher's K what
     does not seem possible with [eq_rec_eq]. In particular, the proof of [UIP]
     requires to use [eq_rect_eq] on [fun y -> x=y] which is in [Type] but not
     in [Set].
@@ -325,22 +359,55 @@ Section Equivalences.
 
 End Equivalences.
 
+(** UIP_refl is downward closed (a short proof of the key lemma of Voevodsky's
+    proof of inclusion of h-level n into h-level n+1; see hlevelntosn
+    in https://github.com/vladimirias/Foundations.git). *)
+
+Theorem UIP_shift_on (X : Type) (x : X) :
+  UIP_refl_on_ X x -> forall y : x = x, UIP_refl_on_ (x = x) y.
+Proof.
+  intros UIP_refl y.
+  rewrite (UIP_refl y).
+  intros z.
+  assert (UIP:forall y' y'' : x = x, y' = y'').
+  { intros. apply eq_trans with (eq_refl x). apply UIP_refl.
+    symmetry. apply UIP_refl. }
+  transitivity (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z)
+                         (eq_sym (UIP (eq_refl x) (eq_refl x)))).
+  - destruct z. destruct (UIP _ _). reflexivity.
+  - change
+      (match eq_refl x as y' in _ = x' return y' = y' -> Prop with
+       | eq_refl => fun z => z = (eq_refl (eq_refl x))
+       end (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z)
+                     (eq_sym (UIP (eq_refl x) (eq_refl x))))).
+    destruct z. destruct (UIP _ _). reflexivity.
+Qed.
+Theorem UIP_shift : forall U, UIP_refl_ U -> forall x:U, UIP_refl_ (x = x).
+Proof (fun U UIP_refl x =>
+         @UIP_shift_on U x (UIP_refl x)).
+
 Section Corollaries.
 
   Variable U:Type.
 
   (** UIP implies the injectivity of equality on dependent pairs in Type *)
 
- Definition Inj_dep_pair :=
-   forall (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y.
 
- Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair.
+ Definition Inj_dep_pair_on (P : U -> Type) (p : U) (x : P p) :=
+   forall (y : P p), existT P p x = existT P p y -> x = y.
+ Definition Inj_dep_pair := forall P p x, Inj_dep_pair_on P p x.
+
+ Lemma eq_dep_eq_on__inj_pair2_on (P : U -> Type) (p : U) (x : P p) :
+   Eq_dep_eq_on U P p x -> Inj_dep_pair_on P p x.
  Proof.
    intro eq_dep_eq; red; intros.
    apply eq_dep_eq.
    apply eq_sigT_eq_dep.
    assumption.
  Qed.
+ Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair.
+ Proof (fun eq_dep_eq P p x =>
+          @eq_dep_eq_on__inj_pair2_on P p x (eq_dep_eq P p x)).
 
 End Corollaries.
 
@@ -412,5 +479,27 @@ Notation inj_pairT2 := inj_pair2.
 
 End EqdepTheory.
 
+(** Basic facts about eq_dep *)
+
+Lemma f_eq_dep :
+  forall U (P:U->Type) R p q x y (f:forall p, P p -> R p),
+    eq_dep p x q y -> eq_dep p (f p x) q (f q y).
+Proof.
+intros * []. reflexivity.
+Qed.
+
+Lemma eq_dep_non_dep :
+  forall U P p q x y, @eq_dep U (fun _ => P) p x q y -> x = y.
+Proof.
+intros * []. reflexivity.
+Qed.
+
+Lemma f_eq_dep_non_dep :
+  forall U (P:U->Type) R p q x y (f:forall p, P p -> R),
+    eq_dep p x q y -> f p x = f q y.
+Proof.
+intros * []. reflexivity.
+Qed.
+
 Arguments eq_dep  U P p x q _ : clear implicits.
 Arguments eq_dep1 U P p x q y : clear implicits.
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 015c7a5f..65011e8e 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -35,6 +35,7 @@ Table of contents:
 (** * Streicher's K and injectivity of dependent pair hold on decidable types *)
 
 Set Implicit Arguments.
+(* Set Universe Polymorphism. *)
 
 Section EqdepDec.
 
@@ -49,12 +50,12 @@ Section EqdepDec.
     case u; trivial.
   Qed.
 
-  Variable eq_dec : forall x y:A, x = y \/ x <> y.
-
   Variable x : A.
 
+  Variable eq_dec : forall y:A, x = y \/ x <> y.
+
   Let nu (y:A) (u:x = y) : x = y :=
-    match eq_dec x y with
+    match eq_dec y with
       | or_introl eqxy => eqxy
       | or_intror neqxy => False_ind _ (neqxy u)
     end.
@@ -62,17 +63,17 @@ Section EqdepDec.
   Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v.
     intros.
     unfold nu.
-    case (eq_dec x y); intros.
+    destruct (eq_dec y) as [Heq|Hneq].
     reflexivity.
 
-    case n; trivial.
+    case Hneq; trivial.
   Qed.
 
 
   Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (eq_refl x)) v.
 
 
-  Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u.
+  Remark nu_left_inv_on : forall (y:A) (u:x = y), nu_inv (nu u) = u.
   Proof.
     intros.
     case u; unfold nu_inv.
@@ -80,20 +81,20 @@ Section EqdepDec.
   Qed.
 
 
-  Theorem eq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2.
+  Theorem eq_proofs_unicity_on : forall (y:A) (p1 p2:x = y), p1 = p2.
   Proof.
     intros.
-    elim nu_left_inv with (u := p1).
-    elim nu_left_inv with (u := p2).
+    elim nu_left_inv_on with (u := p1).
+    elim nu_left_inv_on with (u := p2).
     elim nu_constant with y p1 p2.
     reflexivity.
   Qed.
 
-  Theorem K_dec :
+  Theorem K_dec_on :
     forall P:x = x -> Prop, P (eq_refl x) -> forall p:x = x, P p.
   Proof.
     intros.
-    elim eq_proofs_unicity with x (eq_refl x) p.
+    elim eq_proofs_unicity_on with x (eq_refl x) p.
     trivial.
   Qed.
 
@@ -101,27 +102,26 @@ Section EqdepDec.
 
   Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x :=
     match exP with
-      | ex_intro x' prf =>
-        match eq_dec x' x with
-          | or_introl eqprf => eq_ind x' P prf x eqprf
+      | ex_intro _ x' prf =>
+        match eq_dec x' with
+          | or_introl eqprf => eq_ind x' P prf x (eq_sym eqprf)
           | _ => def
         end
     end.
 
 
-  Theorem inj_right_pair :
+  Theorem inj_right_pair_on :
     forall (P:A -> Prop) (y y':P x),
       ex_intro P x y = ex_intro P x y' -> y = y'.
   Proof.
     intros.
     cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y).
     simpl.
-    case (eq_dec x x).
-    intro e.
-    elim e using K_dec; trivial.
+    destruct (eq_dec x) as [Heq|Hneq].
+    elim Heq using K_dec_on; trivial.
 
     intros.
-    case n; trivial.
+    case Hneq; trivial.
 
     case H.
     reflexivity.
@@ -129,6 +129,28 @@ Section EqdepDec.
 
 End EqdepDec.
 
+(** Now we prove the versions that require decidable equality for the entire type
+    rather than just on the given element.  The rest of the file uses this total
+    decidable equality.  We could do everything using decidable equality at a point
+    (because the induction rule for [eq] is really an induction rule for
+    [{ y : A | x = y }]), but we don't currently, because changing everything
+    would break backward compatibility and no-one has yet taken the time to define
+    the pointed versions, and then re-define the non-pointed versions in terms of
+    those. *)
+
+Theorem eq_proofs_unicity A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A)
+: forall (y:A) (p1 p2:x = y), p1 = p2.
+Proof (@eq_proofs_unicity_on A x (eq_dec x)).
+
+Theorem K_dec A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A)
+: forall P:x = x -> Prop, P (eq_refl x) -> forall p:x = x, P p.
+Proof (@K_dec_on A x (eq_dec x)).
+
+Theorem inj_right_pair A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A)
+: forall (P:A -> Prop) (y y':P x),
+    ex_intro P x y = ex_intro P x y' -> y = y'.
+Proof (@inj_right_pair_on A x (eq_dec x)).
+
 Require Import EqdepFacts.
 
 (** We deduce axiom [K] for (decidable) types *)
@@ -181,7 +203,7 @@ Unset Implicit Arguments.
 
 Module Type DecidableType.
 
-  Parameter U:Type.
+  Monomorphic Parameter U:Type.
   Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
 
 End DecidableType.
@@ -249,7 +271,7 @@ End DecidableEqDep.
 
 Module Type DecidableSet.
 
-  Parameter U:Type.
+  Parameter U:Set.
   Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
 
 End DecidableSet.
@@ -272,23 +294,23 @@ Module DecidableEqDepSet (M:DecidableSet).
 
   Theorem eq_dep_eq :
     forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y.
-  Proof N.eq_dep_eq.
+  Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq).
 
   (** Uniqueness of Identity Proofs (UIP) *)
 
   Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.
-  Proof N.UIP.
+  Proof (eq_dep_eq__UIP U eq_dep_eq).
 
   (** Uniqueness of Reflexive Identity Proofs *)
 
   Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x.
-  Proof N.UIP_refl.
+  Proof (UIP__UIP_refl U UIP).
 
   (** Streicher's axiom K *)
 
   Lemma Streicher_K :
     forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.
-  Proof N.Streicher_K.
+  Proof (K_dec_type eq_dec).
 
   (** Proof-irrelevance on subsets of decidable sets *)
 
@@ -318,7 +340,53 @@ Proof.
   intros A eq_dec.
   apply eq_dep_eq__inj_pair2.
   apply eq_rect_eq__eq_dep_eq.
-  unfold Eq_rect_eq.
-  apply eq_rect_eq_dec.
+  unfold Eq_rect_eq, Eq_rect_eq_on.
+  intros; apply eq_rect_eq_dec.
   apply eq_dec.
 Qed.
+
+  (** Examples of short direct proofs of unicity of reflexivity proofs
+      on specific domains *)
+
+Lemma UIP_refl_unit (x : tt = tt) : x = eq_refl tt.
+Proof.
+  change (match tt as b return tt = b -> Prop with
+          | tt => fun x => x = eq_refl tt
+          end x).
+  destruct x; reflexivity.
+Defined.
+
+Lemma UIP_refl_bool (b:bool) (x : b = b) : x = eq_refl.
+Proof.
+  destruct b.
+  - change (match true as b return true=b -> Prop with
+            | true => fun x => x = eq_refl
+            | _ => fun _ => True
+            end x).
+    destruct x; reflexivity.
+  - change (match false as b return false=b -> Prop with
+            | false => fun x => x = eq_refl
+            | _ => fun _ => True
+            end x).
+    destruct x; reflexivity.
+Defined.
+
+Lemma UIP_refl_nat (n:nat) (x : n = n) : x = eq_refl.
+Proof.
+  induction n.
+  - change (match 0 as n return 0=n -> Prop with
+            | 0 => fun x => x = eq_refl
+            | _ => fun _ => True
+            end x).
+    destruct x; reflexivity.
+  - specialize IHn with (f_equal pred x).
+    change eq_refl with (f_equal S (@eq_refl _ n)).
+    rewrite <- IHn; clear IHn.
+    change (match S n as n' return S n = n' -> Prop with
+            | 0 => fun _ => True
+            | S n' => fun x =>
+                x = f_equal S (f_equal pred x)
+            end x).
+  pattern (S n) at 2 3, x.
+  destruct x; reflexivity.
+Defined.
diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v
index 27fb147f..61ee9eb9 100644
--- a/theories/Logic/ExtensionalityFacts.v
+++ b/theories/Logic/ExtensionalityFacts.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/FinFun.v b/theories/Logic/FinFun.v
new file mode 100644
index 00000000..670aa219
--- /dev/null
+++ b/theories/Logic/FinFun.v
@@ -0,0 +1,400 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Functions on finite domains *)
+
+(** Main result : for functions [f:A->A] with finite [A],
+    f injective <-> f bijective <-> f surjective. *)
+
+Require Import List Compare_dec EqNat Decidable ListDec. Require Fin.
+Set Implicit Arguments.
+
+(** General definitions *)
+
+Definition Injective {A B} (f : A->B) :=
+ forall x y, f x = f y -> x = y.
+
+Definition Surjective {A B} (f : A->B) :=
+ forall y, exists x, f x = y.
+
+Definition Bijective {A B} (f : A->B) :=
+ exists g:B->A, (forall x, g (f x) = x) /\ (forall y, f (g y) = y).
+
+(** Finiteness is defined here via exhaustive list enumeration *)
+
+Definition Full {A:Type} (l:list A) := forall a:A, In a l.
+Definition Finite (A:Type) := exists (l:list A), Full l.
+
+(** In many following proofs, it will be convenient to have
+    list enumerations without duplicates. As soon as we have
+    decidability of equality (in Prop), this is equivalent
+    to the previous notion. *)
+
+Definition Listing {A:Type} (l:list A) := NoDup l /\ Full l.
+Definition Finite' (A:Type) := exists (l:list A), Listing l.
+
+Lemma Finite_alt A (d:decidable_eq A) : Finite A <-> Finite' A.
+Proof.
+ split.
+ - intros (l,F). destruct (uniquify d l) as (l' & N & I).
+   exists l'. split; trivial.
+   intros x. apply I, F.
+ - intros (l & _ & F). now exists l.
+Qed.
+
+(** Injections characterized in term of lists *)
+
+Lemma Injective_map_NoDup A B (f:A->B) (l:list A) :
+ Injective f -> NoDup l -> NoDup (map f l).
+Proof.
+ intros Ij. induction 1 as [|x l X N IH]; simpl; constructor; trivial.
+ rewrite in_map_iff. intros (y & E & Y). apply Ij in E. now subst.
+Qed.
+
+Lemma Injective_list_carac A B (d:decidable_eq A)(f:A->B) :
+  Injective f <-> (forall l, NoDup l -> NoDup (map f l)).
+Proof.
+ split.
+ - intros. now apply Injective_map_NoDup.
+ - intros H x y E.
+   destruct (d x y); trivial.
+   assert (N : NoDup (x::y::nil)).
+   { repeat constructor; simpl; intuition. }
+   specialize (H _ N). simpl in H. rewrite E in H.
+   inversion_clear H; simpl in *; intuition.
+Qed.
+
+Lemma Injective_carac A B (l:list A) : Listing l ->
+   forall (f:A->B), Injective f <-> NoDup (map f l).
+Proof.
+ intros L f. split.
+ - intros Ij. apply Injective_map_NoDup; trivial. apply L.
+ - intros N x y E.
+   assert (X : In x l) by apply L.
+   assert (Y : In y l) by apply L.
+   apply In_nth_error in X. destruct X as (i,X).
+   apply In_nth_error in Y. destruct Y as (j,Y).
+   assert (X' := map_nth_error f _ _ X).
+   assert (Y' := map_nth_error f _ _ Y).
+   assert (i = j).
+   { rewrite NoDup_nth_error in N. apply N.
+     - rewrite <- nth_error_Some. now rewrite X'.
+     - rewrite X', Y'. now f_equal. }
+   subst j. rewrite Y in X. now injection X.
+Qed.
+
+(** Surjection characterized in term of lists *)
+
+Lemma Surjective_list_carac A B (f:A->B):
+  Surjective f <-> (forall lB, exists lA, incl lB (map f lA)).
+Proof.
+ split.
+ - intros Su.
+   induction lB as [|b lB IH].
+   + now exists nil.
+   + destruct (Su b) as (a,E).
+     destruct IH as (lA,IC).
+     exists (a::lA). simpl. rewrite E.
+     intros x [X|X]; simpl; intuition.
+ - intros H y.
+   destruct (H (y::nil)) as (lA,IC).
+   assert (IN : In y (map f lA)) by (apply (IC y); now left).
+   rewrite in_map_iff in IN. destruct IN as (x & E & _).
+   now exists x.
+Qed.
+
+Lemma Surjective_carac A B : Finite B -> decidable_eq B ->
+  forall f:A->B, Surjective f <-> (exists lA, Listing (map f lA)).
+Proof.
+ intros (lB,FB) d. split.
+ - rewrite Surjective_list_carac.
+   intros Su. destruct (Su lB) as (lA,IC).
+   destruct (uniquify_map d f lA) as (lA' & N & IC').
+   exists lA'. split; trivial.
+   intro x. apply IC', IC, FB.
+ - intros (lA & N & FA) y.
+   generalize (FA y). rewrite in_map_iff. intros (x & E & _).
+   now exists x.
+Qed.
+
+(** Main result : *)
+
+Lemma Endo_Injective_Surjective :
+ forall A, Finite A -> decidable_eq A ->
+  forall f:A->A, Injective f <-> Surjective f.
+Proof.
+ intros A F d f. rewrite (Surjective_carac F d). split.
+ - apply (Finite_alt d) in F. destruct F as (l,L).
+   rewrite (Injective_carac L); intros.
+   exists l; split; trivial.
+   destruct L as (N,F).
+   assert (I : incl l (map f l)).
+   { apply NoDup_length_incl; trivial.
+     - now rewrite map_length.
+     - intros x _. apply F. }
+   intros x. apply I, F.
+ - clear F d. intros (l,L).
+   assert (N : NoDup l). { apply (NoDup_map_inv f), L. }
+   assert (I : incl (map f l) l).
+   { apply NoDup_length_incl; trivial.
+     - now rewrite map_length.
+     - intros x _. apply L. }
+   assert (L' : Listing l).
+   { split; trivial.
+     intro x. apply I, L. }
+   apply (Injective_carac L'), L.
+Qed.
+
+(** An injective and surjective function is bijective.
+    We need here stronger hypothesis : decidability of equality in Type. *)
+
+Definition EqDec (A:Type) := forall x y:A, {x=y}+{x<>y}.
+
+(** First, we show that a surjective f has an inverse function g such that
+    f.g = id. *)
+
+(* NB: instead of (Finite A), we could ask for (RecEnum A) with:
+Definition RecEnum A := exists h:nat->A, surjective h.
+*)
+
+Lemma Finite_Empty_or_not A :
+  Finite A -> (A->False) \/ exists a:A,True.
+Proof.
+ intros (l,F).
+ destruct l.
+ - left; exact F.
+ - right; now exists a.
+Qed.
+
+Lemma Surjective_inverse :
+  forall A B, Finite A -> EqDec B ->
+   forall f:A->B, Surjective f ->
+    exists g:B->A, forall x, f (g x) = x.
+Proof.
+ intros A B F d f Su.
+ destruct (Finite_Empty_or_not F) as [noA | (a,_)].
+ - (* A is empty : g is obtained via False_rect *)
+   assert (noB : B -> False). { intros y. now destruct (Su y). }
+   exists (fun y => False_rect _ (noB y)).
+   intro y. destruct (noB y).
+ - (* A is inhabited by a : we use it in Option.get *)
+   destruct F as (l,F).
+   set (h := fun x k => if d (f k) x then true else false).
+   set (get := fun o => match o with Some y => y | None => a end).
+   exists (fun x => get (List.find (h x) l)).
+   intros x.
+   case_eq (find (h x) l); simpl; clear get; [intros y H|intros H].
+   * apply find_some in H. destruct H as (_,H). unfold h in H.
+     now destruct (d (f y) x) in H.
+   * exfalso.
+     destruct (Su x) as (y & Y).
+     generalize (find_none _ l H y (F y)).
+     unfold h. now destruct (d (f y) x).
+Qed.
+
+(** Same, with more knowledge on the inverse function: g.f = f.g = id *)
+
+Lemma Injective_Surjective_Bijective :
+ forall A B, Finite A -> EqDec B ->
+  forall f:A->B, Injective f -> Surjective f -> Bijective f.
+Proof.
+ intros A B F d f Ij Su.
+ destruct (Surjective_inverse F d Su) as (g, E).
+ exists g. split; trivial.
+ intros y. apply Ij. now rewrite E.
+Qed.
+
+
+(** An example of finite type : [Fin.t] *)
+
+Lemma Fin_Finite n : Finite (Fin.t n).
+Proof.
+ induction n.
+ - exists nil.
+   red;inversion a.
+ - destruct IHn as (l,Hl).
+   exists (Fin.F1 :: map Fin.FS l).
+   intros a. revert n a l Hl.
+   refine (@Fin.caseS _ _ _); intros.
+   + now left.
+   + right. now apply in_map.
+Qed.
+
+(** Instead of working on a finite subset of nat, another
+    solution is to use restricted [nat->nat] functions, and
+    to consider them only below a certain bound [n]. *)
+
+Definition bFun n (f:nat->nat) := forall x, x < n -> f x < n.
+
+Definition bInjective n (f:nat->nat) :=
+ forall x y, x < n -> y < n -> f x = f y -> x = y.
+
+Definition bSurjective n (f:nat->nat) :=
+ forall y, y < n -> exists x, x < n /\ f x = y.
+
+(** We show that this is equivalent to the use of [Fin.t n]. *)
+
+Module Fin2Restrict.
+
+Notation n2f := Fin.of_nat_lt.
+Definition f2n {n} (x:Fin.t n) := proj1_sig (Fin.to_nat x).
+Definition f2n_ok n (x:Fin.t n) : f2n x < n := proj2_sig (Fin.to_nat x).
+Definition n2f_f2n : forall n x, n2f (f2n_ok x) = x := @Fin.of_nat_to_nat_inv.
+Definition f2n_n2f x n h : f2n (n2f h) = x := f_equal (@proj1_sig _ _) (@Fin.to_nat_of_nat x n h).
+Definition n2f_ext : forall x n h h', n2f h = n2f h' := @Fin.of_nat_ext.
+Definition f2n_inj : forall n x y, f2n x = f2n y -> x = y := @Fin.to_nat_inj.
+
+Definition extend n (f:Fin.t n -> Fin.t n) : (nat->nat) :=
+ fun x =>
+   match le_lt_dec n x with
+     | left _ => 0
+     | right h => f2n (f (n2f h))
+   end.
+
+Definition restrict n (f:nat->nat)(hf : bFun n f) : (Fin.t n -> Fin.t n) :=
+ fun x => let (x',h) := Fin.to_nat x in n2f (hf _ h).
+
+Ltac break_dec H :=
+ let H' := fresh "H" in
+ destruct le_lt_dec as [H'|H'];
+  [elim (Lt.le_not_lt _ _ H' H)
+  |try rewrite (n2f_ext H' H) in *; try clear H'].
+
+Lemma extend_ok n f : bFun n (@extend n f).
+Proof.
+ intros x h. unfold extend. break_dec h. apply f2n_ok.
+Qed.
+
+Lemma extend_f2n n f (x:Fin.t n) : extend f (f2n x) = f2n (f x).
+Proof.
+ generalize (n2f_f2n x). unfold extend, f2n, f2n_ok.
+ destruct (Fin.to_nat x) as (x',h); simpl.
+ break_dec h.
+ now intros ->.
+Qed.
+
+Lemma extend_n2f n f x (h:x<n) : n2f (extend_ok f h) = f (n2f h).
+Proof.
+ generalize (extend_ok f h). unfold extend in *. break_dec h. intros h'.
+ rewrite <- n2f_f2n. now apply n2f_ext.
+Qed.
+
+Lemma restrict_f2n n f hf (x:Fin.t n) :
+ f2n (@restrict n f hf x) = f (f2n x).
+Proof.
+ unfold restrict, f2n. destruct (Fin.to_nat x) as (x',h); simpl.
+ apply f2n_n2f.
+Qed.
+
+Lemma restrict_n2f n f hf x (h:x<n) :
+ @restrict n f hf (n2f h) = n2f (hf _ h).
+Proof.
+ unfold restrict. generalize (f2n_n2f h). unfold f2n.
+ destruct (Fin.to_nat (n2f h)) as (x',h'); simpl. intros ->.
+ now apply n2f_ext.
+Qed.
+
+Lemma extend_surjective n f :
+  bSurjective n (@extend n f) <-> Surjective f.
+Proof.
+ split.
+ - intros hf y.
+   destruct (hf _ (f2n_ok y)) as (x & h & Eq).
+   exists (n2f h).
+   apply f2n_inj. now rewrite <- Eq, <- extend_f2n, f2n_n2f.
+ - intros hf y hy.
+   destruct (hf (n2f hy)) as (x,Eq).
+   exists (f2n x).
+   split.
+   + apply f2n_ok.
+   + rewrite extend_f2n, Eq. apply f2n_n2f.
+Qed.
+
+Lemma extend_injective n f :
+  bInjective n (@extend n f) <-> Injective f.
+Proof.
+ split.
+ - intros hf x y Eq.
+   apply f2n_inj. apply hf; try apply f2n_ok.
+   now rewrite 2 extend_f2n, Eq.
+ - intros hf x y hx hy Eq.
+   rewrite <- (f2n_n2f hx), <- (f2n_n2f hy). f_equal.
+   apply hf.
+   rewrite <- 2 extend_n2f.
+   generalize (extend_ok f hx) (extend_ok f hy).
+   rewrite Eq. apply n2f_ext.
+Qed.
+
+Lemma restrict_surjective n f h :
+  Surjective (@restrict n f h) <-> bSurjective n f.
+Proof.
+ split.
+ - intros hf y hy.
+   destruct (hf (n2f hy)) as (x,Eq).
+   exists (f2n x).
+   split.
+   + apply f2n_ok.
+   + rewrite <- (restrict_f2n h), Eq. apply f2n_n2f.
+ - intros hf y.
+   destruct (hf _ (f2n_ok y)) as (x & hx & Eq).
+   exists (n2f hx).
+   apply f2n_inj. now rewrite restrict_f2n, f2n_n2f.
+Qed.
+
+Lemma restrict_injective n f h :
+  Injective (@restrict n f h) <-> bInjective n f.
+Proof.
+ split.
+ - intros hf x y hx hy Eq.
+   rewrite <- (f2n_n2f hx), <- (f2n_n2f hy). f_equal.
+   apply hf.
+   rewrite 2 restrict_n2f.
+   generalize (h x hx) (h y hy).
+   rewrite Eq. apply n2f_ext.
+ - intros hf x y Eq.
+   apply f2n_inj. apply hf; try apply f2n_ok.
+   now rewrite <- 2 (restrict_f2n h), Eq.
+Qed.
+
+End Fin2Restrict.
+Import Fin2Restrict.
+
+(** We can now use Proof via the equivalence ... *)
+
+Lemma bInjective_bSurjective n (f:nat->nat) :
+ bFun n f -> (bInjective n f <-> bSurjective n f).
+Proof.
+ intros h.
+ rewrite <- (restrict_injective h), <- (restrict_surjective h).
+ apply Endo_Injective_Surjective.
+ - apply Fin_Finite.
+ - intros x y. destruct (Fin.eq_dec x y); [left|right]; trivial.
+Qed.
+
+Lemma bSurjective_bBijective n (f:nat->nat) :
+ bFun n f -> bSurjective n f ->
+ exists g, bFun n g /\ forall x, x < n -> g (f x) = x /\ f (g x) = x.
+Proof.
+ intro hf.
+ rewrite <- (restrict_surjective hf). intros Su.
+ assert (Ij : Injective (restrict hf)).
+ { apply Endo_Injective_Surjective; trivial.
+   - apply Fin_Finite.
+   - intros x y. destruct (Fin.eq_dec x y); [left|right]; trivial. }
+ assert (Bi : Bijective (restrict hf)).
+ { apply Injective_Surjective_Bijective; trivial.
+   - apply Fin_Finite.
+   - exact Fin.eq_dec. }
+ destruct Bi as (g & Hg & Hg').
+ exists (extend g).
+ split.
+ - apply extend_ok.
+ - intros x Hx. split.
+   + now rewrite <- (f2n_n2f Hx), <- (restrict_f2n hf), extend_f2n, Hg.
+   + now rewrite <- (f2n_n2f Hx), extend_f2n, <- (restrict_f2n hf), Hg'.
+Qed.
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v
index 7d7792d5..eb50a3aa 100644
--- a/theories/Logic/FunctionalExtensionality.v
+++ b/theories/Logic/FunctionalExtensionality.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -19,6 +19,12 @@ Proof.
   auto.
 Qed.
 
+Lemma equal_f_dep : forall {A B} {f g : forall (x : A), B x},
+  f = g -> forall x, f x = g x.
+Proof.
+intros A B f g <- H; reflexivity.
+Qed.
+
 (** Statements of functional extensionality for simple and dependent functions. *)
 
 Axiom functional_extensionality_dep : forall {A} {B : A -> Type},
@@ -31,13 +37,35 @@ Proof.
   intros ; eauto using @functional_extensionality_dep.
 Qed.
 
+(** Extensionality of [forall]s follows from functional extensionality. *)
+Lemma forall_extensionality {A} {B C : A -> Type} (H : forall x : A, B x = C x)
+: (forall x, B x) = (forall x, C x).
+Proof.
+  apply functional_extensionality in H. destruct H. reflexivity.
+Defined.
+
+Lemma forall_extensionalityP {A} {B C : A -> Prop} (H : forall x : A, B x = C x)
+: (forall x, B x) = (forall x, C x).
+Proof.
+  apply functional_extensionality in H. destruct H. reflexivity.
+Defined.
+
+Lemma forall_extensionalityS {A} {B C : A -> Set} (H : forall x : A, B x = C x)
+: (forall x, B x) = (forall x, C x).
+Proof.
+  apply functional_extensionality in H. destruct H. reflexivity.
+Defined.
+
 (** Apply [functional_extensionality], introducing variable x. *)
 
 Tactic Notation "extensionality" ident(x) :=
   match goal with
     [ |- ?X = ?Y ] =>
     (apply (@functional_extensionality _ _ X Y) ||
-     apply (@functional_extensionality_dep _ _ X Y)) ; intro x
+     apply (@functional_extensionality_dep _ _ X Y) ||
+     apply forall_extensionalityP ||
+     apply forall_extensionalityS ||
+     apply forall_extensionality) ; intro x
   end.
 
 (** Eta expansion follows from extensionality. *)
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 95e98038..ede51f57 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,74 +8,686 @@
 (*                              Hurkens.v                               *)
 (************************************************************************)
 
-(** This is Hurkens paradox [Hurkens] in system U-, adapted by Herman
-    Geuvers [Geuvers] to show the inconsistency in the pure calculus of
-    constructions of a retract from Prop into a small type.
+(** Exploiting Hurkens's paradox [[Hurkens95]] for system U- so as to
+    derive various contradictory contexts.
+
+    The file is divided into various sub-modules which all follow the
+    same structure: a section introduces the contradictory hypotheses
+    and a theorem named [paradox] concludes the module with a proof of
+    [False].
+
+    - The [Generic] module contains the actual Hurkens's paradox for a
+      postulated shallow encoding of system U- in Coq. This is an
+      adaptation by Arnaud Spiwack of a previous, more restricted
+      implementation by Herman Geuvers. It is used to derive every
+      other special cases of the paradox in this file.
+
+    - The [NoRetractToImpredicativeUniverse] module contains a simple
+      and effective formulation by Herman Geuvers [[Geuvers01]] of a
+      result by Thierry Coquand [[Coquand90]]. It states that no
+      impredicative sort can contain a type of which it is a
+      retract. This result implies that Coq with classical logic
+      stated in impredicative Set is inconsistent and that classical
+      logic stated in Prop implies proof-irrelevance (see
+      [ClassicalFacts.v])
+
+    - The [NoRetractFromSmallPropositionToProp] module is a
+      specialisation of the [NoRetractToImpredicativeUniverse] module
+      to the case where the impredicative sort is [Prop].
+
+    - The [NoRetractToModalProposition] module is a strengthening of
+      the [NoRetractFromSmallPropositionToProp] module.  It shows that
+      given a monadic modality (aka closure operator) [M], the type of
+      modal propositions (i.e. such that [M A -> A]) cannot be a
+      retract of a modal proposition. It is an example of use of the
+      paradox where the universes of system U- are not mapped to
+      universes of Coq.
+
+    - The [NoRetractToNegativeProp] module is the specialisation of
+      the [NoRetractFromSmallPropositionToProp] module where the
+      modality is double-negation. This result implies that the
+      principle of weak excluded middle ([forall A, ~~A\/~A]) implies
+      a weak variant of proof irrelevance.
+
+    - The [NoRetractFromTypeToProp] module proves that [Prop] cannot
+      be a retract of a larger type.
+
+    - The [TypeNeqSmallType] module proves that [Type] is different
+      from any smaller type.
+
+    - The [PropNeqType] module proves that [Prop] is different from
+      any larger [Type]. It is an instance of the previous result.
 
     References:
 
-    - [Hurkens] A. J. Hurkens, "A simplification of Girard's paradox",
+    - [[Coquand90]] T. Coquand, "Metamathematical Investigations of a
+      Calculus of Constructions", Proceedings of Logic in Computer
+      Science (LICS'90), 1990.
+
+    - [[Hurkens95]] A. J. Hurkens, "A simplification of Girard's paradox",
       Proceedings of the 2nd international conference Typed Lambda-Calculi
       and Applications (TLCA'95), 1995.
 
-    - [Geuvers] "Inconsistency of Classical Logic in Type Theory", 2001
-      (see http://www.cs.kun.nl/~herman/note.ps.gz).
+    - [[Geuvers01]] H. Geuvers, "Inconsistency of Classical Logic in Type
+      Theory", 2001, revised 2007
+      (see {{http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz}}).
 *)
 
+
+Set Universe Polymorphism.
+
+(* begin show *)
+
+(** * A modular proof of Hurkens's paradox. *)
+
+(** It relies on an axiomatisation of a shallow embedding of system U-
+    (i.e.  types of U- are interpreted by types of Coq). The
+    universes are encoded in a style, due to Martin-Löf, where they
+    are given by a set of names and a family [El:Name->Type] which
+    interprets each name into a type. This allows the encoding of
+    universe to be decoupled from Coq's universes. Dependent products
+    and abstractions are similarly postulated rather than encoded as
+    Coq's dependent products and abstractions. *)
+
+Module Generic.
+
+(* begin hide *)
+(* Notations used in the proof. Hidden in coqdoc. *)
+
+Reserved Notation "'∀₁' x : A , B" (at level 200, x ident, A at level 200,right associativity).
+Reserved Notation "A '⟶₁' B" (at level 99, right associativity, B at level 200).
+Reserved Notation "'λ₁' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "f '·₁' x" (at level 5, left associativity).
+Reserved Notation "'∀₂' A , F" (at level 200, A ident, right associativity).
+Reserved Notation "'λ₂' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "f '·₁' [ A ]" (at level 5, left associativity).
+Reserved Notation "'∀₀' x : A , B" (at level 200, x ident, A at level 200,right associativity).
+Reserved Notation "A '⟶₀' B" (at level 99, right associativity, B at level 200).
+Reserved Notation "'λ₀' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "f '·₀' x" (at level 5, left associativity).
+Reserved Notation "'∀₀¹' A : U , F" (at level 200, A ident, right associativity).
+Reserved Notation "'λ₀¹' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "f '·₀' [ A ]" (at level 5, left associativity).
+
+(* end hide *)
+
+Section Paradox.
+
+(** ** Axiomatisation of impredicative universes in a Martin-Löf style *)
+
+(** System U- has two impredicative universes. In the proof of the
+    paradox they are slightly asymmetric (in particular the reduction
+    rules of the small universe are not needed).  Therefore, the
+    axioms are duplicated allowing for a weaker requirement than the
+    actual system U-. *)
+
+
+(** *** Large universe *)
+Variable U1 : Type.
+Variable El1 : U1 -> Type.
+(** **** Closure by small product *)
+Variable Forall1 : forall u:U1, (El1 u -> U1) -> U1.
+  Notation "'∀₁' x : A , B" := (Forall1 A (fun x => B)).
+  Notation "A '⟶₁' B" := (Forall1 A (fun _ => B)).
+Variable lam1 : forall u B, (forall x:El1 u, El1 (B x)) -> El1 (∀₁ x:u, B x).
+  Notation "'λ₁' x , u" := (lam1 _ _ (fun x => u)).
+Variable app1 : forall u B (f:El1 (Forall1 u B)) (x:El1 u), El1 (B x).
+  Notation "f '·₁' x" := (app1 _ _ f x).
+Variable beta1 : forall u B (f:forall x:El1 u, El1 (B x)) x,
+                   (λ₁ y, f y) ·₁ x = f x.
+(** **** Closure by large products *)
+(** [U1] only needs to quantify over itself. *)
+Variable ForallU1 : (U1->U1) -> U1.
+  Notation "'∀₂' A , F" := (ForallU1 (fun A => F)).
+Variable lamU1 : forall F, (forall A:U1, El1 (F A)) -> El1 (∀₂ A, F A).
+  Notation "'λ₂' x , u" := (lamU1 _ (fun x => u)).
+Variable appU1 : forall F (f:El1(∀₂ A,F A)) (A:U1), El1 (F A).
+  Notation "f '·₁' [ A ]" := (appU1 _ f A).
+Variable betaU1 : forall F (f:forall A:U1, El1 (F A)) A,
+                    (λ₂ x, f x) ·₁ [ A ] = f A.
+
+(** *** Small universe *)
+(** The small universe is an element of the large one. *)
+Variable u0 : U1.
+Notation U0 := (El1 u0).
+Variable El0 : U0 -> Type.
+(** **** Closure by small product *)
+(** [U0] does not need reduction rules *)
+Variable Forall0 : forall u:U0, (El0 u -> U0) -> U0.
+  Notation "'∀₀' x : A , B" := (Forall0 A (fun x => B)).
+  Notation "A '⟶₀' B" := (Forall0 A (fun _ => B)).
+Variable lam0 : forall u B, (forall x:El0 u, El0 (B x)) -> El0 (∀₀ x:u, B x).
+  Notation "'λ₀' x , u" := (lam0 _ _ (fun x => u)).
+Variable app0 : forall u B (f:El0 (Forall0 u B)) (x:El0 u), El0 (B x).
+  Notation "f '·₀' x" := (app0 _ _ f x).
+(** **** Closure by large products *)
+Variable ForallU0 : forall u:U1, (El1 u->U0) -> U0.
+  Notation "'∀₀¹' A : U , F" := (ForallU0 U (fun A => F)).
+Variable lamU0 : forall U F, (forall A:El1 U, El0 (F A)) -> El0 (∀₀¹ A:U, F A).
+  Notation "'λ₀¹' x , u" := (lamU0 _ _ (fun x => u)).
+Variable appU0 : forall U F (f:El0(∀₀¹ A:U,F A)) (A:El1 U), El0 (F A).
+  Notation "f '·₀' [ A ]" := (appU0 _ _ f A).
+
+(** ** Automating the rewrite rules of our encoding. *)
+Local Ltac simplify :=
+  (* spiwack: ideally we could use [rewrite_strategy] here, but I am a tad
+     scared of the idea of depending on setoid rewrite in such a simple
+     file. *)
+  (repeat rewrite ?beta1, ?betaU1);
+  lazy beta.
+
+Local Ltac simplify_in h :=
+  (repeat rewrite ?beta1, ?betaU1 in h);
+  lazy beta in h.
+
+
+(** ** Hurkens's paradox. *)
+
+(** An inhabitant of [U0] standing for [False]. *)
+Variable F:U0.
+
+(** *** Preliminary definitions *)
+
+Definition V : U1 := ∀₂ A, ((A ⟶₁ u0) ⟶₁ A ⟶₁ u0) ⟶₁ A ⟶₁ u0.
+Definition U : U1 := V ⟶₁ u0.
+
+Definition sb (z:El1 V) : El1 V := λ₂ A, λ₁ r, λ₁ a, r ·₁ (z·₁[A]·₁r) ·₁ a.
+
+Definition le (i:El1 (U⟶₁u0)) (x:El1 U) : U0 :=
+  x ·₁ (λ₂ A, λ₁ r, λ₁ a, i ·₁ (λ₁ v, (sb v) ·₁ [A] ·₁ r ·₁ a)).
+Definition le' : El1 ((U⟶₁u0) ⟶₁ U ⟶₁ u0) := λ₁ i, λ₁ x, le i x.
+Definition induct (i:El1 (U⟶₁u0)) : U0 :=
+  ∀₀¹ x:U, le i x ⟶₀ i ·₁ x.
+
+Definition WF : El1 U := λ₁ z, (induct (z·₁[U] ·₁ le')).
+Definition I (x:El1 U) : U0 :=
+  (∀₀¹ i:U⟶₁u0, le i x ⟶₀ i ·₁ (λ₁ v, (sb v) ·₁ [U] ·₁ le' ·₁ x)) ⟶₀ F
+.
+
+(** *** Proof *)
+
+Lemma Omega : El0 (∀₀¹ i:U⟶₁u0, induct i ⟶₀ i ·₁ WF).
+Proof.
+  refine (λ₀¹ i, λ₀ y, _).
+  refine (y·₀[_]·₀_).
+  unfold le,WF,induct. simplify.
+  refine (λ₀¹ x, λ₀ h0, _). simplify.
+  refine (y·₀[_]·₀_).
+  unfold le. simplify.
+  unfold sb at 1. simplify.
+  unfold le' at 1. simplify.
+  exact h0.
+Qed.
+
+Lemma lemma1 : El0 (induct (λ₁ u, I u)).
+Proof.
+  unfold induct.
+  refine (λ₀¹ x, λ₀ p, _). simplify.
+  refine (λ₀ q,_).
+  assert (El0 (I (λ₁ v, (sb v)·₁[U]·₁le'·₁x))) as h.
+  { generalize (q·₀[λ₁ u, I u]·₀p). simplify.
+    intros q'.
+    exact q'. }
+  refine (h·₀_).
+  refine (λ₀¹ i,_).
+  refine (λ₀ h', _).
+  generalize (q·₀[λ₁ y, i ·₁ (λ₁ v, (sb v)·₁[U] ·₁ le' ·₁ y)]). simplify.
+  intros q'.
+  refine (q'·₀_). clear q'.
+  unfold le at 1 in h'. simplify_in h'.
+  unfold sb at 1 in h'. simplify_in h'.
+  unfold le' at 1 in h'. simplify_in h'.
+  exact h'.
+Qed.
+
+Lemma lemma2 : El0 ((∀₀¹i:U⟶₁u0, induct i ⟶₀ i·₁WF) ⟶₀ F).
+Proof.
+  refine (λ₀ x, _).
+  assert (El0 (I WF)) as h.
+  { generalize (x·₀[λ₁ u, I u]·₀lemma1). simplify.
+    intros q.
+    exact q. }
+  refine (h·₀_). clear h.
+  refine (λ₀¹ i, λ₀ h0, _).
+  generalize (x·₀[λ₁ y, i·₁(λ₁ v, (sb v)·₁[U]·₁le'·₁y)]). simplify.
+  intros q.
+  refine (q·₀_). clear q.
+  unfold le in h0. simplify_in h0.
+  unfold WF in h0. simplify_in h0.
+  exact h0.
+Qed.
+
+Theorem paradox : El0 F.
+Proof.
+  exact (lemma2·₀Omega).
+Qed.
+
+End Paradox.
+
+(** The [paradox] tactic can be called as a shortcut to use the paradox. *)
+Ltac paradox h :=
+  refine ((fun h => _) (paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ));cycle 1.
+
+End Generic.
+
+(** * Impredicative universes are not retracts. *)
+
+(** There can be no retract to an impredicative Coq universe from a
+    smaller type. In this version of the proof, the impredicativity of
+    the universe is postulated with a pair of functions from the
+    universe to its type and back which commute with dependent product
+    in an appropriate way. *)
+
+Module NoRetractToImpredicativeUniverse.
+
 Section Paradox.
 
+Let      U2    := Type.
+Let      U1:U2 := Type.
+Variable U0:U1.
+
+(** *** [U1] is impredicative *)
+Variable u22u1 : U2 -> U1.
+Hypothesis u22u1_unit   : forall (c:U2), c -> u22u1 c.
+(** [u22u1_counit] and [u22u1_coherent] only apply to dependent
+    product so that the equations happen in the smaller [U1] rather
+    than [U2].  Indeed, it is not generally the case that one can
+    project from a large universe to an impredicative universe and
+    then get back the original type again. It would be too strong a
+    hypothesis to require (in particular, it is not true of
+    [Prop]). The formulation is reminiscent of the monadic
+    characteristic of the projection from a large type to [Prop].*)
+Hypothesis u22u1_counit : forall (F:U1->U1), u22u1 (forall A,F A) -> (forall A,F A).
+Hypothesis u22u1_coherent : forall (F:U1 -> U1) (f:forall x:U1, F x) (x:U1), 
+                              u22u1_counit _ (u22u1_unit _ f) x = f x.
+
+(** *** [U0] is a retract of [U1] *)
+Variable u02u1 : U0 -> U1.
+Variable u12u0 : U1 -> U0.
+Hypothesis u12u0_unit   : forall (b:U1), b -> u02u1 (u12u0 b).
+Hypothesis u12u0_counit : forall (b:U1), u02u1 (u12u0 b) -> b.
+
+(** ** Paradox *)
+
+Theorem paradox : forall F:U1, F.
+Proof.
+  intros F.
+  Generic.paradox h.
+  (** Large universe *)
+  + exact U1.
+  + exact (fun X => X).
+  + cbn. exact (fun u F => forall x:u, F x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. easy.
+  + cbn. exact (fun F => u22u1 (forall x, F x)).
+  + cbn. exact (fun _ x => u22u1_unit _ x).
+  + cbn. exact (fun _ x => u22u1_counit _ x).
+  + cbn. intros **. now rewrite u22u1_coherent.
+  (** Small universe *)
+  + exact U0.
+  (** The interpretation of the small universe is the image of
+      [U0] in [U1]. *)
+  + cbn. exact (fun X => u02u1 X).
+  + cbn. exact (fun u F => u12u0 (forall x:(u02u1 u), u02u1 (F x))).
+  + cbn. intros * x. exact (u12u0_unit _ x).
+  + cbn. intros * x. exact (u12u0_counit _ x).
+  + cbn. exact (fun u F => u12u0 (forall x:u, u02u1 (F x))).
+  + cbn. intros * x. exact (u12u0_unit _ x).
+  + cbn. intros * x. exact (u12u0_counit _ x).
+  + cbn. exact (u12u0 F).
+  + cbn in h.
+    exact (u12u0_counit _ h).
+Qed.
+
+End Paradox.
+
+End NoRetractToImpredicativeUniverse.
+
+(** * Prop is not a retract *)
+
+(** The existence in the pure Calculus of Constructions of a retract
+    from [Prop] into a small type of [Prop] is inconsistent. This is a
+    special case of the previous result. *)
+
+Module NoRetractFromSmallPropositionToProp.
+
+Section Paradox.
+
+(** ** Retract of [Prop] in a small type *)
+
+(** The retract is axiomatized using logical equivalence as the
+    equality on propositions. *)
+
 Variable bool : Prop.
 Variable p2b : Prop -> bool.
 Variable b2p : bool -> Prop.
 Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
 Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
-Variable B : Prop.
-
-Definition V := forall A:Prop, ((A -> bool) -> A -> bool) -> A -> bool.
-Definition U := V -> bool.
-Definition sb (z:V) : V := fun A r a => r (z A r) a.
-Definition le (i:U -> bool) (x:U) : bool :=
-  x (fun A r a => i (fun v => sb v A r a)).
-Definition induct (i:U -> bool) : Prop :=
-  forall x:U, b2p (le i x) -> b2p (i x).
-Definition WF : U := fun z => p2b (induct (z U le)).
-Definition I (x:U) : Prop :=
-  (forall i:U -> bool, b2p (le i x) -> b2p (i (fun v => sb v U le x))) -> B.
-
-Lemma Omega : forall i:U -> bool, induct i -> b2p (i WF).
+
+(** ** Paradox *)
+
+Theorem paradox : forall B:Prop, B.
 Proof.
-intros i y.
-apply y.
-unfold le, WF, induct.
-apply p2p2.
-intros x H0.
-apply y.
-exact H0.
+  intros B.
+  pose proof
+      (NoRetractToImpredicativeUniverse.paradox@{Type Prop}) as P.
+  refine (P _ _ _ _ _ _ _ _ _ _);clear P.
+  + exact bool.
+  + exact (fun x => forall P:Prop, (x->P)->P).
+  + cbn. exact (fun _ x P k => k x).
+  + cbn. intros F P x.
+    apply P.
+    intros f.
+    exact (f x).
+  + cbn. easy.
+  + exact b2p.
+  + exact p2b.
+  + exact p2p2.
+  + exact p2p1.
 Qed.
 
-Lemma lemma1 : induct (fun u => p2b (I u)).
+End Paradox.
+
+End NoRetractFromSmallPropositionToProp.
+
+(** * Modal fragments of [Prop] are not retracts *)
+
+(** In presence of a a monadic modality on [Prop], we can define a
+    subset of [Prop] of modal propositions which is also a complete
+    Heyting algebra. These cannot be a retract of a modal
+    proposition. This is a case where the universe in system U- are
+    not encoded as Coq universes. *)
+
+Module NoRetractToModalProposition.
+
+(** ** Monadic modality *)
+
+Section Paradox.
+
+Variable M : Prop -> Prop.
+Hypothesis unit : forall A:Prop, A -> M A.
+Hypothesis join : forall A:Prop, M (M A) -> M A.
+Hypothesis incr : forall A B:Prop, (A->B) -> M A -> M B.
+
+Lemma strength: forall A (P:A->Prop), M(forall x:A,P x) -> forall x:A,M(P x).
 Proof.
-unfold induct.
-intros x p.
-apply (p2p2 (I x)).
-intro q.
-apply (p2p1 (I (fun v:V => sb v U le x)) (q (fun u => p2b (I u)) p)).
-intro i.
-apply q with (i := fun y => i (fun v:V => sb v U le y)).
+  eauto.
 Qed.
 
-Lemma lemma2 : (forall i:U -> bool, induct i -> b2p (i WF)) -> B.
+(** ** The universe of modal propositions *)
+
+Definition MProp := { P:Prop | M P -> P }.
+Definition El : MProp -> Prop := @proj1_sig _ _.
+
+Lemma modal : forall P:MProp, M(El P) -> El P.
 Proof.
-intro x.
-apply (p2p1 (I WF) (x (fun u => p2b (I u)) lemma1)).
-intros i H0.
-apply (x (fun y => i (fun v => sb v U le y))).
-apply (p2p1 _ H0).
+  intros [P m]. cbn.
+  exact m.
 Qed.
 
-Theorem paradox : B.
+Definition Forall {A:Type} (P:A->MProp) : MProp.
+Proof.
+  refine (exist _ _ _).
+  + exact (forall x:A, El (P x)).
+  + intros h x.
+    eapply strength in h.
+    eauto using modal.
+Defined.
+
+(** ** Retract of the modal fragment of [Prop] in a small type *)
+
+(** The retract is axiomatized using logical equivalence as the
+    equality on propositions. *)
+
+Variable bool : MProp.
+Variable p2b : MProp -> El bool.
+Variable b2p : El bool -> MProp.
+Hypothesis p2p1 : forall A:MProp, El (b2p (p2b A)) -> El A.
+Hypothesis p2p2 : forall A:MProp, El A -> El (b2p (p2b A)).
+
+(** ** Paradox *)
+
+Theorem paradox : forall B:MProp, El B.
 Proof.
-exact (lemma2 Omega).
+  intros B.
+  Generic.paradox h.
+  (** Large universe *)
+  + exact MProp.
+  + exact El.
+  + exact (fun _ => Forall).
+  + cbn. exact (fun _ _ f => f).
+  + cbn. exact (fun _ _ f => f).
+  + cbn. easy.
+  + exact Forall.
+  + cbn. exact (fun _ f => f).
+  + cbn. exact (fun _ f => f).
+  + cbn. easy.
+  (** Small universe *)
+  + exact bool.
+  + exact (fun b => El (b2p b)).
+  + cbn. exact (fun _ F => p2b (Forall (fun x => b2p (F x)))).
+  + cbn. auto.
+  + cbn. intros * f.
+    apply p2p1 in f. cbn in f.
+    exact f.
+  + exact (fun _ F => p2b (Forall (fun x => b2p (F x)))).
+  + cbn. auto.
+  + cbn. intros * f.
+    apply p2p1 in f. cbn in f.
+    exact f.
+  + apply p2b.
+    exact B.
+  + cbn in h. auto.
 Qed.
 
 End Paradox.
+
+End NoRetractToModalProposition.
+
+(** * The negative fragment of [Prop] is not a retract *)
+
+(** The existence in the pure Calculus of Constructions of a retract
+    from the negative fragment of [Prop] into a negative proposition
+    is inconsistent. This is an instance of the previous result. *)
+
+Module NoRetractToNegativeProp.
+
+(** ** The universe of negative propositions. *)
+
+Definition NProp := { P:Prop | ~~P -> P }.
+Definition El : NProp -> Prop := @proj1_sig _ _.
+
+Section Paradox.
+
+(** ** Retract of the negative fragment of [Prop] in a small type *)
+
+(** The retract is axiomatized using logical equivalence as the
+    equality on propositions. *)
+
+Variable bool : NProp.
+Variable p2b : NProp -> El bool.
+Variable b2p : El bool -> NProp.
+Hypothesis p2p1 : forall A:NProp, El (b2p (p2b A)) -> El A.
+Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
+
+(** ** Paradox *)
+
+Theorem paradox : forall B:NProp, El B.
+Proof.
+  intros B.
+  refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _));cycle 1.
+  + exact (fun P => ~~P).
+  + cbn. auto.
+  + cbn. auto.
+  + cbn. auto.
+  + exact bool.
+  + exact p2b.
+  + exact b2p.
+  + auto.
+  + auto.
+  + exact B.
+  + exact h.
+Qed.
+
+End Paradox.
+
+End NoRetractToNegativeProp.
+
+(** * Large universes are no retracts of [Prop]. *)
+
+(** The existence in the Calculus of Constructions with universes of a
+    retract from some [Type] universe into [Prop] is inconsistent. *)
+
+(* Note: Assuming the context [down:Type->Prop; up:Prop->Type; forth:
+      forall (A:Type), A -> up (down A); back: forall (A:Type), up
+      (down A) -> A; H: forall (A:Type) (P:A->Type) (a:A),
+      P (back A (forth A a)) -> P a] is probably enough.  *)
+
+Module NoRetractFromTypeToProp.
+
+Definition Type2 := Type.
+Definition Type1 := Type : Type2.
+
+Section Paradox.
+
+(** ** Assumption of a retract from Type into Prop *)
+
+Variable down : Type1 -> Prop.
+Variable up : Prop -> Type1.
+Hypothesis up_down : forall (A:Type1), up (down A) = A :> Type1.
+
+(** ** Paradox *)
+
+Theorem paradox : forall P:Prop, P.
+Proof.
+  intros P.
+  Generic.paradox h.
+  (** Large universe. *)
+  + exact Type1.
+  + exact (fun X => X).
+  + cbn. exact (fun u F => forall x, F x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. easy.
+  + exact (fun F => forall A:Prop, F(up A)).
+  + cbn. exact (fun F f A => f (up A)).
+  + cbn.
+    intros F f A.
+    specialize (f (down A)).
+    rewrite up_down in f.
+    exact f.
+  + cbn.
+    intros F f A.
+    destruct (up_down A). cbn.
+    reflexivity.
+  + exact Prop.
+  + cbn. exact (fun X => X).
+  + cbn. exact (fun A P => forall x:A, P x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact (fun A P => forall x:A, P x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact P.
+  + exact h.
+Qed.
+
+End Paradox.
+
+End NoRetractFromTypeToProp.
+
+(** * [A<>Type] *)
+
+(** No Coq universe can be equal to one of its elements. *)
+
+Module TypeNeqSmallType.
+
+Section Paradox.
+
+(** ** Universe [U] is equal to one of its elements. *)
+
+Let U := Type.
+Variable A:U.
+Hypothesis h : U=A.
+
+(** ** Universe [U] is a retract of [A] *)
+
+(** The following context is actually sufficient for the paradox to
+    hold. The hypothesis [h:U=A] is only used to define [down], [up]
+    and [up_down]. *)
+
+Let down (X:U) : A := @eq_rect _ _ (fun X => X) X _ h.
+Let up   (X:A) : U := @eq_rect_r _ _ (fun X => X) X _ h.
+
+Lemma up_down : forall (X:U), up (down X) = X.
+Proof.
+  unfold up,down.
+  rewrite <- h.
+  reflexivity.
+Qed.
+
+
+Theorem paradox : False.
+Proof.
+  Generic.paradox p.
+  (** Large universe *)
+  + exact U.
+  + exact (fun X=>X).
+  + cbn. exact (fun X F => forall x:X, F x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. exact (fun _ _ x => x).
+  + cbn. easy.
+  + exact (fun F => forall x:A, F (up x)).
+  + cbn. exact (fun _ f => fun x:A => f (up x)).
+  + cbn. intros * f X.
+    specialize (f (down X)).
+    rewrite up_down in f.
+    exact f.
+  + cbn. intros ? f X.
+    destruct (up_down X). cbn.
+    reflexivity.
+  (** Small universe *)
+  + exact A.
+  (** The interpretation of [A] as a universe is [U]. *)
+  + cbn. exact up.
+  + cbn. exact (fun _ F => down (forall x, up (F x))).
+  + cbn. intros ? ? f.
+    rewrite up_down.
+    exact f.
+  + cbn. intros ? ? f.
+    rewrite up_down in f.
+    exact f.
+  + cbn. exact (fun _ F => down (forall x, up (F x))).
+  + cbn. intros ? ? f.
+    rewrite up_down.
+    exact f.
+  + cbn. intros ? ? f.
+    rewrite up_down in f.
+    exact f.
+  + cbn. exact (down False).
+  + rewrite up_down in p.
+    exact p.
+Qed.
+
+End Paradox.
+
+End TypeNeqSmallType.
+
+(** * [Prop<>Type]. *)
+
+(** Special case of [TypeNeqSmallType]. *)
+
+Module PropNeqType.
+
+Theorem paradox : Prop <> Type.
+Proof.
+  intros h.
+  refine (TypeNeqSmallType.paradox _ _).
+  + exact Prop.
+  + easy.
+Qed.
+
+End PropNeqType.
+
+(* end show *)
diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v
index 198b7292..9875710e 100644
--- a/theories/Logic/IndefiniteDescription.v
+++ b/theories/Logic/IndefiniteDescription.v
@@ -1,13 +1,13 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 (** This file provides a constructive form of indefinite description that
-    allows to build choice functions; this is weaker than Hilbert's
+    allows building choice functions; this is weaker than Hilbert's
     epsilon operator (which implies weakly classical properties) but
     stronger than the axiom of choice (which cannot be used outside
     the context of a theorem proof). *)
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 36e2d100..98cddf0a 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -28,9 +28,11 @@ Arguments JMeq_refl {A x} , [A] x.
 
 Hint Resolve JMeq_refl.
 
+Definition JMeq_hom {A : Type} (x y : A) := JMeq x y.
+
 Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
-Proof.
-destruct 1; trivial.
+Proof. 
+intros; destruct H; trivial.
 Qed.
 
 Hint Immediate JMeq_sym.
diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v
index 5cd58419..eb00dedd 100644
--- a/theories/Logic/ProofIrrelevance.v
+++ b/theories/Logic/ProofIrrelevance.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v
index b80cfe52..6ab6abcf 100644
--- a/theories/Logic/ProofIrrelevanceFacts.v
+++ b/theories/Logic/ProofIrrelevanceFacts.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -40,7 +40,7 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance).
   (** We derive the irrelevance of the membership property for subsets *)
 
   Lemma subset_eq_compat :
-    forall (U:Set) (P:U->Prop) (x y:U) (p:P x) (q:P y),
+    forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y),
       x = y -> exist P x p = exist P y q.
   Proof.
     intros.
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v
index 1f700c6c..61598130 100644
--- a/theories/Logic/RelationalChoice.v
+++ b/theories/Logic/RelationalChoice.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/SetIsType.v b/theories/Logic/SetIsType.v
index 412f8956..f110237e 100644
--- a/theories/Logic/SetIsType.v
+++ b/theories/Logic/SetIsType.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,7 +9,7 @@
 (** * The Set universe seen as a synonym for Type *)
 
 (** After loading this file, Set becomes just another name for Type.
-    This allows to easily perform a Set-to-Type migration, or at least
+    This allows easily performing a Set-to-Type migration, or at least
     test whether a development relies or not on specific features of
     Set: simply insert some Require Export of this file at starting
     points of the development and try to recompile...  *)
diff --git a/theories/Logic/WKL.v b/theories/Logic/WKL.v
new file mode 100644
index 00000000..408eca4a
--- /dev/null
+++ b/theories/Logic/WKL.v
@@ -0,0 +1,261 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** A constructive proof of a version of Weak König's Lemma over a
+    decidable predicate in the formulation of which infinite paths are
+    treated as predicates. The representation of paths as relations
+    avoid the need for classical logic and unique choice. The
+    decidability condition is sufficient to ensure that some required
+    instance of double negation for disjunction of finite paths holds.
+
+    The idea of the proof comes from the proof of the weak König's
+    lemma from separation in second-order arithmetic.
+
+    Notice that we do not start from a tree but just from an arbitrary
+    predicate. Original Weak Konig's Lemma is the instantiation of
+    the lemma to a tree *)
+
+Require Import WeakFan List.
+Import ListNotations.
+
+Require Import Omega.
+
+(** [is_path_from P n l] means that there exists a path of length [n]
+    from [l] on which [P] does not hold *)
+
+Inductive is_path_from (P:list bool -> Prop) : nat -> list bool -> Prop :=
+| here l : ~ P l -> is_path_from P 0 l
+| next_left l n : ~ P l -> is_path_from P n (true::l) -> is_path_from P (S n) l
+| next_right l n : ~ P l -> is_path_from P n (false::l) -> is_path_from P (S n) l.
+
+(** We give the characterization of is_path_from in terms of a more common arithmetical formula *)
+
+Proposition is_path_from_characterization P n l :
+  is_path_from P n l <-> exists l', length l' = n /\ forall n', n'<=n -> ~ P (rev (firstn n' l') ++ l).
+Proof.
+intros. split.
+- induction 1 as [|* HP _ (l'&Hl'&HPl')|* HP _ (l'&Hl'&HPl')].
+  + exists []. split. reflexivity. intros n <-/le_n_0_eq. assumption.
+  + exists (true :: l'). split. apply eq_S, Hl'. intros [|] H.
+    * assumption.
+    * simpl. rewrite <- app_assoc. apply HPl', le_S_n, H.
+  + exists (false :: l'). split. apply eq_S, Hl'. intros [|] H.
+    * assumption.
+    * simpl. rewrite <- app_assoc. apply HPl', le_S_n, H.
+- intros (l'& <- &HPl'). induction l' as [|[|]] in l, HPl' |- *.
+  + constructor. apply (HPl' 0). apply le_0_n.
+  + eapply next_left.
+    * apply (HPl' 0), le_0_n.
+    * fold (length l'). apply IHl'. intros n' H/le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption.
+  + apply next_right.
+    * apply (HPl' 0), le_0_n.
+    * fold (length l'). apply IHl'. intros n' H/le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption.
+Qed.
+
+(** [infinite_from P l] means that we can find arbitrary long paths
+    along which [P] does not hold above [l] *)
+
+Definition infinite_from (P:list bool -> Prop) l := forall n, is_path_from P n l.
+
+(** [has_infinite_path P] means that there is an infinite path
+    (represented as a predicate) along which [P] does not hold at all *)
+
+Definition has_infinite_path (P:list bool -> Prop) :=
+  exists (X:nat -> Prop), forall l, approx X l -> ~ P l.
+
+(** [inductively_barred_at P n l] means that [P] eventually holds above
+    [l] after at most [n] steps upwards *)
+
+Inductive inductively_barred_at (P:list bool -> Prop) : nat -> list bool -> Prop :=
+| now_at l n : P l -> inductively_barred_at P n l
+| propagate_at l n :
+    inductively_barred_at P n (true::l) ->
+    inductively_barred_at P n (false::l) ->
+    inductively_barred_at P (S n) l.
+
+(** The proof proceeds by building a set [Y] of finite paths
+   approximating either the smallest unbarred infinite path in [P], if
+   there is one (taking [true]>[false]), or the path
+   true::true::... if [P] happens to be inductively_barred *)
+
+Fixpoint Y P (l:list bool) :=
+  match l with
+  | [] => True
+  | b::l =>
+      Y P l /\
+      if b then exists n, inductively_barred_at P n (false::l) else infinite_from P (false::l)
+  end.
+
+Require Import Compare_dec Le Lt.
+
+Lemma is_path_from_restrict : forall P n n' l, n <= n' ->
+  is_path_from P n' l -> is_path_from P n l.
+Proof.
+intros * Hle H; induction H in n, Hle, H |- * ; intros.
+- apply le_n_0_eq in Hle as <-. apply here. assumption.
+- destruct n.
+  + apply here. assumption.
+  + apply next_left; auto using le_S_n.
+- destruct n.
+  + apply here. assumption.
+  + apply next_right; auto using le_S_n.
+Qed.
+
+Lemma inductively_barred_at_monotone : forall P l n n', n' <= n ->
+  inductively_barred_at P n' l -> inductively_barred_at P n l.
+Proof.
+intros * Hle Hbar.
+induction Hbar in n, l, Hle, Hbar |- *.
+- apply now_at; auto.
+- destruct n; [apply le_Sn_0 in Hle; contradiction|].
+  apply le_S_n in Hle.
+  apply propagate_at; auto.
+Qed.
+
+Definition demorgan_or (P:list bool -> Prop) l l' := ~ (P l /\ P l') -> ~ P l \/ ~ P l'.
+
+Definition demorgan_inductively_barred_at P :=
+  forall n l, demorgan_or (inductively_barred_at P n) (true::l) (false::l).
+
+Lemma inductively_barred_at_imp_is_path_from :
+  forall P, demorgan_inductively_barred_at P -> forall n l,
+  ~ inductively_barred_at P n l -> is_path_from P n l.
+Proof.
+intros P Hdemorgan; induction n; intros l H.
+- apply here.
+  intro. apply H.
+  apply now_at. auto.
+- assert (H0:~ (inductively_barred_at P n (true::l) /\ inductively_barred_at P n (false::l)))
+  by firstorder using inductively_barred_at.
+  assert (HnP:~ P l) by firstorder using inductively_barred_at.
+  apply Hdemorgan in H0 as [H0|H0]; apply IHn in H0; auto using is_path_from.
+Qed.
+
+Lemma is_path_from_imp_inductively_barred_at : forall P n l,
+   is_path_from P n l -> inductively_barred_at P n l -> False.
+Proof.
+intros P; induction n; intros l H1 H2.
+- inversion_clear H1. inversion_clear H2. auto.
+- inversion_clear H1.
+  + inversion_clear H2.
+    * auto.
+    * apply IHn with (true::l); auto.
+  + inversion_clear H2.
+    * auto.
+    * apply IHn with (false::l); auto.
+Qed.
+
+Lemma find_left_path : forall P l n,
+  is_path_from P (S n) l -> inductively_barred_at P n (false :: l) -> is_path_from P n (true :: l).
+Proof.
+inversion 1; subst; intros.
+- auto.
+- exfalso. eauto using is_path_from_imp_inductively_barred_at.
+Qed.
+
+Lemma Y_unique : forall P, demorgan_inductively_barred_at P ->
+  forall l1 l2, length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2.
+Proof.
+intros * DeMorgan. induction l1, l2.
+- trivial.
+- discriminate.
+- discriminate.
+- intros [= H] (HY1,H1) (HY2,H2).
+  pose proof (IHl1 l2 H HY1 HY2). clear HY1 HY2 H IHl1.
+  subst l1.
+  f_equal.
+  destruct a, b; try reflexivity.
+  + destruct H1 as (n,Hbar).
+    destruct (is_path_from_imp_inductively_barred_at _ _ _ (H2 n) Hbar).
+  + destruct H2 as (n,Hbar).
+    destruct (is_path_from_imp_inductively_barred_at _ _ _ (H1 n) Hbar).
+Qed.
+
+(** [X] is the translation of [Y] as a predicate *)
+
+Definition X P n := exists l, length l = n /\ Y P (true::l).
+
+Lemma Y_approx : forall P, demorgan_inductively_barred_at P ->
+  forall l, approx (X P) l -> Y P l.
+Proof.
+intros P DeMorgan. induction l.
+- trivial.
+- intros (H,Hb). split.
+  + auto.
+  + unfold X in Hb.
+    destruct a.
+    * destruct Hb as (l',(Hl',(HYl',HY))).
+      rewrite <- (Y_unique P DeMorgan l' l Hl'); auto.
+    * intro n. apply inductively_barred_at_imp_is_path_from. assumption.
+      firstorder.
+Qed.
+
+(** Main theorem *)
+
+Theorem PreWeakKonigsLemma : forall P,
+  demorgan_inductively_barred_at P -> infinite_from P [] -> has_infinite_path P.
+Proof.
+intros P DeMorgan Hinf.
+exists (X P). intros l Hl.
+assert (infinite_from P l).
+{ induction l.
+  - assumption.
+  - destruct Hl as (Hl,Ha).
+    intros n.
+    pose proof (IHl Hl) as IHl'. clear IHl.
+    apply Y_approx in Hl; [|assumption].
+    destruct a.
+    + destruct Ha as (l'&Hl'&HY'&n'&Hbar).
+      rewrite (Y_unique _ DeMorgan _ _ Hl' HY' Hl) in Hbar.
+      destruct (le_lt_dec n n') as [Hle|Hlt].
+      * specialize (IHl' (S n')).
+        apply is_path_from_restrict with n'; [assumption|].
+        apply find_left_path; trivial.
+      * specialize (IHl' (S n)).
+        apply inductively_barred_at_monotone with (n:=n) in Hbar; [|apply lt_le_weak, Hlt].
+        apply find_left_path; trivial.
+    + apply inductively_barred_at_imp_is_path_from; firstorder. }
+specialize (H 0). inversion H. assumption.
+Qed.
+
+Lemma inductively_barred_at_decidable :
+  forall P, (forall l, P l \/ ~ P l) -> forall n l, inductively_barred_at P n l \/ ~ inductively_barred_at P n l.
+Proof.
+intros P HP. induction n; intros.
+- destruct (HP l).
+  + left. apply now_at, H.
+  + right. inversion 1. auto.
+- destruct (HP l).
+  + left. apply now_at, H.
+  + destruct (IHn (true::l)).
+    * destruct (IHn (false::l)).
+      { left. apply propagate_at; assumption. }
+      { right. inversion_clear 1; auto. }
+    * right. inversion_clear 1; auto.
+Qed.
+
+Lemma inductively_barred_at_is_path_from_decidable :
+  forall P, (forall l, P l \/ ~ P l) -> demorgan_inductively_barred_at P.
+Proof.
+intros P Hdec n l H.
+destruct (inductively_barred_at_decidable P Hdec n (true::l)).
+- destruct (inductively_barred_at_decidable P Hdec n (false::l)).
+  + auto.
+  + auto.
+- auto.
+Qed.
+
+(** Main corollary *)
+
+Corollary WeakKonigsLemma : forall P, (forall l, P l \/ ~ P l) ->
+  infinite_from P [] -> has_infinite_path P.
+Proof.
+intros P Hdec Hinf.
+apply inductively_barred_at_is_path_from_decidable in Hdec.
+apply PreWeakKonigsLemma; assumption.
+Qed.
diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v
new file mode 100644
index 00000000..49cc12b8
--- /dev/null
+++ b/theories/Logic/WeakFan.v
@@ -0,0 +1,105 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** A constructive proof of a non-standard version of the weak Fan Theorem
+    in the formulation of which infinite paths are treated as
+    predicates. The representation of paths as relations avoid the
+    need for classical logic and unique choice. The idea of the proof
+    comes from the proof of the weak König's lemma from separation in
+    second-order arithmetic [[Simpson99]].
+
+    [[Simpson99]] Stephen G. Simpson. Subsystems of second order
+    arithmetic, Cambridge University Press, 1999 *)
+
+Require Import List.
+Import ListNotations.
+
+(** [inductively_barred P l] means that P eventually holds above l *)
+
+Inductive inductively_barred P : list bool -> Prop :=
+| now l : P l -> inductively_barred P l
+| propagate l :
+    inductively_barred P (true::l) ->
+    inductively_barred P (false::l) ->
+    inductively_barred P l.
+
+(** [approx X l] says that [l] is a boolean representation of a prefix of [X] *)
+
+Fixpoint approx X (l:list bool) :=
+  match l with
+  | [] => True
+  | b::l => approx X l /\ (if b then X (length l) else ~ X (length l))
+  end.
+
+(** [barred P] means that for any infinite path represented as a predicate,
+    the property [P] holds for some prefix of the path *)
+
+Definition barred P :=
+  forall (X:nat -> Prop), exists l, approx X l /\ P l.
+
+(** The proof proceeds by building a set [Y] of finite paths
+   approximating either the smallest unbarred infinite path in [P], if
+   there is one (taking [true]>[false]), or the path [true::true::...]
+   if [P] happens to be inductively_barred *)
+
+Fixpoint Y P (l:list bool) :=
+  match l with
+  | [] => True
+  | b::l =>
+      Y P l /\
+      if b then inductively_barred P (false::l) else ~ inductively_barred P (false::l)
+  end.
+
+Lemma Y_unique : forall P l1 l2, length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2.
+Proof.
+induction l1, l2.
+- trivial.
+- discriminate.
+- discriminate.
+- intros H (HY1,H1) (HY2,H2).
+  injection H as H.
+  pose proof (IHl1 l2 H HY1 HY2). clear HY1 HY2 H IHl1.
+  subst l1.
+  f_equal.
+  destruct a, b; firstorder.
+Qed.
+
+(** [X] is the translation of [Y] as a predicate *)
+
+Definition X P n := exists l, length l = n /\ Y P (true::l).
+
+Lemma Y_approx : forall P l, approx (X P) l -> Y P l.
+Proof.
+induction l.
+- trivial.
+- intros (H,Hb). split.
+  + auto.
+  + unfold X in Hb.
+    destruct a.
+    * destruct Hb as (l',(Hl',(HYl',HY))).
+      rewrite <- (Y_unique P l' l Hl'); auto.
+    * firstorder.
+Qed.
+
+Theorem WeakFanTheorem : forall P, barred P -> inductively_barred P [].
+Proof.
+intros P Hbar.
+destruct (Hbar (X P)) as (l,(Hd,HP)).
+assert (inductively_barred P l) by (apply (now P l), HP).
+clear Hbar HP.
+induction l.
+- assumption.
+- destruct Hd as (Hd,HX).
+  apply (IHl Hd). clear IHl.
+  destruct a; unfold X in HX; simpl in HX.
+  + apply propagate.
+    * apply H.
+    * destruct HX as (l',(Hl,(HY,Ht))); firstorder.
+      apply Y_approx in Hd. rewrite <- (Y_unique P l' l Hl); trivial.
+  + destruct HX. exists l. split; auto using Y_approx.
+Qed.
diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget
index 46046897..32359739 100644
--- a/theories/Logic/vo.itarget
+++ b/theories/Logic/vo.itarget
@@ -4,10 +4,8 @@ ClassicalChoice.vo
 ClassicalDescription.vo
 ClassicalEpsilon.vo
 ClassicalFacts.vo
-Classical_Pred_Set.vo
 Classical_Pred_Type.vo
 Classical_Prop.vo
-Classical_Type.vo
 ClassicalUniqueChoice.vo
 Classical.vo
 ConstructiveEpsilon.vo
@@ -18,7 +16,10 @@ Epsilon.vo
 Eqdep_dec.vo
 EqdepFacts.vo
 Eqdep.vo
+WeakFan.vo
+WKL.vo
 FunctionalExtensionality.vo
+ExtensionalityFacts.vo
 Hurkens.vo
 IndefiniteDescription.vo
 JMeq.vo
@@ -26,3 +27,4 @@ ProofIrrelevanceFacts.vo
 ProofIrrelevance.vo
 RelationalChoice.vo
 SetIsType.vo
+FinFun.vo
\ No newline at end of file