Nuprl Definition : uniform-comp-function
uniform-comp-function{j:l, i:l}(Gamma; A; comp) ==
∀H,K:j⊢. ∀tau:K j⟶ H. ∀sigma:H.𝕀 j⟶ Gamma. ∀phi:{H ⊢ _:𝔽}. ∀u:{H, phi.𝕀 ⊢ _:(A)sigma}.
∀a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}.
((comp H sigma phi u a0)tau
= (comp K sigma o tau+ (phi)tau (u)tau+ (a0)tau)
∈ {K ⊢ _:(((A)sigma)[1(𝕀)])tau[(phi)tau |⟶ ((u)[1(𝕀)])tau]})
Definitions occuring in Statement :
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
context-subset: Gamma, phi,
face-type: 𝔽,
interval-1: 1(𝕀),
interval-0: 0(𝕀),
interval-type: 𝕀,
csm+: tau+,
csm-id-adjoin: [u],
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
csm-comp: G o F,
cube_set_map: A ⟶ B,
cubical_set: CubicalSet,
all: ∀x:A. B[x],
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
cubical_set: CubicalSet,
cube_set_map: A ⟶ B,
face-type: 𝔽,
cubical-term: {X ⊢ _:A},
all: ∀x:A. B[x],
interval-0: 0(𝕀),
equal: s = t ∈ T,
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
csm-ap-type: (AF)s,
csm-id-adjoin: [u],
context-subset: Gamma, phi,
interval-1: 1(𝕀),
apply: f a,
csm-comp: G o F,
cube-context-adjoin: X.A,
csm+: tau+,
interval-type: 𝕀,
csm-ap-term: (t)s
Latex:
uniform-comp-function\{j:l, i:l\}(Gamma; A; comp) ==
\mforall{}H,K:j\mvdash{}. \mforall{}tau:K j{}\mrightarrow{} H. \mforall{}sigma:H.\mBbbI{} j{}\mrightarrow{} Gamma. \mforall{}phi:\{H \mvdash{} \_:\mBbbF{}\}. \mforall{}u:\{H, phi.\mBbbI{} \mvdash{} \_:(A)sigma\}.
\mforall{}a0:\{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][phi |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}.
((comp H sigma phi u a0)tau = (comp K sigma o tau+ (phi)tau (u)tau+ (a0)tau))
Date html generated:
2020_05_20-PM-04_21_19
Last ObjectModification:
2020_04_11-PM-04_54_35
Theory : cubical!type!theory
Home
Index