Nuprl Definition : comp_id_mon
(<o,Id> monoid on T) == <T ⟶ T, λx,y. tt, λx,y. tt, λf,g. (f o g), Id, λx.x>
Definitions occuring in Statement :
compose: f o g,
identity: Id,
btrue: tt,
lambda: λx.A[x],
function: x:A ⟶ B[x],
pair: <a, b>
Definitions occuring in definition :
function: x:A ⟶ B[x],
btrue: tt,
compose: f o g,
pair: <a, b>,
identity: Id,
lambda: λx.A[x]
Latex:
(<o,Id> monoid on T) == <T {}\mrightarrow{} T, \mlambda{}x,y. tt, \mlambda{}x,y. tt, \mlambda{}f,g. (f o g), Id, \mlambda{}x.x>
Date html generated:
2016_05_15-PM-00_17_11
Last ObjectModification:
2015_09_23-AM-06_25_08
Theory : groups_1
Home
Index