Nuprl Lemma : csm-rev_fill_term
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ Compositon(A)]. ∀[u:{Gamma.𝕀, (phi)p ⊢ _:A}].
∀[a1:{Gamma ⊢ _:(A)[1(𝕀)][phi |⟶ u[1]]}]. ∀[Delta:j⊢]. ∀[s:Delta j⟶ Gamma].
  ((rev_fill_term(Gamma;cA;phi;u;a1))s+
  = rev_fill_term(Delta;(cA)s+;(phi)s;(u)s+;(a1)s)
  ∈ {Delta.𝕀 ⊢ _:(A)s+[((phi)s)p |⟶ (u)s+]})
Proof
Definitions occuring in Statement : 
rev_fill_term: rev_fill_term(Gamma;cA;phi;u;a1)
, 
csm-comp-structure: (cA)tau
, 
composition-structure: Gamma ⊢ Compositon(A)
, 
partial-term-1: u[1]
, 
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]}
, 
context-subset: Gamma, phi
, 
face-type: 𝔽
, 
interval-1: 1(𝕀)
, 
interval-type: 𝕀
, 
csm+: tau+
, 
csm-id-adjoin: [u]
, 
cc-fst: p
, 
cube-context-adjoin: X.A
, 
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]
, 
member: t ∈ T
, 
cc-snd: q
, 
interval-type: 𝕀
, 
cc-fst: p
, 
csm-ap-type: (AF)s
, 
constant-cubical-type: (X)
, 
subtype_rel: A ⊆r B
, 
uimplies: b supposing a
, 
csm+: tau+
, 
csm-comp: G o F
, 
guard: {T}
, 
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]}
, 
squash: ↓T
, 
cubical-type: {X ⊢ _}
, 
csm-ap-term: (t)s
, 
csm-adjoin: (s;u)
, 
csm-ap: (s)x
, 
pi1: fst(t)
, 
compose: f o g
, 
rev-type-line: (A)-
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
prop: ℙ
, 
true: True
, 
partial-term-0: u[0]
, 
partial-term-1: u[1]
, 
interval-1: 1(𝕀)
, 
csm-id-adjoin: [u]
, 
interval-rev: 1-(r)
, 
interval-0: 0(𝕀)
, 
csm-id: 1(X)
, 
cubical-term-at: u(a)
, 
pi2: snd(t)
, 
rev_fill_term: rev_fill_term(Gamma;cA;phi;u;a1)
, 
rev-type-comp: rev-type-comp(Gamma;cA)
, 
csm-comp-structure: (cA)tau
Lemmas referenced : 
interval-rev_wf, 
cube-context-adjoin_wf, 
interval-type_wf, 
cc-snd_wf, 
subset-cubical-term2, 
sub_cubical_set_self, 
csm-ap-type_wf, 
cc-fst_wf, 
csm-interval-type, 
csm-constrained-cubical-term, 
csm+_wf_interval, 
csm-ap-term_wf, 
face-type_wf, 
csm-face-type, 
rev_fill_term_wf, 
cube_set_map_wf, 
constrained-cubical-term_wf, 
cubical_set_cumulativity-i-j, 
csm-id-adjoin_wf-interval-1, 
cubical-type-cumulativity2, 
partial-term-1_wf, 
cubical-term_wf, 
context-subset_wf, 
thin-context-subset, 
composition-structure_wf, 
cubical-type_wf, 
cubical_set_wf, 
csm_ap_term_fst_adjoin_lemma, 
rev-type-line_wf, 
csm-adjoin_wf, 
context-subset-map, 
csm_id_adjoin_fst_term_lemma, 
squash_wf, 
true_wf, 
csm-ap-id-term, 
cubical-type-cumulativity, 
rev-type-line-0, 
dma-neg-dM0, 
csm-id-adjoin_wf, 
interval-1_wf, 
csm-fill_term, 
rev-type-comp_wf, 
rev-rev-type-line, 
csm-context-subset-subtype2, 
context-subset-term-subtype
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
cut, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
instantiate, 
hypothesis, 
hypothesisEquality, 
sqequalRule, 
equalityTransitivity, 
equalitySymmetry, 
applyEquality, 
because_Cache, 
independent_isectElimination, 
Error :memTop, 
universeIsType, 
inhabitedIsType, 
applyLambdaEquality, 
setElimination, 
rename, 
imageMemberEquality, 
baseClosed, 
imageElimination, 
dependent_set_memberEquality_alt, 
productElimination, 
dependent_functionElimination, 
lambdaEquality_alt, 
cumulativity, 
universeEquality, 
lambdaFormation_alt, 
hyp_replacement, 
equalityIstype, 
independent_functionElimination, 
natural_numberEquality
Latex:
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:Gamma.\mBbbI{}  \mvdash{}  Compositon(A)].
\mforall{}[u:\{Gamma.\mBbbI{},  (phi)p  \mvdash{}  \_:A\}].  \mforall{}[a1:\{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})][phi  |{}\mrightarrow{}  u[1]]\}].  \mforall{}[Delta:j\mvdash{}].
\mforall{}[s:Delta  j{}\mrightarrow{}  Gamma].
    ((rev\_fill\_term(Gamma;cA;phi;u;a1))s+  =  rev\_fill\_term(Delta;(cA)s+;(phi)s;(u)s+;(a1)s))
Date html generated:
2020_05_20-PM-04_52_21
Last ObjectModification:
2020_04_13-PM-09_45_25
Theory : cubical!type!theory
Home
Index