Nuprl Definition : sigma_comp
sigma_comp(cA;cB) ==
λH,sigma,phi,u,a0. let a = fill (cA)sigma [phi ⊢→ u.1] a0.1 in
let b = comp ((cB)sigma+)[a] [phi ⊢→ u.2] a0.2 in
cubical-pair((a)[1(𝕀)];b)
Definitions occuring in Statement :
fill_term: fill cA [phi ⊢→ u] a0,
comp_term: comp cA [phi ⊢→ u] a0,
csm-comp-structure: (cA)tau,
interval-1: 1(𝕀),
interval-type: 𝕀,
cubical-pair: cubical-pair(u;v),
cubical-snd: p.2,
cubical-fst: p.1,
csm+: tau+,
csm-id-adjoin: [u],
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s,
let: let,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
fill_term: fill cA [phi ⊢→ u] a0,
cubical-fst: p.1,
let: let,
comp_term: comp cA [phi ⊢→ u] a0,
csm-comp-structure: (cA)tau,
csm-ap-type: (AF)s,
csm+: tau+,
cube-context-adjoin: X.A,
interval-type: 𝕀,
cubical-snd: p.2,
cubical-pair: cubical-pair(u;v),
csm-ap-term: (t)s,
csm-id-adjoin: [u],
interval-1: 1(𝕀)
FDL editor aliases :
sigma_comp
Latex:
sigma\_comp(cA;cB) ==
\mlambda{}H,sigma,phi,u,a0. let a = fill (cA)sigma [phi \mvdash{}\mrightarrow{} u.1] a0.1 in
let b = comp ((cB)sigma+)[a] [phi \mvdash{}\mrightarrow{} u.2] a0.2 in
cubical-pair((a)[1(\mBbbI{})];b)
Date html generated:
2016_06_16-PM-02_12_56
Last ObjectModification:
2016_06_02-AM-09_36_32
Theory : cubical!type!theory
Home
Index