Commit 2026-08-13 09:59 3d9e8eef
View on Github →feat(Algebra): IsUnital and IsNotUnital classes (#41923)
This adds Prop-type classes on multiplicative types that state whether a unit exists or not. This shouldn't really be used unless it is the only reasonable way to phrase or prove a statement.