Nuprl Definition : contractible-type
Contractible(A) == Σ A Π(A)p (Path_((A)p)p (q)p q)
Definitions occuring in Statement :
path-type: (Path_A a b),
cubical-sigma: Σ 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
Definitions occuring in definition :
cubical-sigma: Σ A B,
cubical-pi: ΠA B,
path-type: (Path_A a b),
cube-context-adjoin: X.A,
csm-ap-type: (AF)s,
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
contractible-type
contractible-type
Latex:
Contractible(A) == \mSigma{} A \mPi{}(A)p (Path\_((A)p)p (q)p q)
Date html generated:
2016_06_16-PM-01_50_13
Last ObjectModification:
2016_06_03-PM-02_06_19
Theory : cubical!type!theory
Home
Index