### Nuprl Lemma : discrete-cat_wf

`∀[X:Type]. (discrete-cat(X) ∈ SmallCategory)`

Proof

Definitions occuring in Statement :  discrete-cat: `discrete-cat(X)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` discrete-cat: `discrete-cat(X)` so_lambda: `λ2x y.t[x; y]` prop: `ℙ` so_apply: `x[s1;s2]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` unit: `Unit` so_apply: `x[s]` so_lambda: so_lambda5 uimplies: `b supposing a` implies: `P `` Q` so_apply: `x[s1;s2;s3;s4;s5]` all: `∀x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B` it: `⋅`
Lemmas referenced :  mk-cat_wf equal_wf it_wf member_wf equal-wf-base equal_subtype
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality lambdaEquality because_Cache hypothesis applyEquality equalityElimination axiomEquality intEquality natural_numberEquality baseClosed independent_isectElimination lambdaFormation equalityTransitivity independent_pairFormation equalitySymmetry universeEquality

Latex:
\mforall{}[X:Type].  (discrete-cat(X)  \mmember{}  SmallCategory)

Date html generated: 2020_05_20-AM-07_49_46
Last ObjectModification: 2017_07_28-AM-09_18_57

Theory : small!categories

Home Index