Nuprl Lemma : cat-functor_wf

[C1,C2:SmallCategory].  (Functor(C1;C2) ∈ Type)


Proof




Definitions occuring in Statement :  cat-functor: Functor(C1;C2) small-category: SmallCategory uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  prop: all: x:A. B[x] so_apply: x[s] so_lambda: λ2x.t[x] and: P ∧ Q cat-functor: Functor(C1;C2) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  small-category_wf cat-comp_wf cat-id_wf equal_wf all_wf cat-arrow_wf cat-ob_wf
Rules used in proof :  isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality lambdaEquality productElimination applyEquality because_Cache hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution lemma_by_obid functionEquality productEquality setEquality sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[C1,C2:SmallCategory].    (Functor(C1;C2)  \mmember{}  Type)



Date html generated: 2020_05_20-AM-07_50_44
Last ObjectModification: 2015_12_28-PM-02_24_14

Theory : small!categories


Home Index