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) b);I;alpha;J;x;i)
                             ⟶ (Id_Kan-type(A) b)(alpha)| 
                             Kan-A-filler(X;(Id_Kan-type(A) b);filler)} )


Proof




Definitions occuring in Statement :  Kan_id_filler: Kan_id_filler(X;A;a;b) cubical-identity: (Id_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: 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: supposing a subtype_rel: A ⊆B so_apply: x[s1;s2] so_lambda: λ2y.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 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:  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: ⇐⇒ Q rev_implies:  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: 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 then else fi  btrue: tt it: unit: Unit bool: 𝔹 deq: EqDecider(T) true: True cubical-type-ap-morph: (u f) I-path-morph: I-path-morph(X;A;I;K;f;alpha;p) cand: 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