1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
(* the only way to compute zero is for p to become canonical.
The only canonical member of A=A is eq_refl.
However, it is impossible to that p is propositionally equal to eq_refl.
In particular the univalence axiom allows for non-refl proofs. *)
Fixpoint zero (A : Set) (p : A = A) {struct p} : nat := 0.
(* although this axiom breaks canonicity, it is believed to be consistent *)
Axiom strong_exm : Set -> nat.
Axiom strong_exm_true : strong_exm True = 0.
Axiom strong_exm_false : strong_exm False = 1.
(* same type as [zero] above, but provably non parametric *)
Definition nonParam (A : Set) (p : A = A) : nat := strong_exm A.
(* because zero cannot be unfolded, it seems safe to assume the following *)
Axiom zeroOpaque :(forall x, zero x = nonParam x).
Inductive eq_R (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) (x₁ : A₁) (x₂ : A₂)
(x_R : A_R x₁ x₂)
: forall (H : A₁) (H0 : A₂), A_R H H0 -> x₁ = H -> x₂ = H0 -> Prop :=
eq_refl_R : eq_R A₁ A₂ A_R x₁ x₂ x_R x₁ x₂ x_R eq_refl eq_refl.
Lemma zero_not_parametric :
(forall (A₁ A₂ : Set) (A_R : A₁ -> A₂ -> Set) (p₁ : A₁ = A₁) (p₂ : A₂ = A₂),
eq_R Set Set (fun H1 H2 : Set => H1 -> H2 -> Set) A₁ A₂ A_R A₁ A₂ A_R p₁
p₂ -> (zero A₁ p₁) = (zero A₂ p₂)) -> False.
Proof using.
intros Hc.
specialize (Hc True False (fun _ _ => True) eq_refl eq_refl).
do 2 rewrite zeroOpaque in Hc.
unfold nonParam in Hc. simpl in Hc.
rewrite strong_exm_true in Hc.
rewrite strong_exm_false in Hc.
specialize (Hc (@eq_refl_R _ _ _ _ _ _)).
discriminate.
Qed.
|
