Nuprl Definition : algebra_sig
algebra_sig{i:l}(A) ==
car:Type
× eq:car ⟶ car ⟶ 𝔹
× le:car ⟶ car ⟶ 𝔹
× plus:car ⟶ car ⟶ car
× zero:car
× minus:car ⟶ car
× times:car ⟶ car ⟶ car
× one:car
× div:car ⟶ car ⟶ (car?)
× (A ⟶ car ⟶ car)
Definitions occuring in Statement :
bool: 𝔹,
unit: Unit,
function: x:A ⟶ B[x],
product: x:A × B[x],
union: left + right,
universe: Type
Definitions occuring in definition :
universe: Type,
bool: 𝔹,
product: x:A × B[x],
union: left + right,
unit: Unit,
function: x:A ⟶ B[x]
FDL editor aliases :
algebra_sig
Latex:
algebra\_sig\{i:l\}(A) ==
car:Type
\mtimes{} eq:car {}\mrightarrow{} car {}\mrightarrow{} \mBbbB{}
\mtimes{} le:car {}\mrightarrow{} car {}\mrightarrow{} \mBbbB{}
\mtimes{} plus:car {}\mrightarrow{} car {}\mrightarrow{} car
\mtimes{} zero:car
\mtimes{} minus:car {}\mrightarrow{} car
\mtimes{} times:car {}\mrightarrow{} car {}\mrightarrow{} car
\mtimes{} one:car
\mtimes{} div:car {}\mrightarrow{} car {}\mrightarrow{} (car?)
\mtimes{} (A {}\mrightarrow{} car {}\mrightarrow{} car)
Date html generated:
2016_05_16-AM-07_25_50
Last ObjectModification:
2015_09_23-AM-09_50_54
Theory : algebras_1
Home
Index