In cubical type theory, regularity is the condition where composition along a degenerate? open box is the identity.
Last revised on August 21, 2026 at 13:19:21. See the history of this page for a list of all contributions to it.