Nuprl Definition : trans-const-path
trans-const-path(G;cA;a) == <>(rev_fill_term(G;(cA)p;0(𝔽);discr(⋅);a))
Definitions occuring in Statement :
rev_fill_term: rev_fill_term(Gamma;cA;phi;u;a1),
csm-comp-structure: (cA)tau,
term-to-path: <>(a),
face-0: 0(𝔽),
interval-type: 𝕀,
discrete-cubical-term: discr(t),
cc-fst: p,
cube-context-adjoin: X.A,
it: ⋅
Definitions occuring in definition :
it: ⋅,
discrete-cubical-term: discr(t),
face-0: 0(𝔽),
cc-fst: p,
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm-comp-structure: (cA)tau,
rev_fill_term: rev_fill_term(Gamma;cA;phi;u;a1),
term-to-path: <>(a)
FDL editor aliases :
trans-const-path
Latex:
trans-const-path(G;cA;a) == <>(rev\_fill\_term(G;(cA)p;0(\mBbbF{});discr(\mcdot{});a))
Date html generated:
2017_01_10-AM-09_52_17
Last ObjectModification:
2017_01_05-PM-04_55_54
Theory : cubical!type!theory
Home
Index