Nuprl Definition : ctt-opid-arity

ctt-opid-arity(t) ==
  if t =a "inv" then [<0, 0>]
  if t =a "max" then [<0, 0>; <0, 0>]
  if t =a "min" then [<0, 0>; <0, 0>]
  if t =a "comp" then [<0, 0>; <1, 1>; <1, 0>; <0, 0>]
  if t =a "glue" then [<0, 0>; <0, 0>; <0, 0>; <0, 0>]
  if t =a "unglue" then [<0, 1>; <0, 0>; <0, 1>; <0, 0>; <0, 0>]
  if t =a "meet" then [<0, 0>; <0, 0>]
  if t =a "join" then [<0, 0>; <0, 0>]
  if t =a "eq0" then [<0, 0>]
  if t =a "eq1" then [<0, 0>]
  if t =a "0" then []
  if t =a "1" then []
  if t =a "fst" then [<0, 1>; <1, 1>; <0, 0>]
  if t =a "snd" then [<0, 1>; <1, 1>; <0, 0>]
  if t =a "pair" then [<0, 0>; <1, 1>; <0, 0>]
  if t =a "lambda" then [<0, 1>; <1, 0>]
  if t =a "apply" then [<0, 0>; <1, 1>; <0, 0>]
  if t =a "pathabs" then [<0, 1>; <1, 0>]
  if t =a "pathap" then [<0, 1>; <0, 0>; <0, 0>]
  if t =a "decode1" then [<0, 0>]
  if t =a "decode2" then [<0, 0>]
  if t =a "decode3" then [<0, 0>]
  if t =a "encode1" then [<0, 1>]
  if t =a "encode2" then [<0, 1>]
  if t =a "encode3" then [<0, 1>]
  if t =a "I" then []
  if t =a "F" then []
  if t =a "pi" then [<0, 1>; <1, 1>]
  if t =a "sigma" then [<0, 1>; <1, 1>]
  if t =a "path" then [<0, 1>; <0, 0>; <0, 0>]
  if t =a "case" then [<0, 0>; <0, 0>; <0, 1>; <0, 1>]
  if t =a "Glue" then [<0, 1>; <0, 0>; <0, 1>; <0, 0>]
  else []
  fi 


Definitions occuring in Statement :  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  pair: <a, b>,  natural_number: $n,  token: "$token"
Definitions occuring in definition :  pair: <a, b>,  cons: [a / b],  token: "$token",  eq_atom: x =a y,  ifthenelse: if b then t else f fi ,  nil: [],  natural_number: $n
FDL editor aliases :  ctt-opid-arity
Latex:
ctt-opid-arity(t)  ==
    if  t  =a  "inv"  then  [ɘ,  0>]
    if  t  =a  "max"  then  [ɘ,  0>  ɘ,  0>]
    if  t  =a  "min"  then  [ɘ,  0>  ɘ,  0>]
    if  t  =a  "comp"  then  [ɘ,  0>  ə,  1>  ə,  0>  ɘ,  0>]
    if  t  =a  "glue"  then  [ɘ,  0>  ɘ,  0>  ɘ,  0>  ɘ,  0>]
    if  t  =a  "unglue"  then  [ɘ,  1>  ɘ,  0>  ɘ,  1>  ɘ,  0>  ɘ,  0>]
    if  t  =a  "meet"  then  [ɘ,  0>  ɘ,  0>]
    if  t  =a  "join"  then  [ɘ,  0>  ɘ,  0>]
    if  t  =a  "eq0"  then  [ɘ,  0>]
    if  t  =a  "eq1"  then  [ɘ,  0>]
    if  t  =a  "0"  then  []
    if  t  =a  "1"  then  []
    if  t  =a  "fst"  then  [ɘ,  1>  ə,  1>  ɘ,  0>]
    if  t  =a  "snd"  then  [ɘ,  1>  ə,  1>  ɘ,  0>]
    if  t  =a  "pair"  then  [ɘ,  0>  ə,  1>  ɘ,  0>]
    if  t  =a  "lambda"  then  [ɘ,  1>  ə,  0>]
    if  t  =a  "apply"  then  [ɘ,  0>  ə,  1>  ɘ,  0>]
    if  t  =a  "pathabs"  then  [ɘ,  1>  ə,  0>]
    if  t  =a  "pathap"  then  [ɘ,  1>  ɘ,  0>  ɘ,  0>]
    if  t  =a  "decode1"  then  [ɘ,  0>]
    if  t  =a  "decode2"  then  [ɘ,  0>]
    if  t  =a  "decode3"  then  [ɘ,  0>]
    if  t  =a  "encode1"  then  [ɘ,  1>]
    if  t  =a  "encode2"  then  [ɘ,  1>]
    if  t  =a  "encode3"  then  [ɘ,  1>]
    if  t  =a  "I"  then  []
    if  t  =a  "F"  then  []
    if  t  =a  "pi"  then  [ɘ,  1>  ə,  1>]
    if  t  =a  "sigma"  then  [ɘ,  1>  ə,  1>]
    if  t  =a  "path"  then  [ɘ,  1>  ɘ,  0>  ɘ,  0>]
    if  t  =a  "case"  then  [ɘ,  0>  ɘ,  0>  ɘ,  1>  ɘ,  1>]
    if  t  =a  "Glue"  then  [ɘ,  1>  ɘ,  0>  ɘ,  1>  ɘ,  0>]
    else  []
    fi 


Date html generated: 2020_05_20-PM-08_18_28
Last ObjectModification: 2020_05_07-PM-03_16_42

Theory : cubical!type!theory


Home Index