Nuprl Definition : sigma-elim-pscm
SigmaElim == λI,x. let a,u,v = x in ((a;u);v)
Definitions occuring in Statement :
psc-adjoin-set: (v;u),
spreadn: spread3,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
spreadn: spread3,
psc-adjoin-set: (v;u)
FDL editor aliases :
sigma-elim-pscm
Latex:
SigmaElim == \mlambda{}I,x. let a,u,v = x in ((a;u);v)
Date html generated:
2018_05_23-AM-08_21_32
Last ObjectModification:
2018_02_21-PM-05_51_29
Theory : presheaf!models!of!type!theory
Home
Index