Nuprl Lemma : coW-corec
∀[A:𝕌']. ∀[B:A ⟶ Type]. coW(A;a.B[a]) ≡ corec(C.a:A × (B[a] ⟶ C))
Proof
Definitions occuring in Statement :
coW: coW(A;a.B[a]),
corec: corec(T.F[T]),
ext-eq: A ≡ B,
uall: ∀[x:A]. B[x],
so_apply: x[s],
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
isect-family: ⋂a:A. F[a],
corec-family: corec-family(H),
param-co-W: pco-W,
coW: coW(A;a.B[a]),
type-continuous: Continuous(T.F[T]),
strong-type-continuous: Continuous+(T.F[T]),
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
type-monotone: Monotone(T.F[T]),
continuous-monotone: ContinuousMonotone(T.F[T]),
compose: f o g,
fun_exp: f^n,
assert: ↑b,
bnot: ¬bb,
sq_type: SQType(T),
exists: ∃x:A. B[x],
bfalse: ff,
ifthenelse: if b then t else f fi ,
btrue: tt,
it: ⋅,
unit: Unit,
bool: 𝔹,
true: True,
less_than': less_than'(a;b),
le: A ≤ B,
subtract: n - m,
uiff: uiff(P;Q),
rev_implies: P ⇐ Q,
not: ¬A,
iff: P ⇐⇒ Q,
or: P ∨ Q,
decidable: Dec(P),
top: Top,
all: ∀x:A. B[x],
prop: ℙ,
uimplies: b supposing a,
guard: {T},
ge: i ≥ j ,
false: False,
implies: P ⇒ Q,
nat: ℕ,
corec: corec(T.F[T]),
subtype_rel: A ⊆r B,
and: P ∧ Q,
ext-eq: A ≡ B,
so_apply: x[s],
so_lambda: λ2x.t[x],
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
it_wf,
compose_wf,
unit_wf2,
continuous-id,
strong-continuous-function,
strong-continuous-depproduct,
subtype_rel_wf,
subtype_rel_function,
subtype_rel_product,
corec-ext,
int_seg_wf,
top_wf,
le_wf,
not-le-2,
primrec_wf,
assert-bnot,
bool_subtype_base,
subtype_base_sq,
bool_cases_sqequal,
equal_wf,
eqff_to_assert,
assert_of_lt_int,
eqtt_to_assert,
bool_wf,
lt_int_wf,
primrec-unroll,
subtype_rel_weakening,
coW-ext,
nat_wf,
le-add-cancel,
add-zero,
add_functionality_wrt_le,
add-commutes,
add-swap,
add-associates,
minus-minus,
minus-add,
minus-one-mul-top,
zero-add,
minus-one-mul,
condition-implies-le,
less-iff-le,
not-ge-2,
false_wf,
subtract_wf,
decidable__le,
primrec0_lemma,
less_than_wf,
ge_wf,
less_than_irreflexivity,
less_than_transitivity1,
nat_properties,
coW_wf,
corec_wf
Rules used in proof :
isectEquality,
dependent_set_memberEquality,
functionExtensionality,
dependent_pairEquality,
promote_hyp,
dependent_pairFormation,
equalityElimination,
hypothesis_subsumption,
minusEquality,
intEquality,
addEquality,
unionElimination,
voidEquality,
dependent_functionElimination,
voidElimination,
independent_functionElimination,
independent_isectElimination,
natural_numberEquality,
lambdaFormation,
intWeakElimination,
rename,
setElimination,
because_Cache,
isect_memberEquality,
axiomEquality,
independent_pairEquality,
productElimination,
equalitySymmetry,
equalityTransitivity,
hypothesis,
independent_pairFormation,
universeEquality,
applyEquality,
cumulativity,
functionEquality,
hypothesisEquality,
productEquality,
lambdaEquality,
sqequalRule,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
instantiate,
thin,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[A:\mBbbU{}']. \mforall{}[B:A {}\mrightarrow{} Type]. coW(A;a.B[a]) \mequiv{} corec(C.a:A \mtimes{} (B[a] {}\mrightarrow{} C))
Date html generated:
2018_07_25-PM-01_37_21
Last ObjectModification:
2018_07_21-PM-07_11_44
Theory : co-recursion
Home
Index