Nuprl Definition : type-functor
Functor ==
{p:F:Type ⟶ Type × (⋂T,S:Type. ((T ⟶ S) ⟶ (F T) ⟶ (F S)))|
let F,M = p
in (∀T:Type. ((M (λx.x)) = (λx.x) ∈ ((F T) ⟶ (F T))))
∧ (∀T,S,V:Type. ∀f:T ⟶ S. ∀g:S ⟶ V. ((M (g o f)) = ((M g) o (M f)) ∈ ((F T) ⟶ (F V))))}
Definitions occuring in Statement :
compose: f o g,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
spread: spread def,
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
product: x:A × B[x],
isect: ⋂x:A. B[x],
spread: spread def,
and: P ∧ Q,
lambda: λx.A[x],
universe: Type,
all: ∀x:A. B[x],
equal: s = t ∈ T,
function: x:A ⟶ B[x],
compose: f o g,
apply: f a
FDL editor aliases :
type-functor
Latex:
Functor ==
\{p:F:Type {}\mrightarrow{} Type \mtimes{} (\mcap{}T,S:Type. ((T {}\mrightarrow{} S) {}\mrightarrow{} (F T) {}\mrightarrow{} (F S)))|
let F,M = p
in (\mforall{}T:Type. ((M (\mlambda{}x.x)) = (\mlambda{}x.x)))
\mwedge{} (\mforall{}T,S,V:Type. \mforall{}f:T {}\mrightarrow{} S. \mforall{}g:S {}\mrightarrow{} V. ((M (g o f)) = ((M g) o (M f))))\}
Date html generated:
2016_05_15-PM-01_44_37
Last ObjectModification:
2015_09_23-AM-07_36_59
Theory : basic
Home
Index