Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: wide pullback

Bottom of Page

1 to 5 of 5

- CommentRowNumber1.
- CommentAuthorGuest
- CommentTimeMay 25th 2023
- PermaLink
Author: Guest
Format: MarkdownItexstarting discussion page <a href="https://ncatlab.org/nlab/revision/diff/wide+pullback/26">diff</a>, <a href="https://ncatlab.org/nlab/revision/wide+pullback/26">v26</a>, <a href="https://ncatlab.org/nlab/show/wide+pullback">current</a>

starting discussion page

diff, v26, current
- CommentRowNumber2.
- CommentAuthorGuest
- CommentTimeMay 25th 2023
- PermaLink
Author: Guest
Format: MarkdownItexIn 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$?

In dependent type theory, the pullback of a pair of functions $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">f:A \to C</annotation></semantics></math>$ and $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>g</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">g:B \to C</annotation></semantics></math>$ is represented by the dependent sum type
$<math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><munder><mo lspace="0.16667em" rspace="0.16667em">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><munder><mo lspace="0.16667em" rspace="0.16667em">∑</mo> <mrow><mi>y</mi><mo>:</mo><mi>B</mi></mrow></munder><msub><mi mathvariant="normal">Id</mi> <mi>C</mi></msub><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>,</mo><mi>g</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{x:A} \sum_{y:B} \mathrm{Id}_C(f(x),g(y))</annotation></semantics></math>$
What happens when instead of a pair of functions with codomain $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>$ , one has a family $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>x</mi><mo>:</mo><mi>I</mi><mo>⊢</mo><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">x:I \vdash f(x):A(x) \to C</annotation></semantics></math>$ of functions with codomain $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>$ ? In category theory the corresponding notion is a wide pullback of a family of morphisms with codomain $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>$ . How does one represent the wide pullback of the family of functions $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>x</mi><mo>:</mo><mi>I</mi><mo>⊢</mo><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">x:I \vdash f(x):A(x) \to C</annotation></semantics></math>$ ?
- CommentRowNumber3.
- CommentAuthorvarkor
- CommentTimeDec 9th 2023
- PermaLink
Author: varkor
Format: MarkdownItexAdded a reference for the terminology "wide pullback". <a href="https://ncatlab.org/nlab/revision/diff/wide+pullback/27">diff</a>, <a href="https://ncatlab.org/nlab/revision/wide+pullback/27">v27</a>, <a href="https://ncatlab.org/nlab/show/wide+pullback">current</a>

Added a reference for the terminology “wide pullback”.

diff, v27, current
- CommentRowNumber4.
- CommentAuthorMadeleine Birchfield
- CommentTimeFeb 10th 2024
- PermaLink
Author: Madeleine Birchfield
Format: MarkdownItexMoved existing section on wide pushouts in dependent type theory over to [[wide pushout type]] <a href="https://ncatlab.org/nlab/revision/diff/wide+pullback/32">diff</a>, <a href="https://ncatlab.org/nlab/revision/wide+pullback/32">v32</a>, <a href="https://ncatlab.org/nlab/show/wide+pullback">current</a>

Moved existing section on wide pushouts in dependent type theory over to wide pushout type

diff, v32, current
- CommentRowNumber5.
- CommentAuthorMadeleine Birchfield
- CommentTimeFeb 10th 2024
- PermaLink
Author: Madeleine Birchfield
Format: MarkdownItexMoved existing section on wide pullbacks in dependent type theory over to [[wide pullback type]] <a href="https://ncatlab.org/nlab/revision/diff/wide+pullback/34">diff</a>, <a href="https://ncatlab.org/nlab/revision/wide+pullback/34">v34</a>, <a href="https://ncatlab.org/nlab/show/wide+pullback">current</a>

Moved existing section on wide pullbacks in dependent type theory over to wide pullback type

diff, v34, current

1 to 5 of 5

nForum

Discussion Feed

Not signed in

Site Tag Cloud

nLab > Latest Changes: wide pullback