An equation is a proposition of equality.


x:Xϕ(x):Z x : X \vdash \phi(x) : Z


y:Yψ(y):Z y : Y \vdash \psi(y) : Z

two terms of some type ZZ dependent on variables xx of type XX and yy of type YY, respectively, the equation asserting that these two formulas are equal is as a proposition the bracket type

x:X,y:Y[ϕ(x)=ψ(y)]: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(ϕ(x)=ψ(y)):Type x : X, y : Y \vdash (\phi(x) = \psi(y)) : Type


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

x:Xy:Y(ϕ(x)=ψ(y)):Type. \vdash \sum_{{x : X} \atop {y : Y}} (\phi(x) = \psi(y)) : Type \,.

Hence a particular solution solsol is a term of this type

sol: x:Xy:Y(ϕ(x)=ψ(y)), \vdash sol : \sum_{{x : X} \atop {y : Y}} (\phi(x) = \psi(y)) \,,

which means that it is a triple consisting of an xXx \in X, a yYy \in Y and a witness eq:(ϕ(x)=ψ(y))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 ϕ(x):Z\phi(x) : Z and ψ(y):Z\psi(y) : Z of type ZZ depending on variables of type XX and YY, respectively is the pullback

x:Xy:Y(ϕ(x)=ψ(y)) Y ψ X ϕ Z, \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 ϕ\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.


Revised on May 3, 2017 12:30:58 by Urs Schreiber (