Nothing here yet, have a $J$-rule

$$\frac{\Gamma,\, x:A \vdash d:D[y/x,\, \mathsf{refl}/p]}{\Gamma,\, x:A,\, y:A,\, p:\mathsf{Id}(x,y) \vdash j_d:D}$$