---

Lemma: simp_lemma1
∀[P:ℙ]. (P supposing False ⇐⇒ True)

Lemma: ite_false
∀b:𝔹. ∀[x:ℙ]. (if b then x else False fi  ⇐⇒ (↑b) ∧ x)

Lemma: iflift_1
∀[A,B:Type]. ∀[c:𝔹]. ∀[f:A ⟶ B]. ∀[x,y:A].  (f[if c then x else y fi ] = if c then f[x] else f[y] fi  ∈ B)

Lemma: iflift_sq_1
∀[c:𝔹]. ∀[f,x,y:Top].  (f[if c then x else y fi ] ~ if c then f[x] else f[y] fi )

Lemma: cand_functionality_wrt_iff
∀[a1,a2,b1,b2:ℙ].  ((a1 ⇐⇒ a2) ⇒ (b1 ⇐⇒ b2) ⇒ (a1 c∧ b1 ⇐⇒ a2 c∧ b2))

Lemma: trivial_ite_2
∀[b:𝔹]. ∀[a:Top].  (if b then a else a fi  ~ a)

Lemma: ite_and_reduce
∀[b1,b2:𝔹]. ∀[x,y:Top].  (if b1 then if b2 then x else y fi  else y fi  ~ if b1 ∧b b2 then x else y fi )

Definition: hide
HIDDEN ==  x

Lemma: hide_wf
∀[T:Type]. ∀[x:T].  (HIDDEN ∈ T)

Definition: !hyp_hide
x ==  x

Definition: opt
(b?x) ==  if b then inl x else inr ⋅  fi 

Lemma: opt_wf
∀[T:Type]. ∀[x:T]. ∀[b:𝔹].  ((b?x) ∈ T?)

Definition: Russell
Russell ==  {T:Type ⋂ Base| ¬(T ∈ T)} 

Lemma: Russell_wf
Russell ∈ 𝕌'

Lemma: Russell-property
¬(Russell ∈ Russell)

Lemma: Russell-paradox
¬(𝕌' ⊆r Type)

Lemma: Russell-theorem
¬(Type ∈ Type)

Lemma: Russell-theorem-take2
¬(Type ∈ Type)

Lemma: Russell-theorem-ext
¬(Type ∈ Type)

Definition: decision
Decision ==  Top + Top

Lemma: decision_wf
Decision ∈ Type

Definition: dec2bool
dec2bool(d) ==  case d of inl(x) => tt | inr(x) => ff

Lemma: dec2bool_wf
∀[d:Decision]. (dec2bool(d) ∈ 𝔹)

Lemma: inr_eq_bfalse
∀[x:Top]. ((inr x ) = ff ∈ Decision)

Lemma: inl_eq_btrue
∀[x:Top]. ((inl x) = tt ∈ Decision)

Lemma: bool_decision
∀[x:𝔹]. (x ∈ Decision)

Lemma: decidable_decision
∀[P:ℙ]. ∀[x:Dec(P)].  (x ∈ Decision)

Lemma: dec2bool_decidable
∀[P:ℙ]. ∀p:Dec(P). {↑dec2bool(p) ⇐⇒ P}

Lemma: eqtt_assert_2
∀[b:Decision]. uiff(b = tt ∈ Decision;↑b)

Lemma: eqff_assert_2
∀[b:Decision]. uiff(b = ff ∈ Decision;¬↑b)

Lemma: assert_dec2bool
∀[d:Decision]. uiff(↑dec2bool(d);↑d)

Lemma: decidable__cand
∀[P:ℙ]. ∀[Q:⋂x:P. ℙ].  (Dec(P) ⇒ (P ⇒ Dec(Q)) ⇒ Dec(P c∧ Q))

Definition: limited-omniscience
The limited principle of omniscience (LPO) is a simple, classically true, 
proposition that is not true in intuitionistic mathematics.
It contradicts even a weak form of Brouwer's continutity principle.
Nuprl satisfies strong versions of continuity 
(see rules--proved true in the Nuprl-in-Coq model--
StrongContinuity2 and weak continuity rule Continuity).
Therfore we can prove the negation of LPO:
no-weak-limited-omniscience  
no-limited-omniscience.⋅

LPO ==  ∀f:ℕ ⟶ 𝔹. ((∀n:ℕ. f n = ff) ∨ (∃n:ℕ. f n = tt))

Lemma: limited-omniscience_wf
LPO ∈ ℙ

Definition: type-functor
Functor ==
  {p:F:Type ⟶ Type × (⋂T,S:Type.  ((T ⟶ S) ⟶ (F T) ⟶ (F S)))| 
   let F,M = p 
   in (∀T:Type. ((M (λx.x)) = (λx.x) ∈ ((F T) ⟶ (F T))))
      ∧ (∀T,S,V:Type. ∀f:T ⟶ S. ∀g:S ⟶ V.  ((M (g o f)) = ((M g) o (M f)) ∈ ((F T) ⟶ (F V))))} 

Lemma: type-functor_wf
Functor ∈ 𝕌'

Definition: identity-functor
Id ==  <λx.x, λf.f>

Lemma: identity-functor_wf
Id ∈ Functor

Definition: constant-type-functor
constant-type-functor(X) ==  <λT.X, λf,x. x>

Lemma: constant-type-functor_wf
∀[X:Type]. (constant-type-functor(X) ∈ Functor)

Definition: type-functor-product
p * q ==  let F,MF = p in let G,MG = q in <λT.(F T × (G T)), λf,p. let x,y = p in <MF f x, MG f y>>

Lemma: type-functor-product_wf
∀[F,G:Functor].  (F * G ∈ Functor)

Definition: type-functor-sum
p + q ==
  let F,MF = p 
  in let G,MG = q 
     in <λT.(F T + (G T)), λf,d. case d of inl(x) => inl (MF f x) | inr(y) => inr (MG f y) >

Lemma: type-functor-sum_wf
∀[F,G:Functor].  (F + G ∈ Functor)

Definition: type-functor-compose
p o q ==  let F,MF = p in let G,MG = q in <F o G, MF o MG>

Lemma: type-functor-compose_wf
∀[F,G:Functor].  (F o G ∈ Functor)

Definition: type-functor-iterate
F^n ==  primrec(n;Id;λi,G. (F o G))

Lemma: type-functor-iterate_wf
∀[n:ℕ]. ∀[F:Functor].  (F^n ∈ Functor)

Definition: compact-type
compact-type(T) ==  ∀p:T ⟶ 𝔹. ((∃x:T. p x = ff) ∨ (∀x:T. p x = tt))

Lemma: compact-type_wf
∀[T:Type]. (compact-type(T) ∈ ℙ)

Definition: p-selector
y is a "root" of the decidable property p
if p y = ff  
(thinking of ff as being 0 and tt as non-zero).

x is a selector for decidable property p if
x is a root of p if and only if p has a root.
( a non-void, compact type T has a selector
  see: compact-type-compact-type2)⋅

p-selector(T;x;p) ==  (∃y:T. p y = ff) ⇒ p x = ff

Lemma: p-selector_wf
∀[T:Type]. ∀[x:T]. ∀[p:T ⟶ 𝔹].  (p-selector(T;x;p) ∈ ℙ)

Definition: compact-type2
compact-type2(T) ==  ∀p:T ⟶ 𝔹. (∃x:T [p-selector(T;x;p)])

Lemma: compact-type2_wf
∀[T:Type]. (compact-type2(T) ∈ ℙ)

Lemma: compact-type-compact-type2
∀[T:Type]. (compact-type(T) ∧ T ⇐⇒ compact-type2(T))

Lemma: compact-type-corec-lemma0
∀[F:Type ⟶ Type]
  (Monotone(T.F T)
  ⇒ (((⋂n:ℕ. (F^n Top)) ⟶ 𝔹) ⊆r ⋃n:ℕ.((F^n Top) ⟶ 𝔹))
  ⇒ ((⋂n:ℕ. compact-type2(F^n Top)) ⊆r compact-type2(corec(T.F T))))

Lemma: compact-type-corec-lemma1
∀[F:Type ⟶ Type]
  (Monotone(T.F T)
  ⇒ (((⋂n:ℕ. (F^n Top)) ⟶ 𝔹) ⊆r ⋃n:ℕ.((F^n Top) ⟶ 𝔹))
  ⇒ (∀[T:Type]. (compact-type2(T) ⇒ compact-type2(F T)))
  ⇒ compact-type2(corec(T.F T)))

Lemma: compact-product
∀[T:Type]. ∀[S:T ⟶ Type].  (compact-type(T) ⇒ (∀t:T. compact-type(S[t])) ⇒ compact-type(t:T × S[t]))

Lemma: compact-union
∀[T,S:Type].  (compact-type(T) ⇒ compact-type(S) ⇒ compact-type(T + S))

Lemma: compact-finite
∀n:ℕ. compact-type(ℕn)

Lemma: compact_functionality_wrt_surject
∀[T,S:Type].  ((∃f:T ⟶ S. Surj(T;S;f)) ⇒ compact-type(T) ⇒ compact-type(S))

Lemma: compact_functionality_wrt_equipollent
∀[T,S:Type].  (T ~ S ⇒ compact-type(T) ⇒ compact-type(S))

Lemma: decidable__equal_compact_domain
∀[T,S:Type].  ((∀a,b:S.  Dec(a = b ∈ S)) ⇒ compact-type(T) ⇒ (∀f,g:T ⟶ S.  Dec(f = g ∈ (T ⟶ S))))

Lemma: CCC-compact
∀K:Type. (CCCNSet(K) ⇒ compact-type(K))

Lemma: compact-dCCC
∀K:Type. (K ⇒ compact-type(K) ⇒ dCCC(K))

Definition: weak-continuity
weak-continuity(T;V) ==
  ∀F:(ℕ ⟶ T) ⟶ V. ∀f:ℕ ⟶ T.  (↓∃n:ℕ. ∀g:ℕ ⟶ T. ((∀i:ℕn. ((f i) = (g i) ∈ T)) ⇒ ((F f) = (F g) ∈ V)))

Lemma: weak-continuity_wf
∀[T,V:Type].  (weak-continuity(T;V) ∈ ℙ)

Lemma: weak-continuity-bool-bool
weak-continuity(𝔹;𝔹)

Lemma: no-weak-limited-omniscience
¬(∀f:ℕ ⟶ 𝔹. Dec(∀n:ℕ. f n = ff))

Lemma: no-limited-omniscience
¬LPO

Definition: nat-inf
ℕ∞ ==  {f:ℕ ⟶ 𝔹| ∀n:ℕ. ((↑(f (n + 1))) ⇒ (↑(f n)))} 

Lemma: nat-inf_wf
ℕ∞ ∈ Type

Definition: nat2inf
n∞ ==  λi.i <z n

Lemma: nat2inf_wf
∀[n:ℕ]. (n∞ ∈ ℕ∞)

Lemma: nat2inf-one-one
∀[a,b:ℕ].  ((a∞ = b∞ ∈ ℕ∞) ⇒ (a = b ∈ ℕ))

Lemma: nat2inf-injection
Inj(ℕ;ℕ∞;λn.n∞)

Definition: nat-inf-infinity
∞ ==  λn.tt

Lemma: nat-inf-infinity_wf
∞ ∈ ℕ∞

Lemma: nat-inf-infinity-new
∀[n:ℕ]. (¬(∞ = n∞ ∈ ℕ∞))

Lemma: equal-nat-inf-infinity
∀[x:ℕ∞]. uiff(x = ∞ ∈ ℕ∞;∀i:ℕ. (¬(x = i∞ ∈ ℕ∞)))

Lemma: equal-nat-inf-infinity2
∀[x:ℕ∞]. uiff(x = ∞ ∈ ℕ∞;∀i:ℕ. (↑(x i)))

Definition: coW2natinf
coW2natinf(w;n) ==  if (fst(w) =z 1) then if (n =z 0) then tt else coW2natinf(coW-item(w;⋅);n - 1) fi  else ff fi 

Lemma: coW2natinf_wf
∀[n:ℕ]. ∀[w:coW(ℕ2;x.if (x =z 0) then Void else Unit fi )].  (coW2natinf(w;n) ∈ 𝔹)

Definition: ni-selector
ni-selector(p) ==  λn.(¬b(∃i<n + 1.¬b(p i∞))_b)

Lemma: ni-selector_wf
∀[p:ℕ∞ ⟶ 𝔹]. (ni-selector(p) ∈ ℕ∞)

Lemma: ni-selector-property
∀p:ℕ∞ ⟶ 𝔹. (∃x:ℕ∞. p x = ff ⇐⇒ p ni-selector(p) = ff)

Lemma: compact-nat-inf
∀p:ℕ∞ ⟶ 𝔹. ((∃x:ℕ∞. p x = ff) ∨ (∀x:ℕ∞. p x = tt))

Lemma: nat-inf-attach-unit
∀F:ℕ ⟶ Type. ∃G:ℕ∞ ⟶ Type. ((∀n:ℕ. G n∞ ~ F n) ∧ G ∞ ~ ℕ1)

Lemma: nat-inf-attach
∀F:ℕ ⟶ Type. ∀T:Type.  ∃G:ℕ∞ ⟶ Type. ((∀n:ℕ. G n∞ ~ F n) ∧ G ∞ ~ T)

Lemma: nat-inf-limit
∀p:ℕ∞ ⟶ 𝔹. ((∀n:ℕ. p n∞ = ff) ⇒ p ∞ = ff)

Comment: decidable properties of types
Are there any non-trivial, decidable properties of types?
If F ∈ Type ⟶ 𝔹 and F is not constant, then
1) can F exists at all?
2) if it can, then can it respect extensional equality
    (i.e.  can X ≡ Y ⇒ F X = F Y) ?
3) if it could respect extensional equality, then could it
   repsect equipollence?
  (i.e  X ~ Y ⇒ F X = F Y)

  The answer to 3) is No.
  Rice-theorem-for-Type
  This was proved by Escardo, and we did the proof in Nuprl.

If we had ⌜Type ⊆r Base⌝ (which might be possible, but doesn't seem 
provable now) and if there we canonical form tests for some of the
types, say a test isInt, and if Type were a value type (which also seems
possible), then isInt could give us a function ⌜Type ⟶ 𝔹⌝ that would
be non-constant. So the answer to 1) could possibly be Yes.

But such a function would be very intensional so it wouldn't answer 2)
with Yes.  It seems likely that the answer to 2) is No, but we have not
proved that.⋅

Lemma: Rice-theorem-for-Type
∀F:Type ⟶ 𝔹. ((∀X,Y:Type.  (X ~ Y ⇒ F X = F Y)) ⇒ ((F = (λT.tt) ∈ (Type ⟶ 𝔹)) ∨ (F = (λT.ff) ∈ (Type ⟶ 𝔹))))

Definition: ni-max
ni-max(f;g) ==  λi.((f i) ∨b(g i))

Lemma: ni-max_wf
∀[f,g:ℕ∞].  (ni-max(f;g) ∈ ℕ∞)

Lemma: ni-max-nat
∀[n,m:ℕ].  (ni-max(n∞;m∞) = imax(n;m)∞ ∈ ℕ∞)

Lemma: ni-max-com
∀[x,y:ℕ∞].  (ni-max(x;y) = ni-max(y;x) ∈ ℕ∞)

Lemma: ni-max-assoc
∀[x,y,z:ℕ∞].  (ni-max(ni-max(x;y);z) = ni-max(x;ni-max(y;z)) ∈ ℕ∞)

Lemma: ni-max-identity
∀[x:ℕ∞]. (ni-max(x;∞) = ∞ ∈ ℕ∞)

Lemma: ni-max-zero
∀[x:ℕ∞]. (ni-max(x;0∞) = x ∈ ℕ∞)

Lemma: ni-max-idemp
∀[x:ℕ∞]. (ni-max(x;x) = x ∈ ℕ∞)

Definition: ni-min
ni-min(f;g) ==  λi.((f i) ∧b (g i))

Lemma: ni-min_wf
∀[f,g:ℕ∞].  (ni-min(f;g) ∈ ℕ∞)

Lemma: ni-min-nat
∀[n,m:ℕ].  (ni-min(n∞;m∞) = imin(n;m)∞ ∈ ℕ∞)

Lemma: ni-min-com
∀[x,y:ℕ∞].  (ni-min(x;y) = ni-min(y;x) ∈ ℕ∞)

Lemma: ni-min-assoc
∀[x,y,z:ℕ∞].  (ni-min(ni-min(x;y);z) = ni-min(x;ni-min(y;z)) ∈ ℕ∞)

Lemma: ni-min-identity
∀[x:ℕ∞]. (ni-min(x;∞) = x ∈ ℕ∞)

Lemma: ni-min-zero
∀[x:ℕ∞]. (ni-min(x;0∞) = 0∞ ∈ ℕ∞)

Lemma: ni-min-idemp
∀[x:ℕ∞]. (ni-min(x;x) = x ∈ ℕ∞)

Definition: ni-iterated-min
ni-iterated-min(n;f) ==  primrec(n;∞;λm,s. ni-min(f m;s))

Lemma: ni-iterated-min_wf
∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ∞].  (ni-iterated-min(n;f) ∈ ℕ∞)

Definition: ni-eventually-equal
ni-eventually-equal(f;g) ==  ∃n:ℕ. ∀m:{n...}. f m = g m

Lemma: ni-eventually-equal_wf
∀[f,g:ℕ∞].  (ni-eventually-equal(f;g) ∈ ℙ)

Lemma: ni-eventually-equal-equiv
EquivRel(ℕ∞;f,g.ni-eventually-equal(f;g))

Lemma: not-ni-eventually-equal-inf
∀[x:ℕ∞]. (¬ni-eventually-equal(x;0∞) ⇐⇒ x = ∞ ∈ ℕ∞)



Home Index