DaoFP Chapter 17 Solutions

solution

Solutions to the exercises of DaoFP, Chapter 17: DaoFP Chapter 17 Exercises. Index: Map of Content.

Solution 17.1.1

proof — Exercise 17.1.1

Send every object of $\mathcal{C}$ to $0$ and every object of $\mathcal{D}$ to $1$; send morphisms of $\mathcal{C}$ to ${\mathrm{id}}_0$, morphisms of $\mathcal{D}$ to ${\mathrm{id}}_1$, and heteromorphisms (elements of $P⟨c,d⟩$) to the unique arrow $0\to 1$. Composition is preserved: composing a heteromorphism with a $\mathcal{C}$- or $\mathcal{D}$-morphism is again a heteromorphism, mapped to $0\to 1={\mathrm{id}}_1\circ (0\to 1)=(0\to 1)\circ {\mathrm{id}}_0$; there are no composable pairs of heteromorphisms since none go from $\mathcal{D}$ to $\mathcal{C}$.

Sources: DaoFP Exercise 17.1.1.

Solution 17.1.2

proof — Exercise 17.1.2

Let $\mathcal{C}=F^{-1}(0)$ and $\mathcal{D}=F^{-1}(1)$ be the full subcategories on the objects sent to $0$ and $1$. Since $2$ has no arrow $1\to 0$, there are no morphisms from $\mathcal{D}$-objects to $\mathcal{C}$-objects. Define $P⟨c,d⟩:=\mathcal{E}(c,d)$; it is a Profunctor ${\mathcal{C}}^{\mathrm{op}}\times \mathcal{D}\to \mathbf{Set}$ by pre- and post-composition. Then $\mathcal{E}$ is exactly the collage of $P$: objects the disjoint union, hom-sets as in $\mathcal{C}$, $\mathcal{D}$, or $P$, and composition inherited from $\mathcal{E}$.

Sources: DaoFP Exercise 17.1.2.

Solution 17.2.1

proof — Exercise 17.2.1

With $Q={\Delta }_d$ constant, $Q⟨d^{\prime },d^{\prime }⟩=d$ for all $d^{\prime }$ and $Q⟨\mathrm{id},g⟩=Q⟨g,\mathrm{id}⟩={\mathrm{id}}_d$. The first diamond, for $f:c\to c^{\prime }$, reads ${\alpha }_{c^{\prime }}\circ P⟨\mathrm{id},f⟩={\alpha }_c\circ P⟨f,\mathrm{id}⟩$ on $P⟨c^{\prime },c⟩$ — exactly the cowedge condition. The second diamond, for $g:d\to d^{\prime }$, reads ${\mathrm{id}}_d\circ {\alpha }_c={\mathrm{id}}_d\circ {\alpha }_c$, trivially true (the components do not depend on the second index).

Sources: DaoFP Exercise 17.2.1.

Solution 17.2.2

program — Exercise 17.2.2

newtype ProPair q p a b x y = ProPair (q a y, p x b)
instance (Profunctor p, Profunctor q) => Profunctor (ProPair q p a b) where
  dimap f g (ProPair (qay, pxb)) = ProPair (dimap id g qay, dimap f id pxb)

x is contravariant (it is the source of p x b), y covariant (the target of q a y).

Sources: DaoFP Exercise 17.2.2.

Solution 17.2.3

program — Exercise 17.2.3

newtype CoEndCompose p q a b = CoEndCompose (Coend (ProPair q p a b))
instance (Profunctor p, Profunctor q) => Profunctor (CoEndCompose p q) where
  dimap l r (CoEndCompose (Coend (ProPair (qax, pxb)))) =
    CoEndCompose (Coend (ProPair (dimap l id qax, dimap id r pxb)))

Extending on the left acts on q, extending on the right on p; the hidden middle type x is untouched — the same as for Procompose.

Sources: DaoFP Exercise 17.2.3.

Solution 17.3.1

proof — Exercise 17.3.1

Let $F:2\to \mathcal{C}$ pick $a,b$, and $P⟨x,y⟩:=Fy$. A wedge is an object $d$ with ${\pi }_1:d\to a$, ${\pi }_2:d\to b$; since $2$ has only identity arrows the wedge condition is vacuous. The universal wedge is therefore an object with two projections through which every such pair factors uniquely — the product $a\times b$. So ${\int }_{x:2}Fx=a\times b$.

Sources: DaoFP Exercise 17.3.1.

Solution 17.6.1

proof — Exercise 17.6.1

For an arbitrary set $S$: $\mathbf{Set}({\int }^x\mathcal{C}(a,x)\times Gx,S)\cong {\int }_x\mathbf{Set}(\mathcal{C}(a,x)\times Gx,S)\cong {\int }_x\mathbf{Set}(\mathcal{C}(a,x),S^{Gx})$. The functor $x\mapsto S^{Gx}$ is covariant (contravariant twice), so the covariant ninja Yoneda lemma gives $S^{Ga}\cong \mathbf{Set}(Ga,S)$. By the Yoneda corollary (objects with isomorphic mapping-outs are isomorphic), ${\int }^x\mathcal{C}(a,x)\times Gx\cong Ga$.

Sources: DaoFP Exercise 17.6.1.

Solution 17.7.1

program — Exercise 17.7.1

instance Functor (Day f g) where
  fmap h (Day abx fa gb) = Day (h . abx) fa gb

Sources: DaoFP Exercise 17.7.1.

Solution 17.7.2

program — Exercise 17.7.2

assoc :: Day f (Day g h) x -> Day (Day f g) h x
assoc (Day abx fa (Day cdb gc hd)) =
  Day (\((a, c), d) -> abx (a, cdb (c, d))) (Day (,) fa gc) hd

The new inner existential type is the pair (a, c); the combining function re-associates.

Sources: DaoFP Exercise 17.7.2.

Solution 17.7.3

program — Exercise 17.7.3

instance Functor f => Functor (FreeA f) where
  fmap h (DoneA x)          = DoneA (h x)
  fmap h (MoreA abx fa frb) = MoreA (h . abx) fa frb

Only the combining function at the head changes; the tail is untouched.

Sources: DaoFP Exercise 17.7.3.

Solution 17.9.1

proof — Exercise 17.9.1

Given $f:x^{\prime }\to x$ and $g:y\to y^{\prime }$, map $(l,r)\mapsto ((g\times {\mathrm{id}}_a)\circ l,r\circ (f\times {\mathrm{id}}_b))$: the first factor is covariant in $y$ (post-composition), the second contravariant in $x$ (pre-composition). Functoriality follows from that of composition and of $\times$. So it is a functor ${\mathcal{C}}^{\mathrm{op}}\times \mathcal{C}\to \mathbf{Set}$ in $⟨x,y⟩$ with $⟨s,t⟩,⟨a,b⟩$ fixed, and its coend is the existential lens.

Sources: DaoFP Exercise 17.9.1.