Nuprl Lemma : type-functor-product_wf

[F,G:Functor].  (F G ∈ Functor)


Proof




Definitions occuring in Statement :  type-functor-product: q type-functor: Functor uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T type-functor: Functor type-functor-product: q and: P ∧ Q all: x:A. B[x] subtype_rel: A ⊆B compose: g cand: c∧ B squash: T prop: implies:  Q label: ...$L... t true: True uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q so_lambda: λ2x.t[x] so_apply: x[s] exists: x:A. B[x]
Lemmas referenced :  istype-universe equal_wf squash_wf true_wf trivial-equal iff_weakening_equal subtype_rel_self isect_subtype_rel_trivial subtype_rel_universe1 subtype_rel_wf type-functor_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut sqequalHypSubstitution setElimination thin rename productElimination sqequalRule dependent_set_memberEquality_alt dependent_pairEquality_alt lambdaEquality_alt because_Cache universeIsType universeEquality isect_memberEquality_alt independent_pairEquality lambdaFormation_alt applyEquality hypothesisEquality hypothesis functionIsType inhabitedIsType dependent_functionElimination productIsType introduction extract_by_obid isectElimination isectIsType imageElimination equalityTransitivity equalitySymmetry productEquality equalityIsType1 independent_functionElimination independent_pairFormation equalityIsType3 baseClosed applyLambdaEquality functionExtensionality natural_numberEquality imageMemberEquality independent_isectElimination instantiate cumulativity functionEquality isectEquality closedConclusion dependent_pairFormation_alt

Latex:
\mforall{}[F,G:Functor].    (F  *  G  \mmember{}  Functor)



Date html generated: 2019_10_15-AM-10_47_03
Last ObjectModification: 2018_10_11-PM-06_49_58

Theory : basic


Home Index