Nuprl Definition : equiv-bijection-is
equiv-bijection-is(e) == <λa1,a2,eq. Ax, λb.<equiv-contr(e;discr(b)).1.1(⋅), Ax>>
Definitions occuring in Statement :
equiv-contr: equiv-contr(f;a),
discrete-cubical-term: discr(t),
cubical-fst: p.1,
cubical-term-at: u(a),
empty-fset: {},
it: ⋅,
lambda: λx.A[x],
pair: <a, b>,
axiom: Ax
Definitions occuring in definition :
axiom: Ax,
it: ⋅,
empty-fset: {},
discrete-cubical-term: discr(t),
equiv-contr: equiv-contr(f;a),
cubical-fst: p.1,
cubical-term-at: u(a),
pair: <a, b>,
lambda: λx.A[x]
FDL editor aliases :
equiv-bijection-is
Latex:
equiv-bijection-is(e) == <\mlambda{}a1,a2,eq. Ax, \mlambda{}b.<equiv-contr(e;discr(b)).1.1(\mcdot{}), Ax>>
Date html generated:
2017_02_21-AM-10_52_02
Last ObjectModification:
2017_02_13-PM-00_26_59
Theory : cubical!type!theory
Home
Index