Nuprl Definition : same-cubical-type
Gamma ⊢ A = B == A = B ∈ {Gamma ⊢ _}
Definitions occuring in Statement :
cubical-type: {X ⊢ _},
equal: s = t ∈ T
Definitions occuring in definition :
equal: s = t ∈ T,
cubical-type: {X ⊢ _}
FDL editor aliases :
same-cubical-type
Latex:
Gamma \mvdash{} A = B == A = B
Date html generated:
2016_05_19-AM-08_36_37
Last ObjectModification:
2016_03_04-PM-11_58_22
Theory : cubical!type!theory
Home
Index