Nuprl Definition : Kan-cubical-identity
Kan(Id_A a b) == <(Id_Kan-type(A) a b), Kan_id_filler(X;A;a;b)>
Definitions occuring in Statement :
Kan_id_filler: Kan_id_filler(X;A;a;b),
cubical-identity: (Id_A a b),
Kan-type: Kan-type(Ak),
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
cubical-identity: (Id_A a b),
Kan-type: Kan-type(Ak),
Kan_id_filler: Kan_id_filler(X;A;a;b)
FDL editor aliases :
Kan-cubical-identity
Latex:
Kan(Id\_A a b) == <(Id\_Kan-type(A) a b), Kan\_id\_filler(X;A;a;b)>
Date html generated:
2016_06_16-PM-08_03_47
Last ObjectModification:
2015_09_23-AM-09_34_48
Theory : cubical!sets
Home
Index