Context
Equality and Equivalence
equivalence
-
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
-
identity type, equivalence of types, definitional isomorphism
-
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
-
natural equivalence, natural isomorphism
-
gauge equivalence
-
Examples.
principle of equivalence
equation
-
fiber product, pullback
-
homotopy pullback
-
Examples.
-
linear equation, differential equation, ordinary differential equation, critical locus
-
Euler-Lagrange equation, Einstein equation, wave equation
-
Schrödinger equation, Knizhnik-Zamolodchikov equation, Maurer-Cartan equation, quantum master equation, Euler-Arnold equation, Fuchsian equation, Fokker-Planck equation, Lax equation
Type theory
Contents
Idea
A form of heterogeneous equality in dependent type theory.
Definition
Given a type and an -dependent type , the fibered heterogeneous identity type is the dependent type indexed by
-
a pair of parameters
indexing a pair of fibers of ,
-
a pair of terms of these fiber types
whose “heterogeneous” identification is to be witnessed,
and defined equivalently as follows:
-
[Winterhalter 2023, p. 30] as the dependent sum type
of the heterogeneous identity types
over all identifications , where
denotes the type transport along ;
-
as the identification type of dependent pairs in the dependent sum type
The two definitions are equivalent due to the extensionality property of dependent sum types.
Inference rules with UIP
Beware that the following text writes “” for what above is denoted .
When the type theory has a set truncation axiom such as UIP or axiom K, one could use one of the following inference rules to define John Major equality:
McBride’s axiomatization
The axioms given in McBride 1999 are in OLEG? pseudocode, use Russell universes, and interpret relations impredicatively as functions into a type of all propositions. Here, the axioms are written as inference rules in a deduction system, modified slightly to use Tarski universes instead of Russell universes, as well as interpreting relations predicatively as prop-valued type families instead of functions into a type of all propositions. The axioms are as follows:
The use of Tarski universes instead of Russell universes makes it clear that John Major equality could be defined using inference rules for any type family instead of just the Tarski universe type family :
Winterhalter’s axiomatization
The axioms given in Winterhalter 2023 are in Coq pseudocode and use Russell universes. Here, the axioms are written as inference rules in a deduction system and modified slightly to use Tarski universes instead of Russell universes. The axioms are as follows:
The use of Tarski universes instead of Russell universes makes it clear that John Major equality could be defined using inference rules for any type family instead of just the Tarski universe type family :
Inference rules without UIP
It should be possible to take McBride’s axiomatization of John Major equality above and simply remove the requirement that John Major equality be a proposition-valued type family.
Then, the inference rules for forming John Major equality and terms are as follows. First the inference rule that defines the John Major equality itself, as a dependent type, in some context .
Formation rule for John Major equality:
Now the basic “introduction” rule, which says that everything is equal to itself in a canonical way.
Introduction rule for John Major equality:
Next we have the “elimination” rule:
Elimination rule for John Major equality:
The elimination rule then says that if:
- for any elements and , any elements and , and any John Major equality we have a type , and
- we have a specified dependent function
then we can construct a canonically defined term called the eliminator
for any , , , , and .
Then, we have the computation rule or beta-reduction rule. This says that for all elements and , substituting the dependent function into the eliminator along reflexivity for and yields an element equal to itself. Normally “equal” here means judgmental equality (a.k.a. definitional equality), but it is also possible for it to mean propositional equality (a.k.a. typal equality), so there are two possible computation rules.
Computation rules for John Major equality:
Finally, one might consider a uniqueness rule or eta-conversion rule. But similar to the case for identity types, a judgmental uniqueness rule for John Major equality implies that the type theory is an extensional type theory, in which case there is not much need for John Major equality, so such a rule is almost never written down. And as for identity types and other inductive types, the propositional/typal uniqueness rule is provable from the other four inference rules, so we don’t write it out explicitly.
References
-
Conor McBride, §5.1.3 in: Dependently Typed Functional Programs and their Proofs, (1999) [pdf]
(who speaks of “John Major equality” McBride 1999 with reference to British political discussion of that times)
-
Théo Winterhalter, A conservative and constructive translation from extensional type theory to weak type theory, Strength of Weak Type Theory, DutchCATS, 11 May 2023. (slides)