Nuprl Definition : csm
CSM(V) ==
C:Type
× M:Type
× A:V ⟶ Type
× B:V ⟶ Type
× G:V ⟶ V ⟶ 𝔹
× i:V ⟶ (A i)
× i:V ⟶ (A i) ⟶ (B i) ⟶ (C + M) ⟶ (A i)
× (i:V ⟶ {j:V| ↑(G i j)} ⟶ (A i) ⟶ (B i) ⟶ (C + M) ⟶ (M + Top))
Definitions occuring in Statement :
assert: ↑b,
bool: 𝔹,
top: Top,
set: {x:A| B[x]} ,
apply: f a,
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],
set: {x:A| B[x]} ,
assert: ↑b,
apply: f a,
function: x:A ⟶ B[x],
union: left + right,
top: Top
FDL editor aliases :
csm
Latex:
CSM(V) ==
C:Type
\mtimes{} M:Type
\mtimes{} A:V {}\mrightarrow{} Type
\mtimes{} B:V {}\mrightarrow{} Type
\mtimes{} G:V {}\mrightarrow{} V {}\mrightarrow{} \mBbbB{}
\mtimes{} i:V {}\mrightarrow{} (A i)
\mtimes{} i:V {}\mrightarrow{} (A i) {}\mrightarrow{} (B i) {}\mrightarrow{} (C + M) {}\mrightarrow{} (A i)
\mtimes{} (i:V {}\mrightarrow{} \{j:V| \muparrow{}(G i j)\} {}\mrightarrow{} (A i) {}\mrightarrow{} (B i) {}\mrightarrow{} (C + M) {}\mrightarrow{} (M + Top))
Date html generated:
2016_05_15-PM-05_09_25
Last ObjectModification:
2015_09_23-AM-07_51_34
Theory : general
Home
Index