Nuprl Lemma : pscm-id-adjoin-ap-type

C:SmallCategory. ∀Gamma,Delta:ps_context{j:l}(C). ∀A:{Gamma ⊢ _}. ∀B:{Gamma.A ⊢ _}.
sigma:psc_map{j:l}(C; Delta; Gamma). ∀u:{Delta ⊢ _:(A)sigma}.
  (((B)(sigma p;q))[u] (B)(sigma;u) ∈ {Delta ⊢ _})


Proof




Definitions occuring in Statement :  pscm-id-adjoin: [u] pscm-adjoin: (s;u) psc-snd: q psc-fst: p psc-adjoin: X.A presheaf-term: {X ⊢ _:A} pscm-ap-type: (AF)s presheaf-type: {X ⊢ _} pscm-comp: F psc_map: A ⟶ B ps_context: __⊢ all: x:A. B[x] equal: t ∈ T small-category: SmallCategory
Definitions unfolded in proof :  all: x:A. B[x] presheaf-type: {X ⊢ _} pscm-adjoin: (s;u) pscm-ap-type: (AF)s psc-snd: q psc-fst: p pscm-comp: F pscm-id-adjoin: [u] pscm-ap: (s)x pscm-id: 1(X) compose: g pi1: fst(t) pi2: snd(t) member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B psc_map: A ⟶ B nat-trans: nat-trans(C;D;F;G) cat-ob: cat-ob(C) op-cat: op-cat(C) spreadn: spread4 cat-arrow: cat-arrow(C) type-cat: TypeCat cat-comp: cat-comp(C)
Lemmas referenced :  pscm-ap-type_wf psc-adjoin_wf small-category-cumulativity-2 ps_context_cumulativity2 presheaf-type-cumulativity2 pscm-adjoin_wf subtype_rel_self psc_map_wf presheaf-term_wf presheaf-type_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut sqequalHypSubstitution setElimination thin rename productElimination sqequalRule hypothesis instantiate introduction extract_by_obid isectElimination hypothesisEquality applyEquality because_Cache universeIsType

Latex:
\mforall{}C:SmallCategory.  \mforall{}Gamma,Delta:ps\_context\{j:l\}(C).  \mforall{}A:\{Gamma  \mvdash{}  \_\}.  \mforall{}B:\{Gamma.A  \mvdash{}  \_\}.
\mforall{}sigma:psc\_map\{j:l\}(C;  Delta;  Gamma).  \mforall{}u:\{Delta  \mvdash{}  \_:(A)sigma\}.
    (((B)(sigma  o  p;q))[u]  =  (B)(sigma;u))



Date html generated: 2020_05_20-PM-01_28_25
Last ObjectModification: 2020_04_02-PM-01_56_09

Theory : presheaf!models!of!type!theory


Home Index