Nuprl Definition : compatible-system
compatible-system{i:l}(Gamma;sys) ==
(∀phiA1,phiA2∈sys. let phi1,A1 = phiA1
in let phi2,A2 = phiA2
in A1 = A2 ∈ {Gamma, (phi1 ∧ phi2) ⊢ _})
Definitions occuring in Statement :
context-subset: Gamma, phi,
face-and: (a ∧ b),
cubical-type: {X ⊢ _},
pairwise: (∀x,y∈L. P[x; y]),
spread: spread def,
equal: s = t ∈ T
Definitions occuring in definition :
pairwise: (∀x,y∈L. P[x; y]),
spread: spread def,
equal: s = t ∈ T,
cubical-type: {X ⊢ _},
context-subset: Gamma, phi,
face-and: (a ∧ b)
FDL editor aliases :
compatible-system
Latex:
compatible-system\{i:l\}(Gamma;sys) ==
(\mforall{}phiA1,phiA2\mmember{}sys. let phi1,A1 = phiA1
in let phi2,A2 = phiA2
in A1 = A2)
Date html generated:
2016_05_19-AM-08_50_08
Last ObjectModification:
2016_03_04-PM-02_39_44
Theory : cubical!type!theory
Home
Index