Nuprl Definition : trivial-section

The trivial section, () must satisfy I,0 |- ():A subset-iota().
But since the "cubical subset" I,0 is empty, everything satisfies this
property; so we could define it to be anything we like.
(We chose ⌜⋅⌝.)⋅

() == ⋅

Definitions occuring in Statement : it: ⋅
Definitions occuring in definition : it: ⋅
FDL editor aliases : trivial-section

Latex:
() == \mcdot{} Date html generated: 2016_07_08-PM-06_30_56 Last ObjectModification: 2015_11_11-PM-09_12_36 Theory : cubical!type!theory Home Index