Nuprl Definition : ctt-op-sort

ctt-op-sort(f) ==
  let k,v = f 
  in if k =a "opid"
       then if v ∈b ``Glue decode1 decode2 decode3 case sigma path pi F`` then "fibrant"
            if v =a "I" then "type"
            else "term"
            fi 
     if k =a "nType" then "fibrant"
     if k =a "nterm" then "term"
     else "fibrant"
     fi 


Definitions occuring in Statement :  deq-member: x ∈b L,  cons: [a / b],  nil: [],  atom-deq: AtomDeq,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  spread: spread def,  token: "$token"
Definitions occuring in definition :  spread: spread def,  deq-member: x ∈b L,  atom-deq: AtomDeq,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  token: "$token"
FDL editor aliases :  ctt-op-sort
Latex:
ctt-op-sort(f)  ==
    let  k,v  =  f 
    in  if  k  =a  "opid"
              then  if  v  \mmember{}\msubb{}  ``Glue  decode1  decode2  decode3  case  sigma  path  pi  F``  then  "fibrant"
                        if  v  =a  "I"  then  "type"
                        else  "term"
                        fi 
          if  k  =a  "nType"  then  "fibrant"
          if  k  =a  "nterm"  then  "term"
          else  "fibrant"
          fi 


Date html generated: 2020_05_20-PM-08_17_06
Last ObjectModification: 2020_05_07-PM-03_21_52

Theory : cubical!type!theory


Home Index