Nuprl Definition : pi_comp
pi_comp(X;A;cA;cB) ==
λH,sigma,phi,u,a0. let v = revfill(H.((A)sigma)[1(𝕀)];((cA)sigma)p+;q) in
(λcomp (cB)(sigma o p+;v) [(phi)p ⟶ app((u)p+; v)] app((a0)p; (v)[0(𝕀)]))
Definitions occuring in Statement :
revfill: revfill(Gamma;cA;a1),
comp_term: comp cA [phi ⟶ u] a0,
csm-comp-structure: (cA)tau,
interval-1: 1(𝕀),
interval-0: 0(𝕀),
interval-type: 𝕀,
cubical-app: app(w; u),
cubical-lambda: (λb),
csm+: tau+,
csm-id-adjoin: [u],
csm-adjoin: (s;u),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s,
csm-comp: G o F,
let: let,
lambda: λx.A[x]
Definitions occuring in definition :
interval-0: 0(𝕀),
csm-id-adjoin: [u],
csm-ap-term: (t)s,
cc-fst: p,
cubical-app: app(w; u),
interval-type: 𝕀,
csm-ap-type: (AF)s,
interval-1: 1(𝕀),
cube-context-adjoin: X.A,
csm+: tau+,
csm-comp: G o F,
csm-adjoin: (s;u),
csm-comp-structure: (cA)tau,
comp_term: comp cA [phi ⟶ u] a0,
cubical-lambda: (λb),
cc-snd: q,
revfill: revfill(Gamma;cA;a1),
let: let,
lambda: λx.A[x]
FDL editor aliases :
pi_comp
Latex:
pi\_comp(X;A;cA;cB) ==
\mlambda{}H,sigma,phi,u,a0. let v = revfill(H.((A)sigma)[1(\mBbbI{})];((cA)sigma)p+;q) in
(\mlambda{}comp (cB)(sigma o p+;v) [(phi)p \mvdash{}\mrightarrow{} app((u)p+; v)] app((a0)p; (v)[0(\mBbbI{})]))
Date html generated:
2017_01_10-AM-09_55_04
Last ObjectModification:
2016_12_21-PM-06_27_11
Theory : cubical!type!theory
Home
Index