PiSigma: why does 'unfold' bind a variable?
I don't think there's any magic/necessary reason. IMO, it's written that way to make it more straightforwardly obvious that unfold is an analytic/checking elimination rule; just like why split is written the way it is rather than being written as first and second projections, and why case is written the way it is rather than being written like uneither in Haskell. 

Re the "analytic" bit, note how the other elimination rules are either synthetic/inferring (beta) or bidirectional (bang)