Nuprl Lemma : csm-fiber-member
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[w:{X ⊢ _:(T ⟶ A)}]. ∀[a:{X ⊢ _:A}]. ∀[p:{X ⊢ _:Fiber(w;a)}]. ∀[H:j⊢]. ∀[s:H j⟶ X].
  ((fiber-member(p))s = fiber-member((p)s) ∈ {H ⊢ _:(T)s})
Proof
Definitions occuring in Statement : 
fiber-member: fiber-member(p)
, 
cubical-fiber: Fiber(w;a)
, 
cubical-fun: (A ⟶ B)
, 
csm-ap-term: (t)s
, 
cubical-term: {X ⊢ _:A}
, 
csm-ap-type: (AF)s
, 
cubical-type: {X ⊢ _}
, 
cube_set_map: A ⟶ B
, 
cubical_set: CubicalSet
, 
uall: ∀[x:A]. B[x]
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
cubical-fiber: Fiber(w;a)
, 
fiber-member: fiber-member(p)
, 
member: t ∈ T
, 
subtype_rel: A ⊆r B
, 
all: ∀x:A. B[x]
, 
and: P ∧ Q
Lemmas referenced : 
csm-ap-cubical-fst, 
cube_set_map_wf, 
cubical-term_wf, 
cubical-fiber_wf, 
cubical-type-cumulativity2, 
cubical_set_cumulativity-i-j, 
cubical-fun_wf, 
cubical-type_wf, 
cubical_set_wf, 
cc-snd_wf, 
csm-ap-term_wf, 
cube-context-adjoin_wf, 
cc-fst_wf, 
csm-cubical-fun, 
cubical-app_wf_fun, 
csm-ap-type_wf, 
path-type_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
cut, 
sqequalHypSubstitution, 
introduction, 
extract_by_obid, 
isectElimination, 
thin, 
hypothesisEquality, 
hypothesis, 
universeIsType, 
inhabitedIsType, 
instantiate, 
applyEquality, 
sqequalRule, 
because_Cache, 
equalityTransitivity, 
equalitySymmetry, 
dependent_functionElimination, 
dependent_set_memberEquality_alt, 
independent_pairFormation, 
productIsType, 
equalityIstype, 
applyLambdaEquality, 
setElimination, 
rename, 
productElimination, 
lambdaEquality_alt, 
hyp_replacement
Latex:
\mforall{}[X:j\mvdash{}].  \mforall{}[T,A:\{X  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].  \mforall{}[a:\{X  \mvdash{}  \_:A\}].  \mforall{}[p:\{X  \mvdash{}  \_:Fiber(w;a)\}].  \mforall{}[H:j\mvdash{}].
\mforall{}[s:H  j{}\mrightarrow{}  X].
    ((fiber-member(p))s  =  fiber-member((p)s))
Date html generated:
2020_05_20-PM-03_24_30
Last ObjectModification:
2020_04_07-PM-04_10_58
Theory : cubical!type!theory
Home
Index