Nuprl Definition : refl-inv
refl-inv(b) == λI,alpha. (b(alpha) @ 0(𝕀))p(fst(alpha))
Definitions occuring in Statement :
cubicalpath-app: pth @ r,
interval-0: 0(𝕀),
cc-fst: p,
cubical-term-at: u(a),
csm-ap-type: (AF)s,
pi1: fst(t),
lambda: λx.A[x]
Definitions occuring in definition :
pi1: fst(t),
interval-0: 0(𝕀),
cubical-term-at: u(a),
cubicalpath-app: pth @ r,
cc-fst: p,
csm-ap-type: (AF)s,
lambda: λx.A[x]
FDL editor aliases :
refl-inv
Latex:
refl-inv(b) == \mlambda{}I,alpha. (b(alpha) @ 0(\mBbbI{}))p(fst(alpha))
Date html generated:
2017_02_21-AM-10_54_03
Last ObjectModification:
2017_02_20-PM-06_08_06
Theory : cubical!type!theory
Home
Index