Nuprl Definition : cubical-sigma-fun
cubical-sigma-fun(G;A;B;f) == cubical-lam(G;cubical-pair(q.1;app(app(((λf))p; q.1); q.2)))
Definitions occuring in Statement :
cubical-pair: cubical-pair(u;v)
,
cubical-snd: p.2
,
cubical-fst: p.1
,
cubical-app: app(w; u)
,
cubical-lam: cubical-lam(X;b)
,
cubical-lambda: (λb)
,
cc-snd: q
,
cc-fst: p
,
csm-ap-term: (t)s
Definitions occuring in definition :
cubical-lam: cubical-lam(X;b)
,
cubical-pair: cubical-pair(u;v)
,
cubical-app: app(w; u)
,
csm-ap-term: (t)s
,
cc-fst: p
,
cubical-lambda: (λb)
,
cubical-fst: p.1
,
cubical-snd: p.2
,
cc-snd: q
FDL editor aliases :
cubical-sigma-fun
Latex:
cubical-sigma-fun(G;A;B;f) == cubical-lam(G;cubical-pair(q.1;app(app(((\mlambda{}f))p; q.1); q.2)))
Date html generated:
2018_05_23-AM-09_13_05
Last ObjectModification:
2017_11_08-AM-11_56_19
Theory : cubical!type!theory
Home
Index