Nuprl Definition : Glue-meaning

Glue-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(mb))=𝔽
            ∧ (allowed(mc) ∧ allowed(md))
            ∧ let A = type(allow(ma)) in
               let phi = term(allow(mb)) in
               let T = type(allow(mc)) in
               type(allow(md))=Equiv(T;A); let A = type(allow(ma)) in
                                            let cA = comp(allow(ma)) in
                                            let phi = term(allow(mb)) in
                                            let T = type(allow(mc)) in
                                            let cT = comp(allow(mc)) in
                                            let f = term(allow(md)) in
                                            cttType(levl= levelsup(level(allow(ma));level(allow(mc)))
                                                    type= gluetype(context-set(Xa);A;phi;T;f)
                                                    comp= comp(Glue [phi ⊢→ (T, f)] A) ))


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),  gluetype: gluetype(Gamma;A;phi;T;f),  glue-comp: comp(Glue [phi ⊢→ (T, f)] A) ,  cubical-equiv: Equiv(T;A),  context-subset: Gamma, phi,  face-type: 𝔽,  let: let,  spreadn: spread3,  and: P ∧ Q,  allow: allow(x),  allowed: allowed(x),  provision: provision(ok; v)
Definitions occuring in definition :  spreadn: spread3,  provision: Error :provision,  face-type: 𝔽,  and: P ∧ Q,  allowed: Error :allowed,  ctt-term-type-is: type(t)=T,  cubical-equiv: Equiv(T;A),  context-subset: Gamma, phi,  ctt-type-type: type(T),  ctt-type-comp: comp(T),  let: let,  ctt-term-term: term(t),  mk_ctt-type-mng: mk_ctt-type-mng,  levelsup: levelsup(x;y),  ctt-type-level: level(T),  allow: Error :allow,  gluetype: gluetype(Gamma;A;phi;T;f),  glue-comp: comp(Glue [phi ⊢→ (T, f)] A) ,  context-set: context-set(ctxt)
Latex:
Glue-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(mb))=\mBbbF{}
                        \mwedge{}  (allowed(mc)  \mwedge{}  allowed(md))
                        \mwedge{}  let  A  =  type(allow(ma))  in
                              let  phi  =  term(allow(mb))  in
                              let  T  =  type(allow(mc))  in
                              type(allow(md))=Equiv(T;A);
                        let  A  =  type(allow(ma))  in
                          let  cA  =  comp(allow(ma))  in
                          let  phi  =  term(allow(mb))  in
                          let  T  =  type(allow(mc))  in
                          let  cT  =  comp(allow(mc))  in
                          let  f  =  term(allow(md))  in
                          cttType(levl=  levelsup(level(allow(ma));level(allow(mc)))
                                          type=  gluetype(context-set(Xa);A;phi;T;f)
                                          comp=  comp(Glue  [phi  \mvdash{}\mrightarrow{}  (T,  f)]  A)  ))


Date html generated: 2020_05_21-AM-10_44_15
Last ObjectModification: 2020_05_08-PM-00_38_55

Theory : cubical!type!theory


Home Index