Nuprl Definition : uniform-extend
Gamma ⊢ Extension(A) == {ext:extension-fun{i:l}(Gamma;A)| uniform-extension-fun{i:l}(Gamma;A;ext)}
Definitions occuring in Statement :
uniform-extension-fun: uniform-extension-fun{i:l}(Gamma;A;ext),
extension-fun: extension-fun{i:l}(Gamma;A),
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
extension-fun: extension-fun{i:l}(Gamma;A),
uniform-extension-fun: uniform-extension-fun{i:l}(Gamma;A;ext)
FDL editor aliases :
uniform-extend
Latex:
Gamma \mvdash{} Extension(A) == \{ext:extension-fun\{i:l\}(Gamma;A)| uniform-extension-fun\{i:l\}(Gamma;A;ext)\}
Date html generated:
2017_02_21-AM-10_57_27
Last ObjectModification:
2017_01_20-PM-06_06_02
Theory : cubical!type!theory
Home
Index