Nuprl Definition : h-level
h-level(X;n;A) == primrec(n;λA.Contractible(A);λi,r,A. (r ΠA Π(A)p (Path_((A)p)p (q)p q))) A
Definitions occuring in Statement :
contractible-type: Contractible(A),
path-type: (Path_A a b),
cubical-pi: ΠA B,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s,
primrec: primrec(n;b;c),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s,
csm-ap-type: (AF)s,
cube-context-adjoin: X.A,
path-type: (Path_A a b),
cubical-pi: ΠA B,
apply: f a,
lambda: λx.A[x],
contractible-type: Contractible(A),
primrec: primrec(n;b;c)
FDL editor aliases :
h-level
Latex:
h-level(X;n;A) == primrec(n;\mlambda{}A.Contractible(A);\mlambda{}i,r,A. (r \mPi{}A \mPi{}(A)p (Path\_((A)p)p (q)p q))) A
Date html generated:
2017_01_10-AM-09_07_07
Last ObjectModification:
2016_12_05-PM-03_04_46
Theory : cubical!type!theory
Home
Index