Nuprl Lemma : pscm-presheaf-type-ap-morph

[A,I,J,f,a,u,s:Top].  ((u f) (u (s)a f))


Proof




Definitions occuring in Statement :  pscm-ap-type: (AF)s presheaf-type-ap-morph: (u f) pscm-ap: (s)x uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  presheaf-type-ap-morph: (u f) pi2: snd(t) uall: [x:A]. B[x] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) member: t ∈ T so_apply: x[s1;s2;s3;s4] top: Top uimplies: supposing a strict4: strict4(F) and: P ∧ Q all: x:A. B[x] implies:  Q has-value: (a)↓ prop: guard: {T} or: P ∨ Q squash: T so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] pscm-ap-type: (AF)s pscm-ap: (s)x
Lemmas referenced :  lifting-strict-spread has-value_wf_base base_wf is-exception_wf strict4-spread top_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalTransitivity computationStep sqequalReflexivity cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin baseClosed isect_memberEquality voidElimination voidEquality independent_isectElimination independent_pairFormation lambdaFormation callbyvalueApply hypothesis baseApply closedConclusion hypothesisEquality applyExceptionCases inrFormation imageMemberEquality imageElimination inlFormation instantiate because_Cache isect_memberFormation sqequalAxiom

Latex:
\mforall{}[A,I,J,f,a,u,s:Top].    ((u  a  f)  \msim{}  (u  (s)a  f))



Date html generated: 2018_05_22-PM-10_03_47
Last ObjectModification: 2018_05_20-PM-09_48_18

Theory : presheaf!models!of!type!theory


Home Index