Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
identity_type [2016/04/12 15:53] nikolaj |
identity_type [2016/07/20 01:23] nikolaj |
||
|---|---|---|---|
| Line 16: | Line 16: | ||
| | ${\large\frac{\dots,\,p\,:\,Id_A(x,y)\ \vdash\ Q(x,y,p)\,:\,\mathrm{Type}\hspace{.5cm}\dots\ \vdash\ t\,:\,Q(x,x,refl_x)}{\dots\ \vdash\ J(t,x,y,p)\,:\,Q(x,y,p)}}$ | | | ${\large\frac{\dots,\,p\,:\,Id_A(x,y)\ \vdash\ Q(x,y,p)\,:\,\mathrm{Type}\hspace{.5cm}\dots\ \vdash\ t\,:\,Q(x,x,refl_x)}{\dots\ \vdash\ J(t,x,y,p)\,:\,Q(x,y,p)}}$ | | ||
| - | This means that is we know that $x=y$, then if $Q(x,x)$ is true, then so must be $Q(x,y)$. | + | This means that if we know that $x=y$, then if $Q(x,x)$ is true, then so must be $Q(x,y)$. |
| == Computational rule == | == Computational rule == | ||
