Nuprl Definition : base-type-family
base-type-family{i:l}(A;a.B[a]) == ∀[a,a':Base]. B[a] = B[a'] ∈ Type supposing a = a' ∈ A
Definitions occuring in Statement :
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
base: Base,
universe: Type,
equal: s = t ∈ T
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
base: Base,
uimplies: b supposing a,
equal: s = t ∈ T,
universe: Type
FDL editor aliases :
base-type-family
Latex:
base-type-family\{i:l\}(A;a.B[a]) == \mforall{}[a,a':Base]. B[a] = B[a'] supposing a = a'
Date html generated:
2016_05_13-PM-03_53_25
Last ObjectModification:
2015_09_22-PM-05_45_30
Theory : per!type
Home
Index