Nuprl Definition : filling-structure
Gamma ⊢ Filling(A) == {fill:filling-function{j:l, i:l}(Gamma;A)| uniform-filling-function{j:l, i:l}(Gamma;A;fill)}
Definitions occuring in Statement :
uniform-filling-function: uniform-filling-function{j:l, i:l}(Gamma;A;fill),
filling-function: filling-function{j:l, i:l}(Gamma;A),
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
filling-function: filling-function{j:l, i:l}(Gamma;A),
uniform-filling-function: uniform-filling-function{j:l, i:l}(Gamma;A;fill)
FDL editor aliases :
filling-structure
Latex:
Gamma \mvdash{} Filling(A) ==
\{fill:filling-function\{j:l, i:l\}(Gamma;A)| uniform-filling-function\{j:l, i:l\}(Gamma;A;fill)\}
Date html generated:
2020_05_20-PM-04_41_26
Last ObjectModification:
2020_04_11-AM-10_42_35
Theory : cubical!type!theory
Home
Index