Nuprl Definition : comp_term
comp cA [phi ⊢→ u] a0 == cA Gamma 1(Gamma.𝕀) phi u a0
Definitions occuring in Statement :
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm-id: 1(X),
apply: f a
Definitions occuring in definition :
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm-id: 1(X),
apply: f a
FDL editor aliases :
comp_term
Latex:
comp cA [phi \mvdash{}\mrightarrow{} u] a0 == cA Gamma 1(Gamma.\mBbbI{}) phi u a0
Date html generated:
2016_05_19-AM-10_41_32
Last ObjectModification:
2016_04_13-PM-01_33_41
Theory : cubical!type!theory
Home
Index