Nuprl Definition : cubical-fun-ext
cubical-fun-ext(X;e) == <>((λapp(((e)p)p; q) @ (q)p))
Definitions occuring in Statement :
term-to-path: <>(a),
cubical-path-app: pth @ r,
interval-type: 𝕀,
cubical-app: app(w; u),
cubical-lambda: (λb),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s
Definitions occuring in definition :
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s,
cubical-app: app(w; u),
cubical-path-app: pth @ r,
interval-type: 𝕀,
cube-context-adjoin: X.A,
cubical-lambda: (λb),
term-to-path: <>(a)
FDL editor aliases :
cubical-fun-ext
Latex:
cubical-fun-ext(X;e) == <>((\mlambda{}app(((e)p)p; q) @ (q)p))
Date html generated:
2017_02_21-AM-10_40_21
Last ObjectModification:
2017_02_12-PM-07_02_32
Theory : cubical!type!theory
Home
Index