Nuprl Lemma : presheaf-pi-family-comp

∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀s:psc_map{j:l}(C; Delta; X). ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I.
∀a:Delta(I). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀w:presheaf-pi-family(C; X; A; B; I; (s)a).
  (λK,g. (w K (cat-comp(C) K J I g f)) ∈ presheaf-pi-family(C; X; A; B; J; (s)f(a)))


Proof



Definitions occuring in Statement :  presheaf-pi-family: presheaf-pi-family(C; X; A; B; I; a),  psc-adjoin: X.A,  presheaf-type: {X ⊢ _},  pscm-ap: (s)x,  psc_map: A ⟶ B,  psc-restriction: f(s),  I_set: A(I),  ps_context: __⊢,  all: ∀x:A. B[x],  member: t ∈ T,  apply: f a,  lambda: λx.A[x],  cat-comp: cat-comp(C),  cat-arrow: cat-arrow(C),  cat-ob: cat-ob(C),  small-category: SmallCategory
Definitions unfolded in proof :  all: ∀x:A. B[x],  member: t ∈ T,  presheaf-pi-family: presheaf-pi-family(C; X; A; B; I; a),  uall: ∀[x:A]. B[x],  subtype_rel: A ⊆r B,  so_lambda: λ2x.t[x],  so_apply: x[s],  uimplies: b supposing a,  squash: ↓T,  guard: {T},  iff: P ⇐⇒ Q,  and: P ∧ Q,  rev_implies: P ⇐ Q,  implies: P ⇒ Q,  true: True,  prop: ℙ
Lemmas referenced :  cat-comp_wf,  subtype_rel_dep_function,  presheaf-type-at_wf,  psc-restriction_wf,  pscm-ap_wf,  psc-adjoin_wf,  ps_context_cumulativity2,  presheaf-type-cumulativity2,  psc-adjoin-set_wf,  subtype_rel-equal,  equal_wf,  I_set_wf,  pscm-ap-restriction,  iff_weakening_equal,  psc-restriction-comp,  cat-arrow_wf,  presheaf-type-ap-morph_wf,  squash_wf,  true_wf,  psc-adjoin-set-restriction,  subtype_rel_self,  istype-universe,  presheaf-pi-family_wf,  small-category-cumulativity-2,  presheaf-type_wf,  cat-ob_wf,  psc_map_wf,  ps_context_wf,  small-category_wf,  cat-comp-assoc
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation_alt,  cut,  sqequalHypSubstitution,  setElimination,  thin,  rename,  dependent_set_memberEquality_alt,  lambdaEquality_alt,  applyEquality,  hypothesisEquality,  introduction,  extract_by_obid,  isectElimination,  hypothesis,  because_Cache,  sqequalRule,  instantiate,  dependent_functionElimination,  universeIsType,  independent_isectElimination,  imageElimination,  imageMemberEquality,  baseClosed,  equalityTransitivity,  equalitySymmetry,  productElimination,  independent_functionElimination,  natural_numberEquality,  Error :memTop,  universeEquality,  functionIsType,  equalityIstype,  inhabitedIsType,  hyp_replacement,  functionEquality
Latex:
\mforall{}C:SmallCategory.  \mforall{}X,Delta:ps\_context\{j:l\}(C).  \mforall{}s:psc\_map\{j:l\}(C;  Delta;  X).  \mforall{}I,J:cat-ob(C).
\mforall{}f:cat-arrow(C)  J  I.  \mforall{}a:Delta(I).  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.  \mforall{}w:presheaf-pi-family(C;
                                                                                                                                                                    X;
                                                                                                                                                                    A;
                                                                                                                                                                    B;
                                                                                                                                                                    I;
                                                                                                                                                                    (s)a).
    (\mlambda{}K,g.  (w  K  (cat-comp(C)  K  J  I  g  f))  \mmember{}  presheaf-pi-family(C;  X;  A;  B;  J;  (s)f(a)))


Date html generated: 2020_05_20-PM-01_28_49
Last ObjectModification: 2020_04_02-PM-02_00_46

Theory : presheaf!models!of!type!theory


Home Index