Nuprl Lemma : univ-trans-equiv_path
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[f:{G ⊢ _:Equiv(decode(A);decode(B))}].
  (univ-trans(G;equiv_path(G;A;B;f)) = trans-equiv-path(G;A;B;f) ∈ {G ⊢ _:(decode(A) ⟶ decode(B))})
Proof
Definitions occuring in Statement : 
trans-equiv-path: trans-equiv-path(G;A;B;f)
, 
univ-trans: univ-trans(G;T)
, 
equiv_path: equiv_path(G;A;B;f)
, 
universe-decode: decode(t)
, 
cubical-universe: c𝕌
, 
cubical-equiv: Equiv(T;A)
, 
cubical-fun: (A ⟶ B)
, 
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
, 
equiv_path: equiv_path(G;A;B;f)
, 
univ-trans: univ-trans(G;T)
, 
let: let, 
all: ∀x:A. B[x]
, 
guard: {T}
, 
prop: ℙ
, 
uimplies: b supposing a
, 
transprt-fun: transprt-fun(Gamma;A;cA)
, 
trans-equiv-path: trans-equiv-path(G;A;B;f)
, 
equiv-path2: equiv-path2(G;A;B;cA;cB;f)
, 
transprt: transprt(G;cA;a0)
, 
comp_term: comp cA [phi ⊢→ u] a0
, 
cc-snd: q
, 
interval-type: 𝕀
, 
cc-fst: p
, 
csm-ap-type: (AF)s
, 
constant-cubical-type: (X)
, 
implies: P 
⇒ Q
, 
csm-comp-structure: (cA)tau
, 
csm+: tau+
, 
csm-comp: G o F
, 
interval-0: 0(𝕀)
, 
csm-id-adjoin: [u]
, 
universe-decode: decode(t)
, 
csm-adjoin: (s;u)
, 
compose: f o g
, 
csm-ap: (s)x
, 
cubical-term-at: u(a)
, 
glue-comp: comp(Glue [phi ⊢→ (T, f)] A) 
, 
csm-id: 1(X)
, 
pi1: fst(t)
, 
csm-ap-term: (t)s
, 
interval-1: 1(𝕀)
, 
cubical-lam: cubical-lam(X;b)
, 
squash: ↓T
, 
true: True
, 
cubical-equiv-by-cases: cubical-equiv-by-cases(G;B;f)
, 
iff: P 
⇐⇒ Q
, 
and: P ∧ Q
, 
rev_implies: P 
⇐ Q
, 
same-cubical-term: X ⊢ u=v:A
, 
cubical-type: {X ⊢ _}
, 
cubical-id-fun: cubical-id-fun(X)
, 
cubical-id-equiv: IdEquiv(X;T)
, 
equiv-fun: equiv-fun(f)
, 
equiv-witness: equiv-witness(f;cntr)
, 
cubical-fst: p.1
, 
cubical-lambda: (λb)
, 
cubical-pair: cubical-pair(u;v)
, 
same-cubical-type: Gamma ⊢ A = B
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
transprt-const: transprt-const(G;cA;a)
, 
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)
, 
equiv-contr: equiv-contr(f;a)
, 
contr-center: contr-center(c)
, 
cubical-snd: p.2
, 
cubical-app: app(w; u)
, 
pi2: snd(t)
, 
cubical-id-is-equiv: cubical-id-is-equiv(X;T)
, 
contr-witness: contr-witness(X;c;p)
, 
cc-adjoin-cube: (v;u)
, 
id-fiber-center: id-fiber-center(X;T)
, 
fiber-member: fiber-member(p)
, 
equiv-path1: equiv-path1(G;A;B;f)
, 
glue-type: Glue [phi ⊢→ (T;w)] A
Lemmas referenced : 
equiv-path2_wf, 
universe-decode_wf, 
universe-comp-fun_wf, 
cubical_set_cumulativity-i-j, 
comp-fun-to-comp-op_wf, 
cube-context-adjoin_wf, 
interval-type_wf, 
equiv-path1_wf, 
composition-structure-cumulativity, 
universe-decode-encode, 
universe-comp-op-encode, 
equal_wf, 
cubical-fun_wf, 
cubical-term-eqcd, 
istype-cubical-term, 
cubical-equiv_wf, 
istype-cubical-universe-term, 
cubical_set_wf, 
csm-glue-comp, 
csm-ap-type_wf, 
cc-fst_wf_interval, 
face-or_wf, 
face-zero_wf, 
cc-snd_wf, 
face-one_wf, 
case-type_wf, 
thin-context-subset, 
same-cubical-type-zero-and-one, 
face-0_wf, 
csm_id_ap_term_lemma, 
cc-snd-1, 
cubical-lam_wf, 
squash_wf, 
true_wf, 
cubical-type-cumulativity2, 
cc-fst_wf, 
cubical-type_wf, 
csm-face-or, 
csm-face-zero, 
csm-face-one, 
csm-case-type, 
q-csm+, 
csm-universe-decode, 
p-csm+-type, 
csm-id-comp-sq, 
cc-snd-0, 
istype-top, 
csm-case-type-comp, 
csm-equiv-fun, 
csm-case-term, 
p-csm+-term, 
composition-structure_wf, 
subtype_rel-equal, 
csm-cubical-equiv, 
istype-universe, 
cube_set_map_wf, 
subtype_rel_self, 
iff_weakening_equal, 
csm-ap-term_wf, 
face-zero-interval-0, 
case-term-1, 
equiv-fun_wf, 
unglue-term-1, 
subset-cubical-type, 
context-subset_wf, 
interval-0_wf, 
context-subset-is-subset, 
face-type_wf, 
face-1-or, 
cubical-fun-subset, 
subset-cubical-term, 
glue-type-1', 
cubical-app_wf_fun, 
csm-comp-structure_wf2, 
case-type-comp-false-true, 
interval-1_wf, 
face-one-interval-1, 
member_wf, 
face-zero-interval-1, 
face-term-implies_wf, 
face-term-implies-1, 
composition-structure-subset, 
csm-cubical-id-equiv, 
csm+_wf_interval, 
csm-id-adjoin_wf-interval-1, 
cubical-id-equiv-subset, 
case-term-0, 
case-type-0, 
subtype_rel_product, 
fset_wf, 
nat_wf, 
I_cube_wf, 
names-hom_wf, 
cube-set-restriction_wf, 
top_wf, 
equals-transprt, 
fiber-comp-subset, 
fiber-comp_wf, 
equiv-fun-cubical-id-equiv, 
equiv-term-0-subset-1, 
face-forall_wf, 
face-forall-q=0-or-q=1, 
face-or-0, 
subset-cubical-term2, 
sub_cubical_set_self, 
cubical-fiber_wf, 
face-or-1, 
glue-term-1', 
fiber-member_wf, 
contractible-type_wf, 
equiv-contr_wf, 
contr-center_wf, 
cubical-id-equiv_wf, 
transprt-const_wf, 
equal_functionality_wrt_subtype_rel2, 
cubical-id-fun_wf, 
fiber-member-transprt-const-fiber-comp, 
cubical-term_wf, 
csm-ap-id-term, 
equiv-path1-0, 
equiv-path1-1, 
transprt_wf, 
csm-id-adjoin_wf, 
csm-interval-type, 
csm-comp-structure_wf, 
csm+_wf, 
transprt-fun_wf, 
comp-op-to-comp-fun_wf2, 
comp-fun-to-comp-op-inverse
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
cut, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
because_Cache, 
hypothesisEquality, 
hypothesis, 
instantiate, 
applyEquality, 
sqequalRule, 
dependent_functionElimination, 
equalityTransitivity, 
equalitySymmetry, 
hyp_replacement, 
independent_isectElimination, 
universeIsType, 
Error :memTop, 
inhabitedIsType, 
lambdaFormation_alt, 
equalityIstype, 
independent_functionElimination, 
lambdaEquality_alt, 
imageElimination, 
natural_numberEquality, 
imageMemberEquality, 
baseClosed, 
universeEquality, 
productElimination, 
applyLambdaEquality, 
setElimination, 
rename, 
dependent_set_memberEquality_alt, 
independent_pairFormation, 
productIsType, 
functionEquality, 
cumulativity, 
functionIsType
Latex:
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(decode(A);decode(B))\}].
    (univ-trans(G;equiv\_path(G;A;B;f))  =  trans-equiv-path(G;A;B;f))
Date html generated:
2020_05_20-PM-07_41_45
Last ObjectModification:
2020_05_01-PM-01_45_52
Theory : cubical!type!theory
Home
Index