Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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$?
Moved existing section on wide pushouts in dependent type theory over to wide pushout type
Moved existing section on wide pullbacks in dependent type theory over to wide pullback type
1 to 5 of 5