Nuprl Lemma : small-category_wf

SmallCategory ∈ 𝕌'


Proof




Definitions occuring in Statement :  small-category: SmallCategory member: t ∈ T universe: Type
Definitions unfolded in proof :  small-category: SmallCategory member: t ∈ T subtype_rel: A ⊆B spreadn: spread4 and: P ∧ Q uall: [x:A]. B[x] so_lambda: λ2x.t[x] prop: so_apply: x[s]
Lemmas referenced :  all_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep setEquality productEquality universeEquality functionEquality cumulativity hypothesisEquality because_Cache cut applyEquality functionExtensionality hypothesis thin lambdaEquality sqequalHypSubstitution productElimination introduction extract_by_obid isectElimination

Latex:
SmallCategory  \mmember{}  \mBbbU{}'



Date html generated: 2017_10_05-AM-00_45_30
Last ObjectModification: 2017_07_28-AM-09_18_55

Theory : small!categories


Home Index