Nuprl Definition : constrained-cubical-term
{Gamma ⊢ _:A[phi |⟶ t]} == {a:{Gamma ⊢ _:A}| t = a ∈ {Gamma, phi ⊢ _:A}}
Definitions occuring in Statement :
context-subset: Gamma, phi,
cubical-term: {X ⊢ _:A},
set: {x:A| B[x]} ,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
equal: s = t ∈ T,
cubical-term: {X ⊢ _:A},
context-subset: Gamma, phi
FDL editor aliases :
constrained-cubical-term
Latex:
\{Gamma \mvdash{} \_:A[phi |{}\mrightarrow{} t]\} == \{a:\{Gamma \mvdash{} \_:A\}| t = a\}
Date html generated:
2016_05_19-AM-08_35_34
Last ObjectModification:
2016_04_04-PM-09_49_40
Theory : cubical!type!theory
Home
Index