Nuprl Definition : comp-op-to-comp-fun
comp-op-to-comp-fun(cA) == ⌜λH,sigma,phi,u,a0. comp csm-composition(sigma;cA) [phi ⊢→ u] a0⌝
Definitions occuring in Statement :
composition-term: comp cA [phi ⊢→ u] a0,
csm-composition: csm-composition(sigma;comp),
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
composition-term: comp cA [phi ⊢→ u] a0,
csm-composition: csm-composition(sigma;comp)
FDL editor aliases :
comp-op-to-comp-fun
Latex:
comp-op-to-comp-fun(cA) == \mkleeneopen{}\mlambda{}H,sigma,phi,u,a0. comp csm-composition(sigma;cA) [phi \mvdash{}\mrightarrow{} u] a0\mkleeneclose{}
Date html generated:
2016_05_19-AM-10_29_26
Last ObjectModification:
2016_03_16-PM-05_15_21
Theory : cubical!type!theory
Home
Index