Lawvere theories
Haskell Community [Unofficial]
April 18, 2026
No, especially because
type Stuck :: Peano
type family Stuck where
This is an irreducible type family, but it’s still technically valid. It also is not an instance of Prop.
Discussion in the ATmosphere