nForum - Discussion Feed (wide pullback) 2023-10-04T05:38:07+00:00 https://nforum.ncatlab.org/ Lussumo Vanilla & Feed Publisher Guest comments on "wide pullback" (109963) https://nforum.ncatlab.org/discussion/16562/?Focus=109963#Comment_109963 2023-05-25T16:51:37+00:00 2023-10-04T05:38:07+00:00 Guest https://nforum.ncatlab.org/account/21/ In dependent type theory, the pullback of a pair of functions f:A&rightarrow;Cf:A \to C and g:B&rightarrow;Cg:B \to C is represented by the dependent sum type &Sum; x:A&Sum; y:BId ...

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$?

]]>
Guest comments on "wide pullback" (109962) https://nforum.ncatlab.org/discussion/16562/?Focus=109962#Comment_109962 2023-05-25T16:43:26+00:00 2023-10-04T05:38:07+00:00 Guest https://nforum.ncatlab.org/account/21/ starting discussion page diff, v26, current

starting discussion page

]]>