Nuprl Lemma : presheaf-type-equal

[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:A:I:cat-ob(C) ⟶ X(I) ⟶ Type × (I:cat-ob(C)
                                                                                               ⟶ J:cat-ob(C)
                                                                                               ⟶ f:(cat-arrow(C) I)
                                                                                               ⟶ a:X(I)
                                                                                               ⟶ (A a)
                                                                                               ⟶ (A f(a)))].
  B ∈ {X ⊢ _} 
  supposing A
  B
  ∈ (A:I:cat-ob(C) ⟶ X(I) ⟶ Type × (I:cat-ob(C)
                                     ⟶ J:cat-ob(C)
                                     ⟶ f:(cat-arrow(C) I)
                                     ⟶ a:X(I)
                                     ⟶ (A a)
                                     ⟶ (A f(a))))


Proof




Definitions occuring in Statement :  presheaf-type: {X ⊢ _} psc-restriction: f(s) I_set: A(I) ps_context: __⊢ uimplies: supposing a uall: [x:A]. B[x] apply: a function: x:A ⟶ B[x] product: x:A × B[x] 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 uimplies: supposing a presheaf-type: {X ⊢ _} and: P ∧ Q all: x:A. B[x] subtype_rel: A ⊆B squash: T true: True prop: guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q
Lemmas referenced :  cat-ob_wf I_set_wf cat-id_wf subtype_rel-equal psc-restriction_wf equal_wf psc-restriction-id ps_context_cumulativity2 subtype_rel_self iff_weakening_equal cat-arrow_wf cat-comp_wf psc-restriction-comp small-category-cumulativity-2 istype-universe presheaf-type_wf ps_context_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution setElimination thin rename dependent_set_memberEquality_alt hypothesis productElimination sqequalRule productIsType functionIsType universeIsType extract_by_obid isectElimination hypothesisEquality applyEquality equalityIstype because_Cache instantiate independent_isectElimination lambdaEquality_alt imageElimination universeEquality natural_numberEquality imageMemberEquality baseClosed equalityTransitivity equalitySymmetry independent_functionElimination dependent_functionElimination inhabitedIsType isect_memberEquality_alt axiomEquality isectIsTypeImplies

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A:\{X  \mvdash{}  \_\}].
\mforall{}[B:A:I:cat-ob(C)  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  Type  \mtimes{}  (I:cat-ob(C)
                                                                        {}\mrightarrow{}  J:cat-ob(C)
                                                                        {}\mrightarrow{}  f:(cat-arrow(C)  J  I)
                                                                        {}\mrightarrow{}  a:X(I)
                                                                        {}\mrightarrow{}  (A  I  a)
                                                                        {}\mrightarrow{}  (A  J  f(a)))].
    A  =  B  supposing  A  =  B



Date html generated: 2020_05_20-PM-01_25_20
Last ObjectModification: 2020_04_01-AM-11_00_46

Theory : presheaf!models!of!type!theory


Home Index