Nuprl Definition : transport-type
TransportType(A) == ∀[B:{G ⊢ _:c𝕌}]. ({G ⊢ _:(Path_c𝕌 A B)} ⟶ {G ⊢ _:(decode(A) ⟶ decode(B))})
Definitions occuring in Statement :
universe-decode: decode(t),
cubical-universe: c𝕌,
path-type: (Path_A a b),
cubical-fun: (A ⟶ B),
cubical-term: {X ⊢ _:A},
uall: ∀[x:A]. B[x],
function: x:A ⟶ B[x]
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
function: x:A ⟶ B[x],
path-type: (Path_A a b),
cubical-universe: c𝕌,
cubical-term: {X ⊢ _:A},
cubical-fun: (A ⟶ B),
universe-decode: decode(t)
FDL editor aliases :
transport-type
Latex:
TransportType(A) == \mforall{}[B:\{G \mvdash{} \_:c\mBbbU{}\}]. (\{G \mvdash{} \_:(Path\_c\mBbbU{} A B)\} {}\mrightarrow{} \{G \mvdash{} \_:(decode(A) {}\mrightarrow{} decode(B))\})
Date html generated:
2018_05_23-PM-06_22_14
Last ObjectModification:
2017_11_24-AM-10_03_20
Theory : cubical!type!theory
Home
Index