Nuprl Lemma : p-compose-id

[A,B:Type]. ∀[f:A ⟶ (B Top)].  (f p-id() f ∈ (A ⟶ (B Top)))


Proof




Definitions occuring in Statement :  p-id: p-id() p-compose: g uall: [x:A]. B[x] top: Top function: x:A ⟶ B[x] union: left right universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T p-id: p-id() p-compose: g do-apply: do-apply(f;x) can-apply: can-apply(f;x) isl: isl(x) outl: outl(x) ifthenelse: if then else fi  btrue: tt
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule functionExtensionality applyEquality hypothesisEquality hypothesis functionEquality unionEquality lemma_by_obid sqequalHypSubstitution isect_memberEquality isectElimination thin axiomEquality because_Cache universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  (B  +  Top)].    (f  o  p-id()  =  f)



Date html generated: 2016_05_15-PM-03_29_58
Last ObjectModification: 2015_12_27-PM-01_10_17

Theory : general


Home Index