# Can someone elaborate on a categorical/homotopical point made in the proof that $\Sigma 2 = S^1$, given in the HoTT book?

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."

## migrated from mathoverflow.netMar 6 '15 at 19:33

This question came from our site for professional mathematicians.

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

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.