Executable-First Lens Integration: Extending the Lean-Verified Heyting Core with Law-Preserving Transports

Executable-First Lens Integration: Extending the Lean-Verified Heyting Core with Law-Preserving Transports | apoth3osis