Nuprl Lemma : strong-subtype-dep-product

[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  (strong-subtype(a:A × B[a];c:C × D[c])) supposing ((∀a:A. strong-subtype(B[a];D[a])) and strong-subtype(A;C))


Proof




Definitions occuring in Statement :  strong-subtype: strong-subtype(A;B) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x] product: x:A × B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a implies:  Q guard: {T} so_apply: x[s] all: x:A. B[x] subtype_rel: A ⊆B strong-subtype: strong-subtype(A;B) cand: c∧ B prop: so_lambda: λ2x.t[x] exists: x:A. B[x] pi1: fst(t) pi2: snd(t) label: ...$L... t
Lemmas referenced :  strong-subtype-implies strong-subtype_witness strong-subtype_wf istype-universe pi1_wf pi2_wf subtype_rel_product
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis productEquality applyEquality sqequalRule Error :functionIsType,  Error :universeIsType,  productElimination Error :isect_memberEquality_alt,  because_Cache Error :isectIsTypeImplies,  Error :inhabitedIsType,  instantiate universeEquality independent_pairFormation lemma_by_obid lambdaEquality independent_isectElimination lambdaFormation dependent_functionElimination Error :lambdaEquality_alt,  Error :setIsType,  Error :productIsType,  Error :equalityIstype,  setElimination rename Error :dependent_set_memberEquality_alt,  Error :dependent_pairFormation_alt,  applyLambdaEquality Error :dependent_pairEquality_alt,  equalityTransitivity equalitySymmetry hyp_replacement

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[C:Type].  \mforall{}[D:C  {}\mrightarrow{}  Type].
    (strong-subtype(a:A  \mtimes{}  B[a];c:C  \mtimes{}  D[c]))  supposing 
          ((\mforall{}a:A.  strong-subtype(B[a];D[a]))  and 
          strong-subtype(A;C))



Date html generated: 2019_06_20-PM-00_27_57
Last ObjectModification: 2018_12_16-PM-00_26_22

Theory : subtype_1


Home Index