Nuprl Lemma : cubical-fun-ext_wf
∀X:j⊢. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀f,g:{X ⊢ _:ΠA B}. ∀e:{X ⊢ _:ΠA (Path_B app((f)p; q) app((g)p; q))}.
(cubical-fun-ext(X;e) ∈ {X ⊢ _:(Path_ΠA B f g)})
Proof
Definitions occuring in Statement :
cubical-fun-ext: cubical-fun-ext(X;e),
path-type: (Path_A a b),
cubical-app: app(w; u),
cubical-pi: ΠA B,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
cubical-term: {X ⊢ _:A},
cubical-type: {X ⊢ _},
cubical_set: CubicalSet,
all: ∀x:A. B[x],
member: t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
squash: ↓T,
prop: ℙ,
uimplies: b supposing a,
guard: {T},
implies: P ⇒ Q,
true: True,
cubical-type: {X ⊢ _},
cc-snd: q,
cc-fst: p,
csm-adjoin: (s;u),
csm-ap-type: (AF)s,
csm-comp: G o F,
csm-id-adjoin: [u],
csm-ap: (s)x,
csm-id: 1(X),
compose: f o g,
pi1: fst(t),
pi2: snd(t),
interval-type: 𝕀,
constant-cubical-type: (X),
csm-ap-term: (t)s,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
path-type: (Path_A a b),
cubical-subset: cubical-subset,
cubical-term-at: u(a),
cubical-fun-ext: cubical-fun-ext(X;e),
interval-1: 1(𝕀),
interval-0: 0(𝕀),
cand: A c∧ B,
csm+: tau+,
same-cubical-term: X ⊢ u=v:A
Lemmas referenced :
cubical-term_wf,
cubical-pi_wf,
cubical-type-cumulativity2,
cubical_set_cumulativity-i-j,
cubical-type_wf,
cube-context-adjoin_wf,
cubical_set_wf,
csm-ap-term_wf,
cc-fst_wf,
squash_wf,
true_wf,
equal_functionality_wrt_subtype_rel2,
csm-ap-type_wf,
csm-adjoin_wf,
cc-snd_wf,
cubical-app_wf,
csm-comp_wf,
csm-cubical-pi,
interval-type_wf,
path-type_wf,
subset-cubical-term2,
sub_cubical_set_self,
csm-adjoin-p-q,
cubical-pi-p,
csm_ap_term_fst_adjoin_lemma,
equal_wf,
subtype_rel_self,
iff_weakening_equal,
istype-universe,
csm-path-type,
csm-cubical-app,
cubical_type_at_pair_lemma,
csm-id-adjoin_wf-interval-1,
csm_id_adjoin_fst_type_lemma,
csm-ap-id-type,
csm-id-adjoin_wf-interval-0,
csm-id-adjoin_wf,
csm_id_adjoin_fst_term_lemma,
cc_snd_csm_id_adjoin_lemma,
cubical-path-app_wf,
csm-interval-type,
cubical-lambda_wf,
term-to-path-wf,
same-cubical-term_wf,
csm-cubical-lambda,
csm-cubical-path-app,
cubical-eta,
cubical-path-app-1,
cubical-path-app-0
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
because_Cache,
universeIsType,
cut,
thin,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesisEquality,
hypothesis,
applyEquality,
sqequalRule,
equalityTransitivity,
equalitySymmetry,
lambdaEquality_alt,
imageElimination,
cumulativity,
independent_isectElimination,
independent_functionElimination,
natural_numberEquality,
imageMemberEquality,
baseClosed,
hyp_replacement,
setElimination,
rename,
productElimination,
dependent_functionElimination,
Error :memTop,
inhabitedIsType,
universeEquality,
applyLambdaEquality,
independent_pairFormation
Latex:
\mforall{}X:j\mvdash{}. \mforall{}A:\{X \mvdash{} \_\}. \mforall{}B:\{X.A \mvdash{} \_\}. \mforall{}f,g:\{X \mvdash{} \_:\mPi{}A B\}.
\mforall{}e:\{X \mvdash{} \_:\mPi{}A (Path\_B app((f)p; q) app((g)p; q))\}.
(cubical-fun-ext(X;e) \mmember{} \{X \mvdash{} \_:(Path\_\mPi{}A B f g)\})
Date html generated:
2020_05_20-PM-03_35_49
Last ObjectModification:
2020_04_08-PM-07_30_05
Theory : cubical!type!theory
Home
Index