Nuprl Definition : prod-ss

ss1 × ss2 ==
  Point=Point(ss1) × Point(ss2) #=λp,q. (fst(p) # fst(q) ∨ snd(p) # snd(q)) cotrans=λx,y,z,d. case d
                                                                                          of inl(a) =>
                                                                                          case ss1."#or" (fst(x)) 
                                                                                               (fst(y)) 
                                                                                               (fst(z)) 
                                                                                               a
                                                                                           of inl(u) =>
                                                                                           inl inl u
                                                                                           | inr(u) =>
                                                                                           inr (inl u) 
                                                                                          | inr(b) =>
                                                                                          case ss2."#or" (snd(x)) 
                                                                                               (snd(y)) 
                                                                                               (snd(z)) 
                                                                                               b
                                                                                           of inl(u) =>
                                                                                           inl (inr u )
                                                                                           | inr(u) =>
                                                                                           inr inr u  


Definitions occuring in Statement :  mk-ss: Point=P #=Sep cotrans=C,  ss-sep: x # y,  ss-point: Point(ss),  pi1: fst(t),  pi2: snd(t),  or: P ∨ Q,  apply: f a,  lambda: λx.A[x],  product: x:A × B[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  token: "$token",  record-select: r.x
Definitions occuring in definition :  mk-ss: Point=P #=Sep cotrans=C,  product: x:A × B[x],  ss-point: Point(ss),  or: P ∨ Q,  ss-sep: x # y,  lambda: λx.A[x],  pi1: fst(t),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  apply: f a,  record-select: r.x,  token: "$token",  pi2: snd(t),  inl: inl x,  inr: inr x 
FDL editor aliases :  prod-ss
Latex:
ss1  \mtimes{}  ss2  ==
    Point=Point(ss1)  \mtimes{}  Point(ss2)  \#=\mlambda{}p,q.  (fst(p)  \#  fst(q)  \mvee{}  snd(p)  \#  snd(q))
    cotrans=\mlambda{}x,y,z,d.  case  d
                                        of  inl(a)  =>
                                        case  ss1."\#or"  (fst(x))  (fst(y))  (fst(z))  a
                                          of  inl(u)  =>
                                          inl  inl  u
                                          |  inr(u)  =>
                                          inr  (inl  u) 
                                        |  inr(b)  =>
                                        case  ss2."\#or"  (snd(x))  (snd(y))  (snd(z))  b
                                          of  inl(u)  =>
                                          inl  (inr  u  )
                                          |  inr(u)  =>
                                          inr  inr  u   


Date html generated: 2019_10_31-AM-07_26_44
Last ObjectModification: 2019_09_19-PM-04_09_12

Theory : constructive!algebra


Home Index