Nuprl Lemma : cubical-fun-equal2

[X:j⊢]. ∀[A,B:{X ⊢ _}]. ∀[f:{X ⊢ _:(A ⟶ B)}].
[g:I:fset(ℕ) ⟶ a:X(I) ⟶ J:fset(ℕ) ⟶ h:J ⟶ I ⟶ u:A(h(a)) ⟶ B(h(a))].
  g ∈ {X ⊢ _:(A ⟶ B)} 
  supposing ∀[I:fset(ℕ)]. ∀[a:X(I)]. ∀[J:fset(ℕ)]. ∀[h:J ⟶ I]. ∀[u:A(h(a))].  ((f(a) u) (g(a) u) ∈ B(h(a)))


Proof




Definitions occuring in Statement :  cubical-fun: (A ⟶ B) cubical-term-at: u(a) cubical-term: {X ⊢ _:A} cubical-type-at: A(a) cubical-type: {X ⊢ _} cube-set-restriction: f(s) I_cube: A(I) cubical_set: CubicalSet names-hom: I ⟶ J fset: fset(T) nat: uimplies: supposing a uall: [x:A]. B[x] apply: a function: x:A ⟶ B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T cubical_set: CubicalSet cubical-fun: (A ⟶ B) presheaf-fun: (A ⟶ B) cubical-fun-family: cubical-fun-family(X; A; B; I; a) presheaf-fun-family: presheaf-fun-family(C; X; A; B; I; a) cube-cat: CubeCat all: x:A. B[x] cubical-type-at: A(a) presheaf-type-at: A(a) cube-set-restriction: f(s) psc-restriction: f(s) cubical-type-ap-morph: (u f) presheaf-type-ap-morph: (u f) I_cube: A(I) I_set: A(I) cubical-term-at: u(a) presheaf-term-at: u(a)
Lemmas referenced :  presheaf-fun-equal2 cube-cat_wf cubical-type-sq-presheaf-type cat_ob_pair_lemma cat_arrow_triple_lemma cat_comp_tuple_lemma cubical-term-sq-presheaf-term
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesis sqequalRule Error :memTop,  dependent_functionElimination

Latex:
\mforall{}[X:j\mvdash{}].  \mforall{}[A,B:\{X  \mvdash{}  \_\}].  \mforall{}[f:\{X  \mvdash{}  \_:(A  {}\mrightarrow{}  B)\}].  \mforall{}[g:I:fset(\mBbbN{})
                                                                                                        {}\mrightarrow{}  a:X(I)
                                                                                                        {}\mrightarrow{}  J:fset(\mBbbN{})
                                                                                                        {}\mrightarrow{}  h:J  {}\mrightarrow{}  I
                                                                                                        {}\mrightarrow{}  u:A(h(a))
                                                                                                        {}\mrightarrow{}  B(h(a))].
    f  =  g 
    supposing  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[a:X(I)].  \mforall{}[J:fset(\mBbbN{})].  \mforall{}[h:J  {}\mrightarrow{}  I].  \mforall{}[u:A(h(a))].
                            ((f(a)  J  h  u)  =  (g(a)  J  h  u))



Date html generated: 2020_05_20-PM-02_23_52
Last ObjectModification: 2020_04_03-PM-08_34_14

Theory : cubical!type!theory


Home Index