Nuprl Definition : cubical-fun-comp
(f o g) == cubical-lam(G;app((f)p; app((g)p; q)))
Definitions occuring in Statement :
cubical-app: app(w; u),
cubical-lam: cubical-lam(X;b),
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s
Definitions occuring in definition :
cubical-lam: cubical-lam(X;b),
cubical-app: app(w; u),
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
cubical-fun-comp
Latex:
(f o g) == cubical-lam(G;app((f)p; app((g)p; q)))
Date html generated:
2018_05_23-AM-08_58_15
Last ObjectModification:
2017_12_05-PM-04_33_29
Theory : cubical!type!theory
Home
Index