Nuprl Definition : imp-type
imp-type(A;B) == x,y:Base//(least-equiv(Base;λx,y. ((x = y ∈ A)
⇒ (x = y ∈ B))) x y)
Definitions occuring in Statement :
least-equiv: least-equiv(A;R)
,
quotient: x,y:A//B[x; y]
,
implies: P
⇒ Q
,
apply: f a
,
lambda: λx.A[x]
,
base: Base
,
equal: s = t ∈ T
Definitions occuring in definition :
quotient: x,y:A//B[x; y]
,
apply: f a
,
least-equiv: least-equiv(A;R)
,
base: Base
,
lambda: λx.A[x]
,
implies: P
⇒ Q
,
equal: s = t ∈ T
FDL editor aliases :
imp-type
Latex:
imp-type(A;B) == x,y:Base//(least-equiv(Base;\mlambda{}x,y. ((x = y) {}\mRightarrow{} (x = y))) x y)
Date html generated:
2019_06_20-PM-02_01_39
Last ObjectModification:
2018_10_14-PM-05_23_30
Theory : relations2
Home
Index