Nuprl Lemma : equal-fiber-when-discrete
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[f:{X ⊢ _:(A ⟶ T)}]. ∀[z:{X ⊢ _:T}]. ∀[a,b:{X ⊢ _:Fiber(f;z)}].
  a = b ∈ {X ⊢ _:Fiber(f;z)} 
⇐⇒ a.1 = b.1 ∈ {X ⊢ _:A} 
  supposing ∀x:{X ⊢ _:Path(T)}. (x = refl(x @ 0(𝕀)) ∈ {X ⊢ _:Path(T)})
Proof
Definitions occuring in Statement : 
cubical-fiber: Fiber(w;a)
, 
cubical-refl: refl(a)
, 
cubicalpath-app: pth @ r
, 
pathtype: Path(A)
, 
interval-0: 0(𝕀)
, 
cubical-fst: p.1
, 
cubical-fun: (A ⟶ B)
, 
cubical-term: {X ⊢ _:A}
, 
cubical-type: {X ⊢ _}
, 
cubical_set: CubicalSet
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
all: ∀x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
uimplies: b supposing a
, 
member: t ∈ T
, 
subtype_rel: A ⊆r B
, 
all: ∀x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
and: P ∧ Q
, 
implies: P 
⇒ Q
, 
squash: ↓T
, 
prop: ℙ
, 
cubical-fiber: Fiber(w;a)
, 
true: True
, 
guard: {T}
, 
rev_implies: P 
⇐ Q
, 
cubical-path-app: pth @ r
, 
cubical-refl: refl(a)
, 
term-to-path: <>(a)
, 
cc-fst: p
, 
csm-ap-term: (t)s
, 
csm-ap: (s)x
Lemmas referenced : 
csm-ap-term_wf, 
cube-context-adjoin_wf, 
cubical_set_cumulativity-i-j, 
cubical-type-cumulativity2, 
cubical-fun_wf, 
cc-fst_wf, 
csm-cubical-fun, 
cubical-term-eqcd, 
cubical-app_wf_fun, 
csm-ap-type_wf, 
cc-snd_wf, 
equal_wf, 
squash_wf, 
true_wf, 
istype-universe, 
cubical-fst_wf, 
istype-cubical-term, 
cubical-sigma_wf, 
cubical-type_wf, 
path-type_wf, 
subtype_rel_self, 
iff_weakening_equal, 
cubical-sigma-equal, 
pathtype_wf, 
cubical-refl_wf, 
cubicalpath-app_wf, 
interval-0_wf, 
path-type-subtype, 
cubical-fiber_wf, 
cubical_set_wf, 
csm-path-type, 
csm-id-adjoin_wf, 
cubical-snd_wf, 
cube_set_map_wf, 
csm_id_adjoin_fst_type_lemma, 
csm_id_adjoin_fst_term_lemma, 
subtype_rel_transitivity, 
cubical-term_wf, 
csm-id_wf, 
subset-cubical-term2, 
sub_cubical_set_self, 
csm-ap-id-type, 
paths-equal, 
subtype_rel_wf, 
cubical-path-app-0, 
csm_id_ap_term_lemma, 
subset-cubical-term
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
cut, 
thin, 
instantiate, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
hypothesisEquality, 
applyEquality, 
hypothesis, 
sqequalRule, 
because_Cache, 
equalityTransitivity, 
equalitySymmetry, 
dependent_functionElimination, 
independent_isectElimination, 
lambdaEquality_alt, 
hyp_replacement, 
universeIsType, 
independent_pairFormation, 
lambdaFormation_alt, 
imageElimination, 
universeEquality, 
natural_numberEquality, 
imageMemberEquality, 
baseClosed, 
productElimination, 
independent_functionElimination, 
equalityIstype, 
inhabitedIsType, 
functionIsType, 
cumulativity, 
Error :memTop, 
applyLambdaEquality
Latex:
\mforall{}[X:j\mvdash{}].  \mforall{}[T,A:\{X  \mvdash{}  \_\}].  \mforall{}[f:\{X  \mvdash{}  \_:(A  {}\mrightarrow{}  T)\}].  \mforall{}[z:\{X  \mvdash{}  \_:T\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:Fiber(f;z)\}].
    a  =  b  \mLeftarrow{}{}\mRightarrow{}  a.1  =  b.1  supposing  \mforall{}x:\{X  \mvdash{}  \_:Path(T)\}.  (x  =  refl(x  @  0(\mBbbI{})))
Date html generated:
2020_05_20-PM-03_37_19
Last ObjectModification:
2020_04_20-AM-11_12_44
Theory : cubical!type!theory
Home
Index