コンテナ〈container〉は、アーボット/アルテンキルヒ/ガニ〈Michael Abbott, Thorsten Altenkirch, Neil Ghani〉等によって導入された、型理論と圏論に関わる概念です(「圏論的コンテナ」参照)。有向コンテナ〈directed container〉は、コンテナにモノイド類似構造を追加した代数系で、アーマン/チャップマン/ウウスタル〈Danel Ahman, James Chapman, Tarmo Uustalu〉が提案したものです。アーマン/チャップマン/ウウスタルによる有向コンテナの説明はAgda構文で記述されているので、初見では困惑します。普…