Nuprl Definition : glue-morph
glue-morph(Gamma;A;phi;T;w;I;rho;J;f;u) ==
if (phi(rho)==1)
then (u rho f)
else let t,a = u
in if (phi(f(rho))==1) then t J f else <λK,g. (t K f ⋅ g), (a rho f)> fi
fi
Definitions occuring in Statement :
cubical-term-at: u(a),
cubical-type-ap-morph: (u a f),
fl-eq: (x==y),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
nh-comp: g ⋅ f,
lattice-1: 1,
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
Definitions occuring in definition :
spread: spread def,
ifthenelse: if b then t else f fi ,
fl-eq: (x==y),
cubical-term-at: u(a),
cube-set-restriction: f(s),
lattice-1: 1,
face_lattice: face_lattice(I),
pair: <a, b>,
lambda: λx.A[x],
apply: f a,
nh-comp: g ⋅ f,
cubical-type-ap-morph: (u a f)
FDL editor aliases :
glue-morph
Latex:
glue-morph(Gamma;A;phi;T;w;I;rho;J;f;u) ==
if (phi(rho)==1)
then (u rho f)
else let t,a = u
in if (phi(f(rho))==1) then t J f else <\mlambda{}K,g. (t K f \mcdot{} g), (a rho f)> fi
fi
Date html generated:
2016_05_19-AM-11_16_03
Last ObjectModification:
2016_02_24-PM-04_55_43
Theory : cubical!type!theory
Home
Index