The sandwich retract of the zig triangle

Over a zigzag datum the sandwich insertion is a section of the sandwich contraction: the module is a retract of its double-dual sandwich. The two legs are read on the carrier, where the zig triangle already lives; RS.Classical.Deligne.ZigzagSandwich supplies those two readings, RS.sandwichIns_hom and RS.modTensorπ_sandwichCon.

theorem RS.sandwichIns_sandwichCon {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) : CategoryTheory.CategoryStruct.comp (sandwichIns A d) (sandwichCon A d) = CategoryTheory.CategoryStruct.id M

The sandwich retract: over a zigzag datum the sandwich insertion is a section of the sandwich contraction.