Nuprl Definition : glue-comp

comp(Glue [phi ⊢→ (T, f)] A)  ==
  λH,sigma,psi,b,b0. let a = unglue(b) in
                      let a0 = unglue(b0) in
                      let a'1 = comp (cA)sigma [psi ⊢→ a] a0 in
                      let t'1 = comp (cT)sigma [psi ⊢→ b] b0 in
                      let w = pres (equiv-fun(f))sigma [psi ⊢→ b] b0 in
                      let st = (t'1 ∨ (b)[1(𝕀)]) in
                      let sw = (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)) in
                      let cF = fiber-comp(H, ((phi)sigma)[1(𝕀)];((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)];
                                          equiv-fun(((f)sigma)[1(𝕀)]);a'1;(cT)sigma o [1(𝕀)];(cA)sigma o [1(𝕀)]) in
                      let z = equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st,  sw)] a'1 in
                      let t1 = fiber-member(z) in
                      let alpha = fiber-path(z) in
                      let a1 = comp (cA)sigma o [1(𝕀)] o p [(((phi)sigma)[1(𝕀)] ∨ psi) ⊢→ ((alpha)p @ q ∨ (a[1])p)]
                                   a'1 in
                      glue [((phi)sigma)[1(𝕀)] ⊢→ t1] a1


Definitions occuring in Statement :  unglue-term: unglue(b),  glue-term: glue [phi ⊢→ t] a,  equiv-term: equiv f [phi ⊢→ (t,  c)] a,  pres: pres f [phi ⊢→ t] t0,  fiber-comp: fiber-comp(X;T;A;w;a;cT;cA),  comp_term: comp cA [phi ⊢→ u] a0,  csm-comp-structure: (cA)tau,  equiv-fun: equiv-fun(f),  fiber-path: fiber-path(p),  fiber-member: fiber-member(p),  term-to-path: <>(a),  cubical-path-app: pth @ r,  case-term: (u ∨ v),  partial-term-1: u[1],  face-forall: (∀ phi),  context-subset: Gamma, phi,  face-or: (a ∨ b),  interval-1: 1(𝕀),  interval-0: 0(𝕀),  interval-type: 𝕀,  cubical-app: app(w; u),  csm-id-adjoin: [u],  cc-snd: q,  cc-fst: p,  cube-context-adjoin: X.A,  csm-ap-term: (t)s,  csm-ap-type: (AF)s,  csm-comp: G o F,  let: let,  lambda: λx.A[x]
Definitions occuring in definition :  csm-ap-term: (t)s,  interval-1: 1(𝕀),  csm-id-adjoin: [u],  context-subset: Gamma, phi,  csm-comp-structure: (cA)tau,  equiv-fun: equiv-fun(f),  csm-ap-type: (AF)s,  fiber-comp: fiber-comp(X;T;A;w;a;cT;cA),  let: let,  cubical-app: app(w; u),  face-forall: (∀ phi),  partial-term-1: u[1],  cc-fst: p,  term-to-path: <>(a),  case-term: (u ∨ v),  interval-type: 𝕀,  cube-context-adjoin: X.A,  pres: pres f [phi ⊢→ t] t0,  comp_term: comp cA [phi ⊢→ u] a0,  interval-0: 0(𝕀),  unglue-term: unglue(b),  lambda: λx.A[x],  csm-comp: G o F,  equiv-term: equiv f [phi ⊢→ (t,  c)] a,  face-or: (a ∨ b),  fiber-member: fiber-member(p),  fiber-path: fiber-path(p),  cubical-path-app: pth @ r,  cc-snd: q,  glue-term: glue [phi ⊢→ t] a
FDL editor aliases :  glue-comp
Latex:
comp(Glue  [phi  \mvdash{}\mrightarrow{}  (T,  f)]  A)    ==
    \mlambda{}H,sigma,psi,b,b0.  let  a  =  unglue(b)  in
                                            let  a0  =  unglue(b0)  in
                                            let  a'1  =  comp  (cA)sigma  [psi  \mvdash{}\mrightarrow{}  a]  a0  in
                                            let  t'1  =  comp  (cT)sigma  [psi  \mvdash{}\mrightarrow{}  b]  b0  in
                                            let  w  =  pres  (equiv-fun(f))sigma  [psi  \mvdash{}\mrightarrow{}  b]  b0  in
                                            let  st  =  (t'1  \mvee{}  (b)[1(\mBbbI{})])  in
                                            let  sw  =  (w  \mvee{}  <>((app((equiv-fun(f))sigma;  b)[1])p))  in
                                            let  cF  =  fiber-comp(H,  ((phi)sigma)[1(\mBbbI{})];((T)sigma)[1(\mBbbI{})];((A)sigma)[1(\mBbbI{})];
                                                                                    equiv-fun(((f)sigma)[1(\mBbbI{})]);a'1;(cT)sigma  o  [1(\mBbbI{})];
                                                                                    (cA)sigma  o  [1(\mBbbI{})])  in
                                            let  z  =  equiv  ((f)sigma)[1(\mBbbI{})]  [((\mforall{}  (phi)sigma)  \mvee{}  psi)  \mvdash{}\mrightarrow{}  (st,    sw)]  a'1  in
                                            let  t1  =  fiber-member(z)  in
                                            let  alpha  =  fiber-path(z)  in
                                            let  a1  =  comp  (cA)sigma  o  [1(\mBbbI{})]  o  p  [(((phi)sigma)[1(\mBbbI{})]  \mvee{}  psi)  \mvdash{}\mrightarrow{}
                                                                                                                        ((alpha)p  @  q  \mvee{}  (a[1])p)]  a'1  in
                                            glue  [((phi)sigma)[1(\mBbbI{})]  \mvdash{}\mrightarrow{}  t1]  a1


Date html generated: 2016_06_16-PM-02_38_40
Last ObjectModification: 2016_06_06-PM-04_55_35

Theory : cubical!type!theory


Home Index