Equality and Equivalence
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence in homotopy type theory
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
natural equivalence, natural isomorphism
principle of equivalence
fiber product, pullback
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
An equation is a proposition of equality.
two terms of some type dependent on variables of type and of type , respectively, the equation asserting that these two formulas are equal is as a proposition the bracket type
and as a not-neccessarily (-1)-truncated type just the identity type
The space of solutions of this equation is the dependent sum over all pairs of terms for which equality holds
Hence a particular solution is a term of this type
which means that it is a triple consisting of an , a and a witness that these indeed solve the equation.
In categorical semantics this means that the space of solutions to an equation between expression and of type depending on variables of type and , respectively is the pullback
the fiber product of with . In the context of homotopy type theory this is the homotopy pullback/homotopy fiber product.
See at homotopy pullback – concrete constructions – In homotopy type theory for more on this.
Revised on December 10, 2014 20:33:57
by Urs Schreiber