Nuprl Definition : composition-function
composition-function{j:l,i:l}(Gamma;A) ==
H:CubicalSet{j}
⟶ sigma:H.𝕀 j⟶ Gamma
⟶ phi:{H ⊢ _:𝔽}
⟶ u:{H, phi.𝕀 ⊢ _:(A)sigma}
⟶ a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
⟶ {H ⊢ _:((A)sigma)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]}
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-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,
function: x:A ⟶ B[x]
Definitions occuring in definition :
cubical_set: CubicalSet,
cube_set_map: A ⟶ B,
face-type: 𝔽,
cubical-term: {X ⊢ _:A},
cube-context-adjoin: X.A,
interval-type: 𝕀,
function: x:A ⟶ B[x],
interval-0: 0(𝕀),
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
csm-ap-type: (AF)s,
csm-ap-term: (t)s,
csm-id-adjoin: [u],
context-subset: Gamma, phi,
interval-1: 1(𝕀)
FDL editor aliases :
composition-function
Latex:
composition-function\{j:l,i:l\}(Gamma;A) ==
H:CubicalSet\{j\}
{}\mrightarrow{} sigma:H.\mBbbI{} j{}\mrightarrow{} Gamma
{}\mrightarrow{} phi:\{H \mvdash{} \_:\mBbbF{}\}
{}\mrightarrow{} u:\{H, phi.\mBbbI{} \mvdash{} \_:(A)sigma\}
{}\mrightarrow{} a0:\{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][phi |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}
{}\mrightarrow{} \{H \mvdash{} \_:((A)sigma)[1(\mBbbI{})][phi |{}\mrightarrow{} (u)[1(\mBbbI{})]]\}
Date html generated:
2020_05_20-PM-04_20_37
Last ObjectModification:
2020_04_11-PM-04_53_47
Theory : cubical!type!theory
Home
Index