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