Nuprl Definition : cubical-identity
(Id_A a b) == <λI,alpha. cubical-path(X;A;a;b;I;alpha), λI,K,f,alpha,p. I-path-morph(X;A;I;K;f;alpha;p)>
Definitions occuring in Statement :
cubical-path: cubical-path(X;A;a;b;I;alpha),
I-path-morph: I-path-morph(X;A;I;K;f;alpha;p),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
cubical-path: cubical-path(X;A;a;b;I;alpha),
lambda: λx.A[x],
I-path-morph: I-path-morph(X;A;I;K;f;alpha;p)
FDL editor aliases :
cubical-identity
Latex:
(Id\_A a b) == <\mlambda{}I,alpha. cubical-path(X;A;a;b;I;alpha), \mlambda{}I,K,f,alpha,p. I-path-morph(X;A;I;K;f;alph\000Ca;p)>
Date html generated:
2016_06_16-PM-07_31_32
Last ObjectModification:
2015_09_23-AM-09_34_23
Theory : cubical!sets
Home
Index