Nuprl Definition : extension-fun
extension-fun{i:l}(Gamma;A) ==
H:CubicalSet ⟶ sigma:H ⟶ Gamma ⟶ phi:{H ⊢ _:𝔽} ⟶ u:{H, phi ⊢ _:(A)sigma} ⟶ {H ⊢ _:(A)sigma[phi |⟶ u]}
Definitions occuring in Statement :
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
context-subset: Gamma, phi,
face-type: 𝔽,
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: 𝔽,
function: x:A ⟶ B[x],
cubical-term: {X ⊢ _:A},
context-subset: Gamma, phi,
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
csm-ap-type: (AF)s
FDL editor aliases :
extension-fun
Latex:
extension-fun\{i:l\}(Gamma;A) ==
H:CubicalSet
{}\mrightarrow{} sigma:H {}\mrightarrow{} Gamma
{}\mrightarrow{} phi:\{H \mvdash{} \_:\mBbbF{}\}
{}\mrightarrow{} u:\{H, phi \mvdash{} \_:(A)sigma\}
{}\mrightarrow{} \{H \mvdash{} \_:(A)sigma[phi |{}\mrightarrow{} u]\}
Date html generated:
2017_02_21-AM-10_56_30
Last ObjectModification:
2017_01_20-PM-05_44_43
Theory : cubical!type!theory
Home
Index