Nuprl Definition : discrete-family
discrete-family(A;a.B[a]) == <λI,alpha. B[snd(alpha)], λI,J,f,alpha,x. x>
Definitions occuring in Statement :
pi2: snd(t),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
lambda: λx.A[x],
pi2: snd(t),
pair: <a, b>
FDL editor aliases :
discrete-family
Latex:
discrete-family(A;a.B[a]) == <\mlambda{}I,alpha. B[snd(alpha)], \mlambda{}I,J,f,alpha,x. x>
Date html generated:
2017_02_21-AM-10_44_35
Last ObjectModification:
2017_02_15-PM-00_00_48
Theory : cubical!type!theory
Home
Index