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
Examples.
An equation is a proposition of equality.
For
and
two terms of some type $Z$ dependent on variables $x$ of type $X$ and $y$ of type $Y$, 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
itself.
The space of solutions of this equation is the dependent sum over all pairs of terms for which equality holds
Hence a particular solution $sol$ is a term of this type
which means that it is a triple consisting of an $x \in X$, a $y \in Y$ and a witness $eq : (\phi(x) = \psi(y))$ that these indeed solve the equation.
In categorical semantics this means that the space of solutions to an equation between expression $\phi(x) : Z$ and $\psi(y) : Z$ of type $Z$ depending on variables of type $X$ and $Y$, respectively is the pullback
the fiber product of $\phi$ with $\psi$. 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.
Last revised on September 11, 2019 at 06:32:37. See the history of this page for a list of all contributions to it.