In dependent type theory, the pullback of a pair of functions $f:A \to C$ and $g:B \to C$ is represented by the dependent sum type

$\sum_{x:A} \sum_{y:B} \mathrm{Id}_C(f(x),g(y))$What happens when instead of a pair of functions with codomain $C$, one has a family $x:I \vdash f(x):A(x) \to C$ of functions with codomain $C$? In category theory the corresponding notion is a wide pullback of a family of morphisms with codomain $C$. How does one represent the wide pullback of the family of functions $x:I \vdash f(x):A(x) \to C$?

]]>starting discussion page

]]>