1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
Set Definitional UIP.
Inductive seq {A} (a:A) : A -> SProp :=
srefl : seq a a.
Arguments srefl {_ _}.
(* Axiom implied by propext (so consistent) *)
Axiom all_eq : forall (P Q:Prop), P -> Q -> seq P Q.
Definition transport (P Q:Prop) (x:P) (y:Q) : Q
:= match all_eq P Q x y with srefl => x end.
Definition top : Prop := forall P : Prop, P -> P.
Definition c : top :=
fun P p =>
transport
(top -> top)
P
(fun x : top => x (top -> top) (fun x => x) x)
p.
Fail Timeout 1 Eval lazy in c (top -> top) (fun x => x) c.
(* loops *)
|
