Nuprl Lemma : Kan_id_filler_wf
∀X:CubicalSet. ∀A:{X ⊢ _(Kan)}. ∀a,b:{X ⊢ _:Kan-type(A)}.
(Kan_id_filler(X;A;a;b) ∈ {filler:I:(Cname List)
⟶ alpha:X(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)
⟶ (Id_Kan-type(A) a b)(alpha)|
Kan-A-filler(X;(Id_Kan-type(A) a b);filler)} )
Proof
Definitions occuring in Statement :
Kan_id_filler: Kan_id_filler(X;A;a;b),
cubical-identity: (Id_A a b),
Kan-type: Kan-type(Ak),
Kan-cubical-type: {X ⊢ _(Kan)},
Kan-A-filler: Kan-A-filler(X;A;filler),
A-open-box: A-open-box(X;A;I;alpha;J;x;i),
cubical-term: {X ⊢ _:AF},
cubical-type-at: A(a),
I-cube: X(I),
cubical-set: CubicalSet,
nameset: nameset(L),
coordinate_name: Cname,
list: T List,
int_seg: {i..j-},
all: ∀x:A. B[x],
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
nameset: nameset(L),
uimplies: b supposing a,
subtype_rel: A ⊆r B,
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
cubical-path: cubical-path(X;A;a;b;I;alpha),
pi1: fst(t),
cubical-type-at: A(a),
cubical-identity: (Id_A a b),
Kan-A-filler: Kan-A-filler(X;A;filler),
prop: ℙ,
Kan_id_filler: Kan_id_filler(X;A;a;b),
I-path: I-path(X;A;a;b;I;alpha),
pi2: snd(t),
so_lambda: λ2x.t[x],
not: ¬A,
implies: P ⇒ Q,
false: False,
so_apply: x[s],
top: Top,
named-path: named-path(X;A;a;b;I;alpha;z),
squash: ↓T,
name-path-endpoints: name-path-endpoints(X;A;a;b;I;alpha;z;omega),
and: P ∧ Q,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
or: P ∨ Q,
fills-A-open-box: fills-A-open-box(X;A;I;alpha;bx;cube),
fills-A-faces: fills-A-faces(X;A;I;alpha;bx;L),
l_all: (∀x∈L.P[x]),
A-open-box: A-open-box(X;A;I;alpha;J;x;i),
int_seg: {i..j-},
guard: {T},
lelt: i ≤ j < k,
sq_stable: SqStable(P),
coordinate_name: Cname,
int_upper: {i...},
decidable: Dec(P),
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
less_than: a < b,
A-face: A-face(X;A;I;alpha),
is-A-face: is-A-face(X;A;I;alpha;bx;f),
spreadn: spread3,
cubical-id-box: cubical-id-box(X;A;a;b;I;alpha;box),
lift-id-faces: lift-id-faces(X;A;I;alpha;box),
extend-A-open-box: extend-A-open-box(bx;f1;f2),
uiff: uiff(P;Q),
subtract: n - m,
sq_type: SQType(T),
add-fresh-cname: I+,
iota': iota'(I),
has-value: (a)↓,
lift-id-face: lift-id-face(X;A;I;alpha;face),
assert: ↑b,
bnot: ¬bb,
bfalse: ff,
ifthenelse: if b then t else f fi ,
btrue: tt,
it: ⋅,
unit: Unit,
bool: 𝔹,
deq: EqDecider(T),
true: True,
cubical-type-ap-morph: (u a f),
I-path-morph: I-path-morph(X;A;I;K;f;alpha;p),
cand: A c∧ B,
named-path-morph: named-path-morph(X;A;I;K;z;x;f;alpha;w),
path-eq: path-eq(X;A;I;alpha;p;q)
Lemmas referenced :
cubical-term_wf,
Kan-type_wf,
Kan-cubical-type_wf,
cubical-set_wf,
Kan_id_filler_wf1,
I-cube_wf,
list_wf,
nameset_wf,
int_seg_wf,
coordinate_name_wf,
subtype_rel_list,
cubical-identity_wf,
A-open-box_wf,
path-eq-equiv,
path-eq_wf,
I-path_wf,
subtype_quotient,
Kan-A-filler_wf,
pi1_wf_top,
not_wf,
l_member_wf,
subtype_rel_product,
named-path_wf,
istype-void,
top_wf,
Kanfiller_wf,
cons_wf,
fresh-cname_wf,
cube-set-restriction_wf,
iota_wf,
cons_member,
nameset_subtype,
l_subset_right_cons_trivial,
cubical-id-box_wf,
select_wf,
A-face_wf,
int_seg_properties,
length_wf,
sq_stable__l_member,
decidable__equal-coordinate_name,
sq_stable__le,
decidable__le,
full-omega-unsat,
intformand_wf,
intformnot_wf,
intformle_wf,
itermConstant_wf,
itermVar_wf,
istype-int,
int_formula_prop_and_lemma,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_formula_prop_wf,
decidable__lt,
intformless_wf,
int_formula_prop_less_lemma,
name-path-endpoints_wf,
fresh-cname-not-member2,
length_of_cons_lemma,
length-map,
add-member-int_seg2,
subtract_wf,
itermSubtract_wf,
int_term_value_subtract_lemma,
itermAdd_wf,
int_term_value_add_lemma,
istype-le,
istype-less_than,
select-cons-tl,
select-map,
subtype_base_sq,
int_subtype_base,
decidable__equal_int,
intformeq_wf,
int_formula_prop_eq_lemma,
is-A-face_wf,
coordinate_name-value-type,
set-value-type,
value-type-has-value,
lift-id-face_wf,
set-path-name_wf,
list-diff_wf,
cname_deq_wf,
nil_wf,
face-map_wf2,
subtype_rel_sets_simple,
member-list-diff,
set_subtype_base,
le_wf,
member_singleton,
assert-bnot,
bool_wf,
bool_cases_sqequal,
bool_subtype_base,
deq-member_wf,
eqff_to_assert,
assert-deq-member,
eqtt_to_assert,
bfalse_wf,
bor_wf,
deq_member_nil_lemma,
deq_member_cons_lemma,
iff_weakening_equal,
subtype_rel_self,
list-diff-cons,
istype-universe,
true_wf,
squash_wf,
equal_wf,
cube-set-restriction-comp,
subtype_rel-equal,
fresh-cname-not-equal2,
iota-face-map,
cubical-type-at_wf,
cubical-type-ap-morph_wf,
subtype_rel_set,
fresh-cname-not-member-list-diff,
quotient-member-eq,
named-path-morph_wf,
cubical-type_wf,
rename-one-name_wf,
extend-name-morph_wf,
cubical-type-ap-morph-comp,
name-comp_wf,
name-morph_wf,
rename-one-extend-name-morph,
fresh-cname-not-equal,
extend-face-map-same,
l_subset_refl,
l_subset_wf,
name-morph_subtype,
rename-one-iota,
extended-face-map1,
list_subtype_base,
name-comp-assoc
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
sqequalHypSubstitution,
hypothesis,
inhabitedIsType,
hypothesisEquality,
universeIsType,
introduction,
extract_by_obid,
isectElimination,
thin,
dependent_functionElimination,
natural_numberEquality,
rename,
setElimination,
lambdaEquality_alt,
independent_isectElimination,
because_Cache,
sqequalRule,
applyEquality,
functionExtensionality,
equalitySymmetry,
equalityTransitivity,
dependent_set_memberEquality_alt,
applyLambdaEquality,
productElimination,
setEquality,
setIsType,
functionIsType,
isect_memberEquality_alt,
voidElimination,
independent_functionElimination,
imageMemberEquality,
baseClosed,
imageElimination,
independent_pairFormation,
inlFormation_alt,
equalityIstype,
unionElimination,
approximateComputation,
dependent_pairFormation_alt,
int_eqEquality,
closedConclusion,
addEquality,
productIsType,
instantiate,
cumulativity,
intEquality,
hyp_replacement,
callbyvalueReduce,
promote_hyp,
equalityIsType1,
baseApply,
equalityIsType4,
equalityElimination,
universeEquality,
axiomEquality,
dependent_pairEquality_alt
Latex:
\mforall{}X:CubicalSet. \mforall{}A:\{X \mvdash{} \_(Kan)\}. \mforall{}a,b:\{X \mvdash{} \_:Kan-type(A)\}.
(Kan\_id\_filler(X;A;a;b) \mmember{} \{filler:I:(Cname List)
{}\mrightarrow{} alpha:X(I)
{}\mrightarrow{} J:(nameset(I) List)
{}\mrightarrow{} x:nameset(I)
{}\mrightarrow{} i:\mBbbN{}2
{}\mrightarrow{} A-open-box(X;(Id\_Kan-type(A) a b);I;alpha;J;x;i)
{}\mrightarrow{} (Id\_Kan-type(A) a b)(alpha)|
Kan-A-filler(X;(Id\_Kan-type(A) a b);filler)\} )
Date html generated:
2019_11_06-PM-00_45_50
Last ObjectModification:
2018_12_10-PM-05_00_24
Theory : cubical!sets
Home
Index