The monoidal comparison for base change at a complex point

Base change along a ℂ-point of a super-commutative algebra, with its comparison morphisms, their invertibility and the braided monoidal structure they give the fibre functor, in the five parts below: the residue algebra and base change over it (Residue.lean), the comparison in super vector spaces and its inverse (Comparison.lean), the calculus of generators the laws are checked in (Calculus.lean), the coherence and invertibility (Coherence.lean), and the monoidal and braided structure of the functor (Functor.lean).