Nuprl Lemma : cat-initial_wf

[C:SmallCategory]. ∀[i:cat-ob(C)].  (Initial(i) ∈ ℙ)


Proof




Definitions occuring in Statement :  cat-initial: Initial(i) cat-ob: cat-ob(C) small-category: SmallCategory uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T cat-initial: Initial(i) so_lambda: λ2x.t[x] prop: and: P ∧ Q so_apply: x[s]
Lemmas referenced :  uall_wf cat-ob_wf cat-arrow_wf equal_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality productEquality applyEquality because_Cache axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[i:cat-ob(C)].    (Initial(i)  \mmember{}  \mBbbP{})



Date html generated: 2020_05_20-AM-07_50_34
Last ObjectModification: 2017_01_09-AM-09_52_17

Theory : small!categories


Home Index