Nuprl Lemma : rev_fill_term_wf
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ Compositon(A)]. ∀[u:{Gamma.𝕀, (phi)p ⊢ _:A}].
∀[a1:{Gamma ⊢ _:(A)[1(𝕀)][phi |⟶ u[1]]}].
  (rev_fill_term(Gamma;cA;phi;u;a1) ∈ {Gamma.𝕀 ⊢ _:A[(phi)p |⟶ u]})
Proof
Definitions occuring in Statement : 
rev_fill_term: rev_fill_term(Gamma;cA;phi;u;a1)
, 
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-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 ⊢ _}
, 
cubical_set: CubicalSet
, 
uall: ∀[x:A]. B[x]
, 
member: 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
, 
rev-type-line: (A)-
, 
implies: P 
⇒ Q
, 
all: ∀x:A. B[x]
, 
guard: {T}
, 
squash: ↓T
, 
prop: ℙ
, 
true: True
, 
partial-term-0: u[0]
, 
partial-term-1: u[1]
, 
interval-1: 1(𝕀)
, 
csm-id-adjoin: [u]
, 
csm-ap-term: (t)s
, 
interval-rev: 1-(r)
, 
csm-adjoin: (s;u)
, 
interval-0: 0(𝕀)
, 
csm-id: 1(X)
, 
csm-ap: (s)x
, 
cubical-term-at: u(a)
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
composition-structure: Gamma ⊢ Compositon(A)
, 
rev_fill_term: rev_fill_term(Gamma;cA;phi;u;a1)
, 
cube-context-adjoin: X.A
, 
context-subset: Gamma, phi
, 
cubical-type: {X ⊢ _}
, 
cubical-term: {X ⊢ _:A}
, 
and: P ∧ Q
, 
cubical-type-at: A(a)
, 
I_cube: A(I)
, 
functor-ob: ob(F)
, 
interval-presheaf: 𝕀
, 
lattice-point: Point(l)
, 
record-select: r.x
, 
dM: dM(I)
, 
free-DeMorgan-algebra: free-DeMorgan-algebra(T;eq)
, 
mk-DeMorgan-algebra: mk-DeMorgan-algebra(L;n)
, 
record-update: r[x := v]
, 
ifthenelse: if b then t else f fi 
, 
eq_atom: x =a y
, 
bfalse: ff
, 
free-DeMorgan-lattice: free-DeMorgan-lattice(T;eq)
, 
free-dist-lattice: free-dist-lattice(T; eq)
, 
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice, 
mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o)
, 
btrue: tt
, 
DeMorgan-algebra: DeMorganAlgebra
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
face-type: 𝔽
, 
face-presheaf: 𝔽
, 
face_lattice: face_lattice(I)
, 
face-lattice: face-lattice(T;eq)
, 
free-dist-lattice-with-constraints: free-dist-lattice-with-constraints(T;eq;x.Cs[x])
, 
constrained-antichain-lattice: constrained-antichain-lattice(T;eq;P)
, 
bdd-distributive-lattice: BoundedDistributiveLattice
, 
iff: P 
⇐⇒ Q
, 
rev_implies: P 
⇐ Q
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_interval, 
csm-interval-type, 
csm-id-adjoin_wf, 
interval-1_wf, 
partial-term-1_wf, 
constrained-cubical-term-eqcd, 
istype-cubical-term, 
context-subset_wf, 
csm-ap-term_wf, 
face-type_wf, 
csm-face-type, 
thin-context-subset, 
composition-structure_wf, 
cubical-type_wf, 
cubical_set_wf, 
cubical_set_cumulativity-i-j, 
cubical-type-cumulativity2, 
cc-fst_wf, 
cubical-term_wf, 
rev-type-line_wf, 
csm_ap_term_fst_adjoin_lemma, 
context-subset-map, 
csm-adjoin_wf, 
csm_id_adjoin_fst_term_lemma, 
squash_wf, 
true_wf, 
csm-ap-id-term, 
cubical-type-cumulativity, 
rev-type-line-0, 
dma-neg-dM0, 
partial-term-0_wf, 
fill_term_wf, 
rev-type-comp_wf, 
csm-constrained-cubical-term, 
rev-rev-type-line, 
cubical-term-equal, 
I_cube_pair_redex_lemma, 
cubical_type_at_pair_lemma, 
cubical_type_ap_morph_pair_lemma, 
DeMorgan-algebra-laws, 
dM_wf, 
subtype_rel_self, 
lattice-point_wf, 
subtype_rel_set, 
DeMorgan-algebra-structure_wf, 
lattice-structure_wf, 
lattice-axioms_wf, 
bounded-lattice-structure-subtype, 
DeMorgan-algebra-structure-subtype, 
subtype_rel_transitivity, 
bounded-lattice-structure_wf, 
bounded-lattice-axioms_wf, 
equal_wf, 
lattice-meet_wf, 
lattice-join_wf, 
DeMorgan-algebra-axioms_wf, 
istype-cubical-type-at, 
cubical-term-at_wf, 
face_lattice_wf, 
I_cube_wf, 
fset_wf, 
nat_wf, 
istype-universe, 
subset-cubical-type, 
context-subset-is-subset, 
iff_weakening_equal, 
cubical-term-eqcd
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, 
independent_functionElimination, 
dependent_functionElimination, 
equalityIstype, 
hyp_replacement, 
lambdaFormation_alt, 
inhabitedIsType, 
lambdaEquality_alt, 
imageElimination, 
natural_numberEquality, 
imageMemberEquality, 
baseClosed, 
cumulativity, 
universeEquality, 
setElimination, 
rename, 
functionExtensionality, 
productElimination, 
dependent_pairEquality_alt, 
productEquality, 
isectEquality, 
dependent_set_memberEquality_alt
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]]\}].
    (rev\_fill\_term(Gamma;cA;phi;u;a1)  \mmember{}  \{Gamma.\mBbbI{}  \mvdash{}  \_:A[(phi)p  |{}\mrightarrow{}  u]\})
Date html generated:
2020_05_20-PM-04_51_20
Last ObjectModification:
2020_05_02-PM-01_20_34
Theory : cubical!type!theory
Home
Index