Nuprl Definition : bijection-equiv
bijection-equiv(X;A;B;f;g) ==
equiv-witness(cubical-lam(X;λI,alpha. (f (snd(alpha))));(λcontr-witness(X.discr(B);fiber-point(λI,alpha. (g (snd(alpha\000C)));
refl(q));refl(q))))
Definitions occuring in Statement :
equiv-witness: equiv-witness(f;cntr),
fiber-point: fiber-point(t;c),
cubical-fiber: Fiber(w;a),
contr-witness: contr-witness(X;c;p),
cubical-refl: refl(a),
discrete-cubical-type: discr(T),
cubical-lam: cubical-lam(X;b),
cubical-lambda: (λb),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s,
pi2: snd(t),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
cc-snd: q,
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
cubical-lam: cubical-lam(X;b),
cc-fst: p,
csm-ap-term: (t)s,
discrete-cubical-type: discr(T),
csm-ap-type: (AF)s,
cube-context-adjoin: X.A,
cubical-fiber: Fiber(w;a),
cubical-refl: refl(a),
fiber-point: fiber-point(t;c),
contr-witness: contr-witness(X;c;p),
cubical-lambda: (λb),
equiv-witness: equiv-witness(f;cntr)
FDL editor aliases :
bijection-equiv
Latex:
bijection-equiv(X;A;B;f;g) ==
equiv-witness(cubical-lam(X;\mlambda{}I,alpha.
(f
(snd(alpha))));(\mlambda{}contr-witness(X.discr(B);...;refl(q))))
Date html generated:
2017_02_21-AM-10_50_19
Last ObjectModification:
2017_02_10-PM-04_59_59
Theory : cubical!type!theory
Home
Index