Nuprl Definition : poset_functor_extend

poset_functor_extend(C;I;L;E;c1;c2)
==r eval d = filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I) in
    if null(d)
    then cat-id(C) (L c1)
    else cat-comp(C) (L c1) (L flip(c1;hd(d))) (L c2) (E hd(d) c1) poset_functor_extend(C;I;L;E;flip(c1;hd(d));c2)
    fi 
poset_functor_extend(C;I;L;E;c1;c2) ==
  fix((λposet_functor_extend,c1. eval d = filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I) in
                                 if null(d)
                                 then cat-id(C) (L c1)
                                 else cat-comp(C) (L c1) (L flip(c1;hd(d))) (L c2) (E hd(d) c1) 
                                      (poset_functor_extend flip(c1;hd(d)))
                                 fi )) 
  c1


Definitions occuring in Statement :  name-morph-flip: flip(f;y),  cat-comp: cat-comp(C),  cat-id: cat-id(C),  hd: hd(l),  null: null(as),  filter: filter(P;l),  band: p ∧b q,  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  callbyvalue: callbyvalue,  filter: filter(P;l),  lambda: λx.A[x],  band: p ∧b q,  eq_int: (i =z j),  natural_number: $n,  ifthenelse: if b then t else f fi ,  null: null(as),  cat-id: cat-id(C),  cat-comp: cat-comp(C),  apply: f a,  name-morph-flip: flip(f;y),  hd: hd(l)
FDL editor aliases :  poset_functor_extend
Latex:
poset\_functor\_extend(C;I;L;E;c1;c2)
==r  eval  d  =  filter(\mlambda{}x.((c1  x  =\msubz{}  0)  \mwedge{}\msubb{}  (c2  x  =\msubz{}  1));I)  in
        if  null(d)
        then  cat-id(C)  (L  c1)
        else  cat-comp(C)  (L  c1)  (L  flip(c1;hd(d)))  (L  c2)  (E  hd(d)  c1) 
                  poset\_functor\_extend(C;I;L;E;flip(c1;hd(d));c2)
        fi 

Latex:
poset\_functor\_extend(C;I;L;E;c1;c2)  ==
    fix((\mlambda{}poset\_functor$_{extend}$,c1.  eval  d  =  filter(\mlambda{}x.((c1  x  =\msubz{}  0)  \mwedge{}\msubb{}  (c2  x  =\msubz{}\000C  1));I)  in
                                                                if  null(d)
                                                                then  cat-id(C)  (L  c1)
                                                                else  cat-comp(C)  (L  c1)  (L  flip(c1;hd(d)))  (L  c2)  (E  hd(d)  c1) 
                                                                          (poset\_functor$_{extend}$  flip(c1;hd(d)))
                                                                fi  )) 
    c1


Date html generated: 2016_06_16-PM-06_55_10
Last ObjectModification: 2015_09_23-AM-09_33_03

Theory : cubical!sets


Home Index