Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
identity_type [2016/04/12 15:53]
nikolaj
identity_type [2016/07/20 01:23] (current)
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 ==
Link to graph
Log In
Improvements of the human condition