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.
added an alternate definition based upon the extensionality principle of dependent sum types, simplified previously added section to simply say that the two definitions are the same because of the extensionality principle of dependent sum types, and merged said section into the definitions section
Anonymouse
added the remark that:
For better or worse, the terminology “John Major equality” was coinded in McBride 1999 §5.1.3 with reference to British political discussion of that time.
Is it too late to find better terminology?
(McBride offers: “…aspiring to be equal to others than oneself is the politics of envy. In much the same way, $\simeq$ forms equations…” What?!)
Is it too late to find better terminology?
How about calling it McBride equality?
This would honor McBride’s mathematical insight while gracefully omitting the proliferation of his political comedy.
How about calling it McBride equality?
How about simply “heterogeneous equality”, which is the other terminology mentioned on the page? Unless this is ambiguous somehow?
I am not into this, but from the disambiguation entry heterogeneous equality I gather the need is felt to have a more specific term.
About the ambiguity in “heterogeneous equality”, Mike Shulman wrote on the HoTT Zulipchat:
Maybe we can distinguish the two with some more meaningful terminology. How about calling the version that depends on a path in the base, or an equality of types, indexed heterogeneous equality, and the other version (which admits a function to equalities of types) fibered heterogeneous equality? It’s the same relationship as other things we use those words for.
have renamed from “John Major equality” to “fibered heterogeneous identity type”
adjusted the definition-section (here)
(beyond just the type naming, I also changed the notation to be more straightforward throughout – for instance, generic terms of type $A$ are to be named “$a$” and not “$x$” and certainly not “$b$”, given that an $A$-dependent type “$B$” plays a major role, too)
For the time being I didn’t touch the following discussion of inference rules (starting here) except for a brief note highlighting the change in notation
1 to 10 of 10