Nuprl Lemma : copath_wf

[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])].  (copath(a.B[a];w) ∈ Type)


Proof




Definitions occuring in Statement :  copath: copath(a.B[a];w) coW: coW(A;a.B[a]) uall: [x:A]. B[x] so_apply: x[s] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T copath: copath(a.B[a];w) so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  nat_wf coPath_wf coW_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule productEquality extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality applyEquality axiomEquality equalityTransitivity equalitySymmetry instantiate cumulativity isect_memberEquality because_Cache functionEquality universeEquality

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:coW(A;a.B[a])].    (copath(a.B[a];w)  \mmember{}  Type)



Date html generated: 2018_07_25-PM-01_38_49
Last ObjectModification: 2018_06_01-AM-08_39_19

Theory : co-recursion


Home Index