feat(algebra/homology/homotopy) : `mk_coinductive` (#12457)
`mk_coinductive` is the dual version of `mk_inductive` in the same file. `mk_inductive` is to build homotopy of chain complexes inductively and `mk_coinductive` is to build homotopy of cochain complexes inductively.
