### Downcasing SDG

Quick index:
```1. Proposition 7
================
Proposition 7: for any f: A --> A, the diagram
b |-> c

\tdf
A×A ------> A×A      b.b_a |------> c,c_a
|           |         -              -
\aa |           | \aa     |              |
v           v         v              v
A^D ------> A^D     da|->b+db |--> da|->c+dc
f^D

b,b_a |--------> c,c_{b}b_a
-                   -
|                   v
v             da|->c+c_{b}b_{a}dx
da|->b+b_{a}da |--> da|->c(b+b_{a}da)

commutes, where \tdf: A×A -> A×A is the map with the description

(a_0, a_1) -> (f(a_0), a_1·f'(a_0))
b,b_a |--------> c,c_{b}b_a

Proof: it suffices to prove that the exponential adjoint diagram
commutes. The exponential diagram is the outer diagram in

\tdf×D
A×A×D ------> A×A×D          b,b_a,da |---------> c,c_a,da
|   \         |                -   /               -
\aa×D |    \ \czaa  | \aa×D          |    \---\          |
v     v       v                v         v         |
A^D×D --> A   A^D×D       (da|->b+db),da |-> b+db    |
|   ev    \   |                -               /   |
f^D×D |        f \  | ev             |                \  |
v     ev    v v                v                 v v
A^D×D --------> A         (da|->c+dc),da |--------> d+dc

b,b_a,da |------------------------> c,c_{b}b_{a},da
-	 /			            -
|	  \-------\		            |
v		   v                        v
(da|->b+b_{a}da),da |-> b+b_{a}da   (da|->c+c_{b}b_{a}da),da
-			     /            -
|			      \-----\     v
v				     v c+c_{b}b_{a}da
(da|->c(b+b_{a}da)),da |-------------------> c(b+b_{a}da)

```