Nuprl Definition : sigmacomp
sigmacomp(Gamma;A;B;cA;cB) ==
λI,i,rho,phi,mu,lambda. let v = fill_from_comp(Gamma;A;cA) I i rho phi mu.1 (fst(lambda)) in
let w = cB I i (rho;v) phi mu.2 (snd(lambda)) in
<(v rho (i1)), w>
Definitions occuring in Statement :
fill_from_comp: fill_from_comp(Gamma;A;comp),
cubical-snd: p.2,
cubical-fst: p.1,
cc-adjoin-cube: (v;u),
cubical-type-ap-morph: (u a f),
nc-1: (i1),
add-name: I+i,
let: let,
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
lambda: λx.A[x],
fill_from_comp: fill_from_comp(Gamma;A;comp),
cubical-fst: p.1,
pi1: fst(t),
let: let,
apply: f a,
cc-adjoin-cube: (v;u),
cubical-snd: p.2,
pi2: snd(t),
pair: <a, b>,
cubical-type-ap-morph: (u a f),
add-name: I+i,
nc-1: (i1)
FDL editor aliases :
sigmacomp
Latex:
sigmacomp(Gamma;A;B;cA;cB) ==
\mlambda{}I,i,rho,phi,mu,lambda. let v = fill\_from\_comp(Gamma;A;cA) I i rho phi mu.1 (fst(lambda)) in
let w = cB I i (rho;v) phi mu.2 (snd(lambda)) in
<(v rho (i1)), w>
Date html generated:
2016_05_19-AM-09_50_03
Last ObjectModification:
2016_02_02-PM-06_49_01
Theory : cubical!type!theory
Home
Index