Nuprl Lemma : type-cat_wf

TypeCat ∈ SmallCategory'


Proof




Definitions occuring in Statement :  type-cat: TypeCat small-category: SmallCategory member: t ∈ T
Definitions unfolded in proof :  type-cat: TypeCat member: t ∈ T small-category: SmallCategory uall: [x:A]. B[x] compose: g spreadn: spread4 and: P ∧ Q cand: c∧ B all: x:A. B[x] squash: T prop: true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  compose_wf equal_wf squash_wf true_wf eta_conv iff_weakening_equal all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_set_memberEquality dependent_pairEquality universeEquality lambdaEquality cumulativity functionEquality hypothesisEquality sqequalRule independent_pairEquality cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin functionExtensionality applyEquality hypothesis productEquality lambdaFormation imageElimination equalityTransitivity equalitySymmetry because_Cache natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination independent_pairFormation instantiate

Latex:
TypeCat  \mmember{}  SmallCategory'



Date html generated: 2020_05_20-AM-07_52_24
Last ObjectModification: 2017_07_28-AM-09_19_32

Theory : small!categories


Home Index