Nuprl Definition : comp-to-fill
comp-to-fill(Gamma;cA) == λH,sigma,phi,u,a0. (cA H.𝕀 sigma o m ((phi)p ∨ (q=0)) ((u)m ∨ ((a0)p)m) (a0)p)
Definitions occuring in Statement :
csm-m: m,
case-term: (u ∨ v),
face-zero: (i=0),
face-or: (a ∨ b),
interval-type: 𝕀,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-comp: G o F,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
apply: f a,
csm-comp: G o F,
cube-context-adjoin: X.A,
interval-type: 𝕀,
face-or: (a ∨ b),
face-zero: (i=0),
cc-snd: q,
case-term: (u ∨ v),
csm-m: m,
csm-ap-term: (t)s,
cc-fst: p
FDL editor aliases :
comp-to-fill
Latex:
comp-to-fill(Gamma;cA) ==
\mlambda{}H,sigma,phi,u,a0. (cA H.\mBbbI{} sigma o m ((phi)p \mvee{} (q=0)) ((u)m \mvee{} ((a0)p)m) (a0)p)
Date html generated:
2016_05_19-AM-10_46_43
Last ObjectModification:
2016_04_05-PM-06_05_24
Theory : cubical!type!theory
Home
Index