Nuprl Definition : uabetatype

uabetatype(G;A;B;f) ==
  ΠEquiv(decode(A);decode(B)) Π(decode(A))p (Path_((decode(B))p)p app(f G.Equiv(decode(A);decode(B)).(decode(A))p 
                                                                      ((A)p)p 
                                                                      app(UA; (q)p); q) app(equiv-fun((q)p); q))


Definitions occuring in Statement :  univ-a: UA,  universe-decode: decode(t),  equiv-fun: equiv-fun(f),  cubical-equiv: Equiv(T;A),  path-type: (Path_A a b),  cubical-app: app(w; u),  cubical-pi: ΠA B,  cc-snd: q,  cc-fst: p,  cube-context-adjoin: X.A,  csm-ap-term: (t)s,  csm-ap-type: (AF)s,  apply: f a
Definitions occuring in definition :  cubical-pi: ΠA B,  path-type: (Path_A a b),  apply: f a,  univ-a: UA,  cube-context-adjoin: X.A,  cubical-equiv: Equiv(T;A),  csm-ap-type: (AF)s,  universe-decode: decode(t),  cubical-app: app(w; u),  equiv-fun: equiv-fun(f),  csm-ap-term: (t)s,  cc-fst: p,  cc-snd: q
FDL editor aliases :  uabetatype
Latex:
uabetatype(G;A;B;f)  ==
    \mPi{}Equiv(decode(A);decode(B))  \mPi{}(decode(A))p  (Path\_((decode(B))p)p
                                                                                                    app(f  G.Equiv(decode(A);decode(B)).(decode(A))p 
                                                                                                            ((A)p)p 
                                                                                                            app(UA;  (q)p);  q)  app(equiv-fun((q)p);  q))


Date html generated: 2018_05_23-PM-06_22_46
Last ObjectModification: 2017_11_24-AM-10_21_56

Theory : cubical!type!theory


Home Index