Nuprl Definition : composition-structure
Gamma ⊢ Compositon(A) ==
{comp:composition-function{j:l,i:l}(Gamma;A)| uniform-comp-function{j:l, i:l}(Gamma; A; comp)}
Definitions occuring in Statement :
uniform-comp-function: uniform-comp-function{j:l, i:l}(Gamma; A; comp),
composition-function: composition-function{j:l,i:l}(Gamma;A),
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
composition-function: composition-function{j:l,i:l}(Gamma;A),
uniform-comp-function: uniform-comp-function{j:l, i:l}(Gamma; A; comp)
FDL editor aliases :
composition-structure
Latex:
Gamma \mvdash{} Compositon(A) ==
\{comp:composition-function\{j:l,i:l\}(Gamma;A)| uniform-comp-function\{j:l, i:l\}(Gamma; A; comp)\}
Date html generated:
2020_05_20-PM-04_22_03
Last ObjectModification:
2020_04_10-PM-05_40_41
Theory : cubical!type!theory
Home
Index