Nuprl Definition : case-meaning

case-meaning{i:l}(A; B; C; D) ==
  let Xa,a,ma = A in 
  let Xb,b,mb = B in 
  let Xc,c,mc = C in 
  let Xd,d,md = D in 
  provision((allowed(ma) ∧ allowed(mb))
            ∧ (type(allow(ma))=𝔽
              ∧ type(allow(mb))=𝔽
              ∧ context-set(Xa) ⊢ ((term(allow(ma)) ∧ term(allow(mb))) ⇒ 0(𝔽))
              ∧ context-set(Xa) ⊢ (1(𝔽) ⇒ (term(allow(ma)) ∨ term(allow(mb)))))
            ∧ allowed(mc)
            ∧ allowed(md); cttType(levl= levelsup(level(allow(mc));level(allow(md)))
                                   type= (if term(allow(ma)) then type(allow(mc)) else type(allow(md)))
                                   comp= case-type-comp(context-set(Xa);
                                                        term(allow(ma));
                                                        term(allow(mb));
                                                        type(allow(mc));
                                                        type(allow(md));
                                                        comp(allow(mc));
                                                        comp(allow(md)))))


Definitions occuring in Statement :  context-set: context-set(ctxt),  mk_ctt-type-mng: mk_ctt-type-mng,  ctt-type-comp: comp(T),  ctt-type-type: type(T),  ctt-type-level: level(T),  ctt-term-term: term(t),  ctt-term-type-is: type(t)=T,  levelsup: levelsup(x;y),  case-type-comp: case-type-comp(G; phi; psi; A; B; cA; cB),  case-type: (if phi then A else B),  face-term-implies: Gamma ⊢ (phi ⇒ psi),  face-or: (a ∨ b),  face-and: (a ∧ b),  face-1: 1(𝔽),  face-0: 0(𝔽),  face-type: 𝔽,  spreadn: spread3,  and: P ∧ Q,  allow: allow(x),  allowed: allowed(x),  provision: provision(ok; v)
Definitions occuring in definition :  spreadn: spread3,  provision: Error :provision,  ctt-term-type-is: type(t)=T,  face-type: 𝔽,  face-and: (a ∧ b),  face-0: 0(𝔽),  face-term-implies: Gamma ⊢ (phi ⇒ psi),  face-1: 1(𝔽),  face-or: (a ∨ b),  and: P ∧ Q,  allowed: Error :allowed,  mk_ctt-type-mng: mk_ctt-type-mng,  levelsup: levelsup(x;y),  ctt-type-level: level(T),  case-type: (if phi then A else B),  case-type-comp: case-type-comp(G; phi; psi; A; B; cA; cB),  context-set: context-set(ctxt),  ctt-term-term: term(t),  ctt-type-type: type(T),  ctt-type-comp: comp(T),  allow: Error :allow
Latex:
case-meaning\{i:l\}(A;  B;  C;  D)  ==
    let  Xa,a,ma  =  A  in 
    let  Xb,b,mb  =  B  in 
    let  Xc,c,mc  =  C  in 
    let  Xd,d,md  =  D  in 
    provision((allowed(ma)  \mwedge{}  allowed(mb))
                        \mwedge{}  (type(allow(ma))=\mBbbF{}
                            \mwedge{}  type(allow(mb))=\mBbbF{}
                            \mwedge{}  context-set(Xa)  \mvdash{}  ((term(allow(ma))  \mwedge{}  term(allow(mb)))  {}\mRightarrow{}  0(\mBbbF{}))
                            \mwedge{}  context-set(Xa)  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  (term(allow(ma))  \mvee{}  term(allow(mb)))))
                        \mwedge{}  allowed(mc)
                        \mwedge{}  allowed(md);
                        cttType(levl=  levelsup(level(allow(mc));level(allow(md)))
                                        type=  (if  term(allow(ma))  then  type(allow(mc))  else  type(allow(md)))
                                        comp=  case-type-comp(context-set(Xa);
                                                                                  term(allow(ma));
                                                                                  term(allow(mb));
                                                                                  type(allow(mc));
                                                                                  type(allow(md));
                                                                                  comp(allow(mc));
                                                                                  comp(allow(md)))))


Date html generated: 2020_05_21-AM-10_43_58
Last ObjectModification: 2020_05_11-PM-03_07_17

Theory : cubical!type!theory


Home Index