Nuprl Definition : contraction-to-extend
contraction-to-extend(Gamma;A;cA;ctr) ==
λH,sigma,phi,u. comp ((cA)sigma)p [phi ⟶ path-eta(contr-path((ctr)sigma;u))] contr-center((ctr)sigma)
Definitions occuring in Statement :
comp_term: comp cA [phi ⟶ u] a0,
csm-comp-structure: (cA)tau,
contr-path: contr-path(c;x),
contr-center: contr-center(c),
path-eta: path-eta(pth),
interval-type: 𝕀,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
comp_term: comp cA [phi ⟶ u] a0,
cube-context-adjoin: X.A,
interval-type: 𝕀,
cc-fst: p,
csm-comp-structure: (cA)tau,
path-eta: path-eta(pth),
contr-path: contr-path(c;x),
contr-center: contr-center(c),
csm-ap-term: (t)s
FDL editor aliases :
contraction-to-extend
Latex:
contraction-to-extend(Gamma;A;cA;ctr) ==
\mlambda{}H,sigma,phi,u. comp ((cA)sigma)p [phi \mvdash{}\mrightarrow{} path-eta(contr-path((ctr)sigma;u))]
contr-center((ctr)sigma)
Date html generated:
2017_02_21-AM-10_58_41
Last ObjectModification:
2017_01_20-PM-11_33_01
Theory : cubical!type!theory
Home
Index