Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
rolled back changes, see the discussion on identity type.
added redirects for dependent identification and dependent identifications
Anonymous
I have fixed the title of the two references (there was a spurious “a” in both cases, also the italicization in the second item was missing).
I find the page name “dependent identity type” misleading, since also the standard ML identity type is, of course, dependent.
The alternative “heterogenous identity type” seems better. One could also try “relative identity type”.
I have rewritten the Definitions section of this article. The old Definitions section gives inference rules for the heterogeneous identity types, but those rules require that function types and dependent function types be defined beforehand, in addition to identity types. The new inference rules here are simpler in that they do not require any other type to be defined beforehand, only identity types.
In addition, the dependent application to identifications for dependent functions are defined the usual way, by induction on reflexivity of the index type’s identity type
Ionel Niculescu
Prompted by Madeleine Birchfield’s mention of this page on the HoTT Zulip, I cleaned up a lot of nonsense.
Theo Winterhalter talks about heterogeneous equality in his talk at DutchCATS a few months ago:
Anonymouse
Winterhalter’s heterogeneous identity types aren’t the same types as the heterogeneous identity types described in this article.
Here, the heterogeneous identity types $c =_{B}^{p} d$ take in as input a type $A$, a type family $B:A \to \mathrm{Type}$, elements $a:A$, $b:A$, $c:B(a)$, $d:B(b)$, and an identification $p:a =_A b$. In addition, there is only one constructor, which is the $hrefl_B(a, c):c =_{B}^{\mathrm{refl}_A(a)} c$.
Winterhalter’s heterogeneous identity types $a \;{_A}=_B b$ take in as input two types $A$ and $B$ and two elements $a:A$ and $b:B$, and in addition to the constructor $hrefl_A(a):a \;{_A}=_A a$ it also seems to have a transport constructor $heqtr(p, a):a \;{_A}=_B tr(p, a)$ for $p:A =_{Type} B$ and $a:A$.
I asked on the HoTT discord and apparently the version of heterogeneous identity types which appeared on Théo Winterhalter slides predates the ones given in the article, first being defined pre-HoTT by Conor McBride in his phd thesis titled “Dependently Typed Programs and their Proofs” - where he calls those types “John Major equality”. The heterogeneous identity types which appear in the article seem to be a post-HoTT thing.
Moved Theo Winterhalter reference to newly created article John Major equality
Anonymouse
1 to 21 of 21