### Nuprl Lemma : tree-cat_wf

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

Proof

Definitions occuring in Statement :  tree-cat: `tree-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` tree-cat: `tree-cat(X)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` so_lambda: so_lambda5 so_apply: `x[s1;s2;s3;s4;s5]` uimplies: `b supposing a` all: `∀x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B`
Lemmas referenced :  mk-cat_wf unit_wf2 it_wf equal-unit
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality lambdaEquality hypothesis because_Cache independent_isectElimination lambdaFormation independent_pairFormation axiomEquality equalityTransitivity equalitySymmetry universeEquality

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

Date html generated: 2020_05_20-AM-07_49_44
Last ObjectModification: 2017_01_13-AM-11_44_37

Theory : small!categories

Home Index