Deriving Dependently-Typed OOP from First Principles | Heykuki News