diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-26 18:43:05 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-26 18:43:42 +0200 |
| commit | 1dccd3509f62560c0a48189f5a3b67ab195deab0 (patch) | |
| tree | 06b84af32269d409869a8b84889a69548a6a5761 /theories/Logic | |
| parent | dd21327dbc388dfbff88834ae628df062b1b7c04 (diff) | |
Hurkens.v: Fix a syntax error.
Introduced in c74a70a73b3bf39394c551f1cdb224450bf77176.
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/Hurkens.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index aea171af6..34dc954ec 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -199,7 +199,7 @@ Definition le' : El1 ((U⟶₁u0) ⟶₁ U ⟶₁ u0) := λ₁ i, λ₁ x, le i Definition induct (i:El1 (U⟶₁u0)) : U0 := ∀₀¹ x:U, le i x ⟶₀ i ·₁ x. -Definition WF : El1 U := λ₁b z, (induct (z·₁[U] ·₁ le')). +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 . |