4
$\begingroup$

In chapter 6, specifically in the section about suspensions a proof is given that $∑2 = S^1$. The book says that $\mathrm{transport}^{x \mapsto g(f(x)) = x}(\mathrm{refl}_N, \mathrm{merid}(y)) = g(f(\mathrm{merid}(y))^{-1} \cdot \mathrm{refl}_N \cdot \mathrm{merid}(y)$ by "transport in path spaces and pulled back fibrations." Of course this is referring to Theorem 2.11.3 (in my copy), i.e. the fact that: $$ \mathrm{transport}^{x \mapsto f(x) = g(x)}(p, q) = \mathrm{ap}_f(p)^{-1} \cdot \mathrm{refl}_N \cdot \mathrm{ap}_g(q)$ $$

What does this have to to with pulled back fibrations, in particular in what sense is the type family $x \mapsto f(x) = g(x)$ a pulled back fibartion?

Here's what I've tried. We want to make the type family $x \mapsto f(x) = g(x)$, since the total space of the fibration that this type family represents is $\sum_{x : A} f(x) = g(x)$ into a pullback, we can try this commutative square: $$ \require{AMScd} \begin{CD} \sum_{x : A} f(x) = g(x) @>pr_1>> A \\ @VVpr_1V @VVgV \\ A @>f>> B \end{CD} $$ However, there is at least one problem with this approach. The above diagram isn't a pullback square, because it fails to be universal, consider a commutative square of this form $$ \require{AMScd} \begin{CD} X @>p>> A \\ @VVqV @VVgV \\ A @>f>> B \end{CD} $$ We want a morphism from $X$ to $\sum_{x : A} f(x) = g(x)$. To put it into type theoretical language, we have a type $X$ and functions $p, q : X \rightarrow A$ and proofs that $g \circ p = f \circ q$. We want to prove that there exists a function of the type $X \rightarrow \sum_{x : A} f(x) = g(x)$. So we can apply the given data to obtain that $g(p(x)) = f(q(x))$ for any $x : X$, however the function that we obtain has the type $X \rightarrow \sum_{a : A} \sum_{b : A} f(a) = g(b)$, which is not the type we wanted. My current conclusion is that the above lemma about transport isn't about "pulled back fibrations."

$\endgroup$

migrated from mathoverflow.net Mar 6 '15 at 19:33

This question came from our site for professional mathematicians.

  • $\begingroup$ Look at the book's definition of the pullback along two maps, and you'll see a similarity in form. $\endgroup$ – Ptharien's Flame Mar 6 '15 at 17:01
  • 1
    $\begingroup$ You mean $\sum_{a, b : B} f(a) = g(b)$ right? $\endgroup$ – 11Kilobytes Mar 6 '15 at 17:02
  • 1
    $\begingroup$ I see a similarity but I don't know how to formalise it. $\endgroup$ – 11Kilobytes Mar 6 '15 at 17:04
4
$\begingroup$

The type family $x\mapsto f(x)=g(x)$ is a restriction of the family $(x,y)\mapsto (x=y)$ over $A\times A$ along the map $(f,g):A\to A\times A$. The word "pullback" is used because restriction (i.e. composition) of a type family along a map corresponds to pullback of the associated fibrations.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.