Nuprl Lemma : presheaf-sigma-p

C:SmallCategory. ∀X:ps_context{j:l}(C). ∀T,A:{X ⊢ _}. ∀B:{X.A ⊢ _}.  ((Σ B)p = Σ (A)p (B)(p p;q) ∈ {X.T ⊢ _})


Proof




Definitions occuring in Statement :  presheaf-sigma: Σ B pscm-adjoin: (s;u) psc-snd: q psc-fst: p psc-adjoin: X.A pscm-ap-type: (AF)s presheaf-type: {X ⊢ _} pscm-comp: F ps_context: __⊢ all: x:A. B[x] equal: t ∈ T small-category: SmallCategory
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T subtype_rel: A ⊆B uall: [x:A]. B[x]
Lemmas referenced :  pscm-presheaf-sigma ps_context_cumulativity2 small-category-cumulativity-2 psc-adjoin_wf presheaf-type-cumulativity2 psc-fst_wf presheaf-type_wf ps_context_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut thin instantiate introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination hypothesisEquality applyEquality isectElimination hypothesis sqequalRule because_Cache universeIsType inhabitedIsType

Latex:
\mforall{}C:SmallCategory.  \mforall{}X:ps\_context\{j:l\}(C).  \mforall{}T,A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.
    ((\mSigma{}  A  B)p  =  \mSigma{}  (A)p  (B)(p  o  p;q))



Date html generated: 2020_05_20-PM-01_31_31
Last ObjectModification: 2020_04_02-PM-03_09_23

Theory : presheaf!models!of!type!theory


Home Index