Nuprl Definition : cubical-equiv-by-cases
cubical-equiv-by-cases(G;B;f) == ((f)p ∨ IdEquiv(G.𝕀, (q=1);(B)p))
Definitions occuring in Statement :
cubical-id-equiv: IdEquiv(X;T),
case-term: (u ∨ v),
context-subset: Gamma, phi,
face-zero: (i=0),
face-one: (i=1),
interval-type: 𝕀,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s
Definitions occuring in definition :
cc-fst: p,
csm-ap-type: (AF)s,
cc-snd: q,
face-one: (i=1),
interval-type: 𝕀,
cube-context-adjoin: X.A,
context-subset: Gamma, phi,
cubical-id-equiv: IdEquiv(X;T),
csm-ap-term: (t)s,
face-zero: (i=0),
case-term: (u ∨ v)
FDL editor aliases :
cubical-equiv-by-cases
Latex:
cubical-equiv-by-cases(G;B;f) == ((f)p \mvee{} IdEquiv(G.\mBbbI{}, (q=1);(B)p))
Date html generated:
2017_01_10-PM-00_17_27
Last ObjectModification:
2016_12_27-PM-01_07_54
Theory : cubical!type!theory
Home
Index