Nuprl Lemma : app-trans-equiv-path
ā[G:jā¢]. ā[A,B:{G ā¢ _:cš}]. ā[f:{G ā¢ _:Equiv(decode(A);decode(B))}]. ā[a:{G ā¢ _:decode(A)}].
(app(trans-equiv-path(G;A;B;f); a)
= transprt-const(G;CompFun(B);transprt-const(G;CompFun(B);app(equiv-fun(f); a)))
ā {G ā¢ _:decode(B)})
Proof
Definitions occuring in Statement :
trans-equiv-path: trans-equiv-path(G;A;B;f)
,
universe-comp-fun: CompFun(A)
,
universe-decode: decode(t)
,
cubical-universe: cš
,
transprt-const: transprt-const(G;cA;a)
,
equiv-fun: equiv-fun(f)
,
cubical-equiv: Equiv(T;A)
,
cubical-app: app(w; u)
,
cubical-term: {X ā¢ _:A}
,
cubical_set: CubicalSet
,
uall: ā[x:A]. B[x]
,
equal: s = t ā T
Definitions unfolded in proof :
uall: ā[x:A]. B[x]
,
member: t ā T
,
subtype_rel: A ār B
,
guard: {T}
,
trans-equiv-path: trans-equiv-path(G;A;B;f)
,
uimplies: b supposing a
,
cubical-lam: cubical-lam(X;b)
,
let: let,
all: āx:A. B[x]
,
composition-structure: Gamma ā¢ Compositon(A)
,
composition-function: composition-function{j:l,i:l}(Gamma;A)
,
uniform-comp-function: uniform-comp-function{j:l, i:l}(Gamma; A; comp)
,
implies: P
ā Q
,
squash: āT
,
prop: ā
,
true: True
,
iff: P
āā Q
,
and: P ā§ Q
,
universe-comp-fun: CompFun(A)
,
universe-comp-op: compOp(t)
,
comp-op-to-comp-fun: cop-to-cfun(cA)
,
csm-comp-structure: (cA)tau
,
cubical-term-at: u(a)
,
cc-fst: p
,
csm-id-adjoin: [u]
,
interval-type: š
,
csm-comp: G o F
,
csm-id: 1(X)
,
csm-adjoin: (s;u)
,
compose: f o g
,
pi1: fst(t)
,
csm-ap: (s)x
,
csm-composition: (comp)sigma
,
rev_implies: P
ā Q
Lemmas referenced :
csm-ap-term-universe,
cubical_set_cumulativity-i-j,
cube-context-adjoin_wf,
cubical-type-cumulativity2,
cc-fst_wf,
universe-decode_wf,
csm-ap-term_wf,
cubical-equiv-p,
cubical-term-eqcd,
cc-snd_wf,
csm-comp-structure_wf2,
universe-comp-fun_wf,
istype-cubical-term,
cubical-equiv_wf,
istype-cubical-universe-term,
cubical_set_wf,
subtype_rel_self,
composition-structure_wf,
csm-universe-decode,
cubical-app_wf_fun,
csm-ap-type_wf,
equiv-fun_wf,
cubical-beta,
transprt-const_wf,
equal_wf,
squash_wf,
true_wf,
istype-universe,
cubical-term_wf,
csm-id-adjoin_wf,
csm-transprt-const,
iff_weakening_equal,
cubical-type_wf,
cubical-lambda_wf,
csm_id_adjoin_fst_type_lemma,
csm-ap-id-type,
cube_set_map_wf,
subset-cubical-term2,
sub_cubical_set_self,
csm-cubical-app,
cc_snd_csm_id_adjoin_lemma,
cubical-fun_wf,
csm-equiv-fun,
csm_id_adjoin_fst_term_lemma,
csm-ap-id-term
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
because_Cache,
thin,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesisEquality,
applyEquality,
hypothesis,
sqequalRule,
equalityTransitivity,
equalitySymmetry,
independent_isectElimination,
lambdaEquality_alt,
hyp_replacement,
universeIsType,
dependent_functionElimination,
Error :memTop,
inhabitedIsType,
lambdaFormation_alt,
equalityIstype,
independent_functionElimination,
imageElimination,
universeEquality,
natural_numberEquality,
imageMemberEquality,
baseClosed,
productElimination,
applyLambdaEquality
Latex:
\mforall{}[G:j\mvdash{}]. \mforall{}[A,B:\{G \mvdash{} \_:c\mBbbU{}\}]. \mforall{}[f:\{G \mvdash{} \_:Equiv(decode(A);decode(B))\}]. \mforall{}[a:\{G \mvdash{} \_:decode(A)\}].
(app(trans-equiv-path(G;A;B;f); a)
= transprt-const(G;CompFun(B);transprt-const(G;CompFun(B);app(equiv-fun(f); a))))
Date html generated:
2020_05_20-PM-07_40_37
Last ObjectModification:
2020_04_30-PM-05_09_19
Theory : cubical!type!theory
Home
Index