Nuprl Definition : compatible-composition
compatible-composition{j:l, i:l}(Gamma; phi; psi; A; B; cA; cB) ==
∀H:j⊢. ∀sigma:H.𝕀 j⟶ Gamma, (phi ∧ psi). ∀chi:{H ⊢ _:𝔽}. ∀u:{H, chi.𝕀 ⊢ _:(A)sigma}.
∀a0:{H ⊢ _:((A)sigma)[0(𝕀)][chi |⟶ (u)[0(𝕀)]]}.
((cB H sigma chi u a0) = (cA H sigma chi u a0) ∈ {H ⊢ _:((A)sigma)[1(𝕀)]})
Definitions occuring in Statement :
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
context-subset: Gamma, phi,
face-and: (a ∧ b),
face-type: 𝔽,
interval-1: 1(𝕀),
interval-0: 0(𝕀),
interval-type: 𝕀,
csm-id-adjoin: [u],
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
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-and: (a ∧ b),
face-type: 𝔽,
cube-context-adjoin: X.A,
interval-type: 𝕀,
all: ∀x:A. B[x],
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
csm-ap-term: (t)s,
context-subset: Gamma, phi,
interval-0: 0(𝕀),
equal: s = t ∈ T,
cubical-term: {X ⊢ _:A},
csm-id-adjoin: [u],
interval-1: 1(𝕀),
csm-ap-type: (AF)s,
apply: f a
Latex:
compatible-composition\{j:l, i:l\}(Gamma; phi; psi; A; B; cA; cB) ==
\mforall{}H:j\mvdash{}. \mforall{}sigma:H.\mBbbI{} j{}\mrightarrow{} Gamma, (phi \mwedge{} psi). \mforall{}chi:\{H \mvdash{} \_:\mBbbF{}\}. \mforall{}u:\{H, chi.\mBbbI{} \mvdash{} \_:(A)sigma\}.
\mforall{}a0:\{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][chi |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}.
((cB H sigma chi u a0) = (cA H sigma chi u a0))
Date html generated:
2020_05_20-PM-05_14_46
Last ObjectModification:
2020_04_14-PM-06_45_07
Theory : cubical!type!theory
Home
Index