### Nuprl Lemma : I-path-morph_functionality

`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I,K:Cname List. ∀f:name-morph(I;K). ∀alpha:X(I).`
`∀p,q:I-path(X;A;a;b;I;alpha).`
`  (path-eq(X;A;I;alpha;p;q) `` path-eq(X;A;K;f(alpha);I-path-morph(X;A;I;K;f;alpha;p);I-path-morph(X;A;I;K;f;alpha;q)))`

Proof

Definitions occuring in Statement :  path-eq: `path-eq(X;A;I;alpha;p;q)` I-path-morph: `I-path-morph(X;A;I;K;f;alpha;p)` I-path: `I-path(X;A;a;b;I;alpha)` cubical-term: `{X ⊢ _:AF}` cubical-type: `{X ⊢ _}` cube-set-restriction: `f(s)` I-cube: `X(I)` cubical-set: `CubicalSet` name-morph: `name-morph(I;J)` coordinate_name: `Cname` list: `T List` all: `∀x:A. B[x]` implies: `P `` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` I-path: `I-path(X;A;a;b;I;alpha)` I-path-morph: `I-path-morph(X;A;I;K;f;alpha;p)` path-eq: `path-eq(X;A;I;alpha;p;q)` named-path-morph: `named-path-morph(X;A;I;K;z;x;f;alpha;w)` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` prop: `ℙ` so_apply: `x[s]` uimplies: `b supposing a` named-path: `named-path(X;A;a;b;I;alpha;z)` subtype_rel: `A ⊆r B` squash: `↓T` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` cand: `A c∧ B` not: `¬A` false: `False`
Lemmas referenced :  fresh-cname_wf set_wf coordinate_name_wf not_wf l_member_wf rename-one-same equal_wf path-eq_wf I-path_wf I-cube_wf name-morph_wf list_wf cubical-term_wf cubical-type_wf cubical-set_wf cubical-type-at_wf cons_wf cube-set-restriction_wf iota_wf cubical-type-ap-morph_wf extend-name-morph_wf subtype_rel-equal cube-set-restriction-comp iff_weakening_equal squash_wf true_wf extend-name-morph-iota name-comp_wf rename-one-name_wf cube-set-restriction-when-id id-morph_wf cubical-type-ap-morph-id cube-set-restriction-id cubical-type-ap-morph-comp extend-name-morph-rename-one rename-one-iota
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin sqequalRule cut introduction extract_by_obid isectElimination hypothesisEquality hypothesis lambdaEquality setElimination rename dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination because_Cache independent_isectElimination applyEquality instantiate imageElimination universeEquality natural_numberEquality imageMemberEquality baseClosed independent_pairFormation voidElimination hyp_replacement applyLambdaEquality

Latex:
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}a,b:\{X  \mvdash{}  \_:A\}.  \mforall{}I,K:Cname  List.  \mforall{}f:name-morph(I;K).  \mforall{}alpha:X(I).
\mforall{}p,q:I-path(X;A;a;b;I;alpha).
(path-eq(X;A;I;alpha;p;q)
{}\mRightarrow{}  path-eq(X;A;K;f(alpha);I-path-morph(X;A;I;K;f;alpha;p);I-path-morph(X;A;I;K;f;alpha;q)))

Date html generated: 2017_10_05-PM-03_55_09
Last ObjectModification: 2017_07_28-AM-11_28_10

Theory : cubical!sets

Home Index