Nuprl Definition : equiv-path2
equiv-path2(G;A;B;cA;cB;f) ==
comp(Glue [((q=0) ∨ (q=1)) ⟶ ((if (q=0) then (A)p else (B)p), cubical-equiv-by-cases(G;B;f))] (B)p)
Definitions occuring in Statement :
cubical-equiv-by-cases: cubical-equiv-by-cases(G;B;f),
glue-comp: comp(Glue [phi ⟶ (T, f)] A) ,
case-type-comp: case-type-comp(G; phi; psi; A; B; cA; cB),
csm-comp-structure: (cA)tau,
case-type: (if phi then A else B),
face-zero: (i=0),
face-one: (i=1),
face-or: (a ∨ b),
interval-type: 𝕀,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-type: (AF)s
Definitions occuring in definition :
cubical-equiv-by-cases: cubical-equiv-by-cases(G;B;f),
cc-fst: p,
interval-type: 𝕀,
cube-context-adjoin: X.A,
csm-comp-structure: (cA)tau,
csm-ap-type: (AF)s,
cc-snd: q,
face-one: (i=1),
face-zero: (i=0),
case-type-comp: case-type-comp(G; phi; psi; A; B; cA; cB),
case-type: (if phi then A else B),
face-or: (a ∨ b),
glue-comp: comp(Glue [phi ⟶ (T, f)] A)
FDL editor aliases :
equiv-path2
Latex:
equiv-path2(G;A;B;cA;cB;f) ==
comp(Glue [((q=0) \mvee{} (q=1)) \mvdash{}\mrightarrow{} ((if (q=0) then (A)p else (B)p), cubical-equiv-by-cases(G;B;f))]
(B)p)
Date html generated:
2017_01_10-PM-00_19_28
Last ObjectModification:
2017_01_01-AM-00_09_52
Theory : cubical!type!theory
Home
Index