blob: 1e6e9b30de74343da8e8d8b10f39bcf3e1e8fc96 (
plain)
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
|
(* -*- coq-prog-args: ("-allow-sprop"); -*- *)
Set Universe Polymorphism.
Inductive False : SProp :=.
Axiom ℙ@{} : SProp.
Definition TYPE@{i} := ℙ -> Type@{i}.
Definition PROP@{} := ℙ -> SProp.
Definition El@{i} (A : TYPE@{i}) := forall p, A p.
Definition sEl@{} (A : PROP@{}) : SProp := forall p, A p.
Definition SPropᶠ@{} := fun (p : ℙ) => SProp.
Definition sProdᶠ@{i}
(A : TYPE@{i})
(B : forall (p : ℙ), El A -> SProp) : PROP := fun (p : ℙ) => forall x : El A, B p x.
Definition Falseᶠ : El SPropᶠ := fun p => False.
Definition EMᶠ : sEl (sProdᶠ SPropᶠ (fun p A => ((sProdᶠ A (fun p _ => Falseᶠ p))) p)).
Proof.
Fail Admitted.
Abort.
|
