Nuprl Definition : uniform-extension-fun
uniform-extension-fun{i:l}(Gamma;A;ext) ==
∀H,K:CubicalSet. ∀tau:K ⟶ H. ∀sigma:H ⟶ Gamma. ∀phi:{H ⊢ _:𝔽}. ∀u:{H, phi ⊢ _:(A)sigma}.
((ext H sigma phi u)tau = (ext K sigma o tau (phi)tau (u)tau) ∈ {K ⊢ _:((A)sigma)tau[(phi)tau |⟶ (u)tau]})
Definitions occuring in Statement :
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
context-subset: Gamma, phi,
face-type: 𝔽,
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: 𝔽,
all: ∀x:A. B[x],
cubical-term: {X ⊢ _:A},
context-subset: Gamma, phi,
equal: s = t ∈ T,
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
csm-ap-type: (AF)s,
apply: f a,
csm-comp: G o F,
csm-ap-term: (t)s
FDL editor aliases :
uniform-extension-fun
Latex:
uniform-extension-fun\{i:l\}(Gamma;A;ext) ==
\mforall{}H,K:CubicalSet. \mforall{}tau:K {}\mrightarrow{} H. \mforall{}sigma:H {}\mrightarrow{} Gamma. \mforall{}phi:\{H \mvdash{} \_:\mBbbF{}\}. \mforall{}u:\{H, phi \mvdash{} \_:(A)sigma\}.
((ext H sigma phi u)tau = (ext K sigma o tau (phi)tau (u)tau))
Date html generated:
2017_02_21-AM-10_56_56
Last ObjectModification:
2017_01_20-PM-05_50_59
Theory : cubical!type!theory
Home
Index