Nuprl Definition : fun-comp
fun-comp(Gamma;A;B;cA;cB) == pi-comp(Gamma;A;(B)p;cA;(cB)p)
Definitions occuring in Statement :
pi-comp: pi-comp(Gamma;A;B;cA;cB),
csm-composition: (comp)sigma,
cc-fst: p,
csm-ap-type: (AF)s
Definitions occuring in definition :
cc-fst: p,
csm-composition: (comp)sigma,
csm-ap-type: (AF)s,
pi-comp: pi-comp(Gamma;A;B;cA;cB)
FDL editor aliases :
fun-comp
Latex:
fun-comp(Gamma;A;B;cA;cB) == pi-comp(Gamma;A;(B)p;cA;(cB)p)
Date html generated:
2017_01_10-AM-09_08_03
Last ObjectModification:
2016_12_02-PM-09_36_48
Theory : cubical!type!theory
Home
Index