Diagrammatic notations:
a wishlist

Shardul Chiplunkar,
Clément Pit-Claudel

Structural composition

Inductive Hydra: Set :=
| node: Hydrae -> Hydra
with Hydrae: Set :=
| hnil: Hydrae
| hcons: Hydra ->
    Hydrae -> Hydrae.

Definition left_hyd […]
Definition right_hyd […]

Definition whole_hyd :=
  (node
    (hcons left_hyd
    (hcons right_hyd
    hnil)).
Left subhydra diagram + Right subhydra diagram
= Whole hydra diagram

Good-looking idioms

Hydra diagram as nested boxes, narrow Hydra diagram as nested boxes, medium Hydra diagram as nested boxes, wide

Cost-benefit balance

(draw-rrd
  ("["
   (+ epsilon
      (mu "[token]"
          (+ epsilon ("," rec))))
   "]"))
Railroad diagram of JSON list syntax specification

Canonicity

(f ⊗ g) · (h ⊗ k) = (f · h) ⊗ (g · k)

f ⊗ idC · idB ⊗ g = idA ⊗ g · f ⊗ idD
String diagram demonstrating bifunctoriality A simple string diagram identity

Continuity

(sep (MCell f2 d1 c2) (sep (MCell p1
f1 b2) (sep (MCell p2 f2 b2) (sep
(MCell b1 x null c2) (sep (MListSeg c2
b2 L2') (sep (MCell b2 d2 null)
(MListSeg f1 b1 L1)))))))
Separation logic proof state after the tactic