この記事は圏論 Advent Calendar 2022 に18日目の記事として投稿されました。「（適切な極限をもつ）圏は対象のデータと射のデータ、そして可換図式のデータで決定される」という内部等式論理の基本的なアイデアについて紹介します。