Nuprl Lemma : coSet-corec
coSet{i:l} ≡ corec(T.a:Type × (a ⟶ T))
Proof
Definitions occuring in Statement :
coSet: coSet{i:l},
corec: corec(T.F[T]),
ext-eq: A ≡ B,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
and: P ∧ Q,
ext-eq: A ≡ B
Lemmas referenced :
corec-subtype-coSet,
coSet-subtype-corec
Rules used in proof :
hypothesis,
extract_by_obid,
introduction,
cut,
independent_pairFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
coSet\{i:l\} \mequiv{} corec(T.a:Type \mtimes{} (a {}\mrightarrow{} T))
Date html generated:
2018_07_29-AM-09_49_31
Last ObjectModification:
2018_07_10-PM-11_22_22
Theory : constructive!set!theory
Home
Index