Nuprl Definition : TRO
TRO{i:l}() == {tr:A:Type × (A ⟶ A ⟶ ℙ)| Trans(fst(tr);a1,a2.a1 (snd(tr)) a2)}
Definitions occuring in Statement :
trans: Trans(T;x,y.E[x; y]),
prop: ℙ,
infix_ap: x f y,
pi1: fst(t),
pi2: snd(t),
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions occuring in definition :
set: {x:A| B[x]} ,
product: x:A × B[x],
universe: Type,
function: x:A ⟶ B[x],
prop: ℙ,
trans: Trans(T;x,y.E[x; y]),
pi1: fst(t),
infix_ap: x f y,
pi2: snd(t)
FDL editor aliases :
TRO
Latex:
TRO\{i:l\}() == \{tr:A:Type \mtimes{} (A {}\mrightarrow{} A {}\mrightarrow{} \mBbbP{})| Trans(fst(tr);a1,a2.a1 (snd(tr)) a2)\}
Date html generated:
2016_05_15-PM-04_13_39
Last ObjectModification:
2015_09_23-AM-07_47_06
Theory : general
Home
Index