Nuprl Definition : gluetype
gluetype(Gamma;A;phi;T;f) == Glue [phi ⊢→ (T;equiv-fun(f))] A
Definitions occuring in Statement :
glue-type: Glue [phi ⊢→ (T;w)] A,
equiv-fun: equiv-fun(f)
Definitions occuring in definition :
glue-type: Glue [phi ⊢→ (T;w)] A,
equiv-fun: equiv-fun(f)
FDL editor aliases :
gluetype
Latex:
gluetype(Gamma;A;phi;T;f) == Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A
Date html generated:
2020_05_20-PM-07_04_46
Last ObjectModification:
2020_02_18-AM-11_24_03
Theory : cubical!type!theory
Home
Index