Nuprl Definition : same-cubical-term
X ⊢ u=v:A == u = v ∈ {X ⊢ _:A}
Definitions occuring in Statement :
cubical-term: {X ⊢ _:A},
equal: s = t ∈ T
Definitions occuring in definition :
equal: s = t ∈ T,
cubical-term: {X ⊢ _:A}
FDL editor aliases :
same-cubical-term
Latex:
X \mvdash{} u=v:A == u = v
Date html generated:
2016_05_19-AM-08_36_52
Last ObjectModification:
2016_03_31-AM-10_09_19
Theory : cubical!type!theory
Home
Index