ch:containers-ornaments: ch:containers-ornaments

Problem and result. Implement the finite list container, reverse morphism, one-hole plug, and vector forget calculation. The accepted run preserves shape three, reverses $[2,4,8]$, plugs $5$ into the middle hole, forgets the length-three vector, and rejects a length-two declaration carrying three contents.

Representation. Use MkContainer Nat (List Nat) for shape and contents, MkZipper (List Nat) (List Nat) for the stored prefix and suffix, and MkVec Nat (List Nat) for a vector view. This concrete list representation is less general than a position function $\mathsf{Fin}(n)\to X$, but makes the shape–contents invariant and the mutation independently observable.

First complete version. Define structural list length, append, and accumulator reverse. Validate a container by comparing its stored shape with the contents length; define the reverse morphism by preserving that shape and reversing only contents.

reverseMorphism : ContainerView -> ContainerView
let reverseMorphism view =
  match view
    case MkContainer shape contents ->
      MkContainer shape (reverse contents)

Remaining cases. Plug by appending the prefix to the new focus followed by the suffix. Forget a vector only after comparing declared and actual lengths. Apply all four operations to the named input and run the mismatched declaration through the same forget function.

A failing version. Return Forgotten contents without checking the declared length. The mutation MkVec 2 [2,4,8] is then accepted and the required shape-content-mismatch witness disappears.

Acceptance test. Require the five exact verdict lines, the final five-case summary, and audit result []; the command record is in appendix E.

Mathematical boundary. The corpus calculates one finite container and one list/vector forget map. It does not prove the container representation theorem, naturality, initiality, the derivative laws, or ornament transport.