Nuprl Definition : universe-comp-op
compOp(t) == λI,i,rho. ((snd(t(rho))) I i 1)
Definitions occuring in Statement :
cubical-term-at: u(a),
add-name: I+i,
nh-id: 1,
pi2: snd(t),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
apply: f a,
pi2: snd(t),
cubical-term-at: u(a),
add-name: I+i,
nh-id: 1
FDL editor aliases :
universe-comp-op
Latex:
compOp(t) == \mlambda{}I,i,rho. ((snd(t(rho))) I i 1)
Date html generated:
2016_07_08-PM-10_28_54
Last ObjectModification:
2016_06_20-PM-00_47_48
Theory : cubical!type!theory
Home
Index