Nuprl Definition : provisional-type
Provisional(T) == x,y:ok:ℙ × T supposing ↓ok//((↓fst(x) ⇐⇒ ↓fst(y)) ∧ ((↓fst(x)) ⇒ ((snd(x)) = (snd(y)) ∈ T)))
Definitions occuring in Statement :
quotient: x,y:A//B[x; y],
uimplies: b supposing a,
prop: ℙ,
pi1: fst(t),
pi2: snd(t),
iff: P ⇐⇒ Q,
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
product: x:A × B[x],
equal: s = t ∈ T
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
product: x:A × B[x],
prop: ℙ,
uimplies: b supposing a,
and: P ∧ Q,
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
squash: ↓T,
pi1: fst(t),
equal: s = t ∈ T,
pi2: snd(t)
FDL editor aliases :
prov-type
prov-type
prov-type
Latex:
Provisional(T) ==
x,y:ok:\mBbbP{} \mtimes{} T supposing \mdownarrow{}ok//((\mdownarrow{}fst(x) \mLeftarrow{}{}\mRightarrow{} \mdownarrow{}fst(y)) \mwedge{} ((\mdownarrow{}fst(x)) {}\mRightarrow{} ((snd(x)) = (snd(y)))))
Date html generated:
2020_05_20-AM-08_00_37
Last ObjectModification:
2020_05_17-PM-06_47_01
Theory : monads
Home
Index