Nuprl Definition : closed-cubical-universe
cc𝕌 == <λI.FibrantType(formal-cube(I)), λI,J,f,FT. csm-fibrant-type(formal-cube(I);formal-cube(J);<f>;FT)>
Definitions occuring in Statement :
csm-fibrant-type: csm-fibrant-type(G;H;s;FT),
fibrant-type: FibrantType(X),
context-map: <rho>,
formal-cube: formal-cube(I),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
fibrant-type: FibrantType(X),
lambda: λx.A[x],
csm-fibrant-type: csm-fibrant-type(G;H;s;FT),
context-map: <rho>,
formal-cube: formal-cube(I)
FDL editor aliases :
cc-univ
Latex:
cc\mBbbU{} ==
<\mlambda{}I.FibrantType(formal-cube(I)), \mlambda{}I,J,f,FT. csm-fibrant-type(formal-cube(I);formal-cube(J);<f>FT)\000C>
Date html generated:
2020_05_20-PM-07_05_31
Last ObjectModification:
2020_03_20-AM-10_37_30
Theory : cubical!type!theory
Home
Index