# Contents

## Definition

An equation is a proposition of equality.

For

$x:X⊢\varphi \left(x\right):Z$x : X \vdash \phi(x) : Z

and

$y:Y⊢\psi \left(y\right):Z$y : Y \vdash \psi(y) : Z

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

$x:X,y:Y⊢\left[\varphi \left(x\right)=\psi \left(y\right)\right]:\mathrm{Type}$x : X, y : Y \vdash [\phi(x) = \psi(y)] : Type

and as a not-neccessarily (-1)-truncated type just the identity type

$x:X,y:Y⊢\left(\varphi \left(x\right)=\psi \left(y\right)\right):\mathrm{Type}$x : X, y : Y \vdash (\phi(x) = \psi(y)) : Type

itself.

The space of solutions of this equation is the dependent sum over all pairs of terms for which equality holds

$⊢\sum _{\genfrac{}{}{0}{}{x:X}{y:Y}}\left(\varphi \left(x\right)=\psi \left(y\right)\right):\mathrm{Type}\phantom{\rule{thinmathspace}{0ex}}.$\vdash \sum_{{x : X} \atop {y : Y}} (\phi(x) = \psi(y)) : Type \,.

Hence a particular solution $\mathrm{sol}$ is a term of this type

$⊢\mathrm{sol}:\sum _{\genfrac{}{}{0}{}{x:X}{y:Y}}\left(\varphi \left(x\right)=\psi \left(y\right)\right)\phantom{\rule{thinmathspace}{0ex}},$\vdash sol : \sum_{{x : X} \atop {y : Y}} (\phi(x) = \psi(y)) \,,

which means that it is a triple consisting of an $x\in X$, a $y\in Y$ and a witness $\mathrm{eq}:\left(\varphi \left(x\right)=\psi \left(y\right)\right)$ that these indeed solve the equation.

In categorical semantics this means that the space of solutions to an equation between expression $\varphi \left(x\right):Z$ and $\psi \left(y\right):Z$ of type $Z$ depending on variables of type $X$ and $Y$, respectively is the pullback

$\begin{array}{ccc}\sum _{\genfrac{}{}{0}{}{x:X}{y:Y}}\left(\varphi \left(x\right)=\psi \left(y\right)\right)& \to & Y\\ ↓& & {↓}^{\psi }\\ X& \stackrel{\varphi }{\to }& Z\end{array}\phantom{\rule{thinmathspace}{0ex}},$\array{ \sum_{{x : X} \atop {y : Y}} (\phi(x) = \psi(y)) &\to& Y \\ \downarrow && \downarrow^{\mathrlap{\psi}} \\ X &\stackrel{\phi}{\to}& Z } \,,

the fiber product of $\varphi$ 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.

## Examples

Revised on April 18, 2013 15:27:01 by Anonymous Coward (141.26.93.54)