DaoFP Chapter 11 Exercises

exercise

Exercises from DaoFP, Chapter 11. Solutions: DaoFP Chapter 11 Solutions. Index: Map of Content.

Exercise 11.1.1

Implement tailV returning the tail of a non-zero-length vector. Try calling it with emptyV (Dependent Type).

Sources: DaoFP Exercise 11.1.1.

Solution: Solution 11.1.1

Exercise 11.2.1

Show that the Pullback with the Terminal Object as target is the Product.

Sources: DaoFP Exercise 11.2.1.

Solution: Solution 11.2.1

Exercise 11.2.2

Show that a Pullback is the Limit of a Diagram from the stick-figure category $a\to b\leftarrow c$.

Sources: DaoFP Exercise 11.2.2.

Solution: Solution 11.2.2

Exercise 11.2.3

Show that a Pullback in $\mathcal{C}$ with target $b$ is a Product in the Slice Category $\mathcal{C}/b$.

Sources: DaoFP Exercise 11.2.3; Kittenlab Lecture 13.

Solution: Solution 11.2.3

Exercise 11.2.4

Define the action of the Base Change Functor $f^{\ast }$ on a morphism $h:⟨e^{\prime },p^{\prime }⟩\to ⟨e,p⟩$ of $\mathcal{C}/a$.

Sources: DaoFP Exercise 11.2.4.

Solution: Solution 11.2.4

Exercise 11.4.1

Let $A=\{0,1\}$ and let $f$ map all of $B$ to $1$. How is the function on the right of the Dependent Product adjunction defined, and what does it do to the fiber over $0$?

Sources: DaoFP Exercise 11.4.1.

Solution: Solution 11.4.1

Exercise 11.4.2

Let $G=1$ with $x:1\to A$ selecting an element. Using the Dependent Product adjunction show: (i) $f^{\ast }1$ has singleton fibers over $f^{-1}(x)$ and empty fibers elsewhere; (ii) a map $\varphi :f^{\ast }1\to E$ is a partial section of $E$ over $f^{-1}(x)$; (iii) the fiber of ${\Pi }_{f}E$ over $x$ is such a partial section; (iv) what if $A$ is a singleton?

Sources: DaoFP Exercise 11.4.2.

Solution: Solution 11.4.2