Nuprl Lemma : discrete-presheaf-term-at-morph

[C:SmallCategory]. ∀[T:Type]. ∀[X:ps_context{j:l}(C)]. ∀[t:{X ⊢ _:discr(T)}].
  ∀I,J:cat-ob(C). ∀f:cat-arrow(C) I. ∀a:X(I).  (t(a) t(f(a)) ∈ T)


Proof




Definitions occuring in Statement :  discrete-presheaf-type: discr(T) presheaf-term-at: u(a) presheaf-term: {X ⊢ _:A} psc-restriction: f(s) I_set: A(I) ps_context: __⊢ uall: [x:A]. B[x] all: x:A. B[x] apply: a universe: Type equal: t ∈ T cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) small-category: SmallCategory
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] presheaf-term: {X ⊢ _:A} discrete-presheaf-type: discr(T) presheaf-term-at: u(a) guard: {T}
Lemmas referenced :  presheaf_type_at_pair_lemma presheaf_type_ap_morph_pair_lemma I_set_wf cat-arrow_wf cat-ob_wf presheaf-term_wf discrete-presheaf-type_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut lambdaFormation_alt sqequalHypSubstitution setElimination thin rename sqequalRule extract_by_obid dependent_functionElimination Error :memTop,  hypothesis universeIsType isectElimination hypothesisEquality applyEquality inhabitedIsType lambdaEquality_alt axiomEquality functionIsTypeImplies isect_memberEquality_alt isectIsTypeImplies because_Cache instantiate universeEquality

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[T:Type].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[t:\{X  \mvdash{}  \_:discr(T)\}].
    \mforall{}I,J:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}a:X(I).    (t(a)  =  t(f(a)))



Date html generated: 2020_05_20-PM-01_34_15
Last ObjectModification: 2020_04_02-PM-06_33_19

Theory : presheaf!models!of!type!theory


Home Index